Physlib.QuantumMechanics.HilbertSpaces.OneDimension.Gaussians

Imports
                /-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QuantumMechanics.HilbertSpaces.OneDimension.Basic
public import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
public import Physlib.Meta.TODO.Basic

              
                Gaussians and the hilbert space
              

              TODO "Generalize Gaussian states to d dimensions and SpaceDHilbertSpace
  using InnerProductSpace.gaussian from Physlib/Mathematics/InnerProductSpace/Gaussian
  and SpaceDHilbertSpace.schwartzIncl. Some of the results in this file have become automatic
  given InnerProductSpace.gaussian is a Schwartz map, e.g. gaussian_integrable and gaussian_memHS
  (via schwartzIncl), and some hold more generally for any Schwartz map or member
  of SchwartzSubmodule, e.g. abs_mul_gaussian_integrable."@[expose] public section

              
                Gaussians
              

              lemma gaussian_integrable {b : ℝ} (c : ℝ) (hb : 0 < b) :
    MeasureTheory.Integrable (fun x => (Real.exp (- b * (x - c)^ 2) : ℂ)) :=
  MeasureTheory.Integrable.ofReal (Integrable.comp_sub_right
    (f := (fun x => Real.exp (- b * x ^ 2))) (integrable_exp_neg_mul_sq hb) ..)lemma gaussian_aestronglyMeasurable {b : ℝ} (c : ℝ) (hb : 0 < b) :
    AEStronglyMeasurable (fun x => (Real.exp (- b * (x - c) ^2) : ℂ)) volume :=
  MeasureTheory.Integrable.aestronglyMeasurable (gaussian_integrable c hb)

lemma gaussian_memHS {b : ℝ} (c : ℝ) (hb : 0 < b) :
    MemHS (fun x => (Real.exp (- b * (x - c) ^2) : ℂ)) := byb:ℝc:ℝhb:0 < b⊢ MemHS fun x => ↑(Real.exp (-b * (x - c) ^ 2))
  rw [memHS_iffb:ℝc:ℝhb:0 < b⊢ AEStronglyMeasurable (fun x => ↑(Real.exp (-b * (x - c) ^ 2))) volume ∧
  Integrable (fun x => ‖↑(Real.exp (-b * (x - c) ^ 2))‖ ^ 2) volumeb:ℝc:ℝhb:0 < b⊢ AEStronglyMeasurable (fun x => ↑(Real.exp (-b * (x - c) ^ 2))) volume ∧
  Integrable (fun x => ‖↑(Real.exp (-b * (x - c) ^ 2))‖ ^ 2) volume]b:ℝc:ℝhb:0 < b⊢ AEStronglyMeasurable (fun x => ↑(Real.exp (-b * (x - c) ^ 2))) volume ∧
  Integrable (fun x => ‖↑(Real.exp (-b * (x - c) ^ 2))‖ ^ 2) volume
  refine ⟨gaussian_aestronglyMeasurable c hb, ?_⟩b:ℝc:ℝhb:0 < b⊢ Integrable (fun x => ‖↑(Real.exp (-b * (x - c) ^ 2))‖ ^ 2) volume
  simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_neg, Complex.ofReal_mul,
    Complex.ofReal_pow, Complex.ofReal_sub, Complex.norm_exp, Complex.neg_re,
    Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero]b:ℝc:ℝhb:0 < b⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume
  have h1 : (fun (x : ℝ) => Real.exp (-(b * ((x - c : ℂ) ^ 2).re)) ^ 2) =
    fun y => (fun x => Real.exp (- (2 * b) * x ^ 2)) (y - c) := byb:ℝc:ℝhb:0 < b⊢ MemHS fun x => ↑(Real.exp (-b * (x - c) ^ 2))b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume
    ext xb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2 = (fun x => Real.exp (-(2 * b) * x ^ 2)) (x - c)b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume
    simp only [neg_mul]b:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2 = Real.exp (-(2 * b * (x - c) ^ 2))b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume
    trans Real.exp (-(b * ((x - c: ℂ) ^ 2).re)) ^ (2 : ℝ)b:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2 = Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2b:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2 = Real.exp (-(2 * b * (x - c) ^ 2))b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume
    ·b:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2 = Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume simpAll goals completed! 🐙b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume
    rw [← Real.exp_mulb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-(b * ((↑x - ↑c) ^ 2).re) * 2) = Real.exp (-(2 * b * (x - c) ^ 2))b:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-(b * ((↑x - ↑c) ^ 2).re) * 2) = Real.exp (-(2 * b * (x - c) ^ 2))b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume]b:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-(b * ((↑x - ↑c) ^ 2).re) * 2) = Real.exp (-(2 * b * (x - c) ^ 2))b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume
    simp only [neg_mul, Real.exp_eq_exp, neg_inj]b:ℝc:ℝhb:0 < bx:ℝ⊢ b * ((↑x - ↑c) ^ 2).re * 2 = 2 * b * (x - c) ^ 2b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume
    rw [← Complex.ofReal_sub,b:ℝc:ℝhb:0 < bx:ℝ⊢ b * (↑(x - c) ^ 2).re * 2 = 2 * b * (x - c) ^ 2b:ℝc:ℝhb:0 < bx:ℝ⊢ b * (x - c) ^ 2 * 2 = 2 * b * (x - c) ^ 2b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume ← Complex.ofReal_pow,b:ℝc:ℝhb:0 < bx:ℝ⊢ b * (↑((x - c) ^ 2)).re * 2 = 2 * b * (x - c) ^ 2b:ℝc:ℝhb:0 < bx:ℝ⊢ b * (x - c) ^ 2 * 2 = 2 * b * (x - c) ^ 2b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume Complex.ofReal_reb:ℝc:ℝhb:0 < bx:ℝ⊢ b * (x - c) ^ 2 * 2 = 2 * b * (x - c) ^ 2b:ℝc:ℝhb:0 < bx:ℝ⊢ b * (x - c) ^ 2 * 2 = 2 * b * (x - c) ^ 2b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume]b:ℝc:ℝhb:0 < bx:ℝ⊢ b * (x - c) ^ 2 * 2 = 2 * b * (x - c) ^ 2b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume
    ringb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volumeb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) volume
  rw [h1b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)) volumeb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)) volume]b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)) volume
  apply Integrable.comp_sub_right (f := fun x => Real.exp (- (2 * b) * x ^ 2))b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ Integrable (fun x => Real.exp (-(2 * b) * x ^ 2)) volume
  apply integrable_exp_neg_mul_sqb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (-(b * ((↑x - ↑c) ^ 2).re)) ^ 2) = fun y => (fun x => Real.exp (-(2 * b) * x ^ 2)) (y - c)⊢ 0 < 2 * b
  simp_allAll goals completed! 🐙

lemma exp_mul_gaussian_integrable (b c : ℝ) (hb : 0 < b) :
    MeasureTheory.Integrable (fun x => Real.exp (c * x) * Real.exp (- b * x ^ 2)) := byb:ℝc:ℝhb:0 < b⊢ Integrable (fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) volume
  have h1 : (fun x => Real.exp (c * x) * Real.exp (- b * x ^ 2))
      = (fun x => Real.exp (c^2 /(4 * b)) * Real.exp (- b * (x - c/(2 * b)) ^ 2)) := by
    funext xb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (c * x) * Real.exp (-b * x ^ 2) = Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) volume
    rw [← Real.exp_add,b:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (c * x + -b * x ^ 2) = Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)b:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (c * x + -b * x ^ 2) = Real.exp (c ^ 2 / (4 * b) + -b * (x - c / (2 * b)) ^ 2)b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) volume ← Real.exp_addb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (c * x + -b * x ^ 2) = Real.exp (c ^ 2 / (4 * b) + -b * (x - c / (2 * b)) ^ 2)b:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (c * x + -b * x ^ 2) = Real.exp (c ^ 2 / (4 * b) + -b * (x - c / (2 * b)) ^ 2)b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) volume]b:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (c * x + -b * x ^ 2) = Real.exp (c ^ 2 / (4 * b) + -b * (x - c / (2 * b)) ^ 2)b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) volume
    congr 1b:ℝc:ℝhb:0 < bx:ℝ⊢ c * x + -b * x ^ 2 = c ^ 2 / (4 * b) + -b * (x - c / (2 * b)) ^ 2b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) volume
    field_simpb:ℝc:ℝhb:0 < bx:ℝ⊢ x * b * (c + -(x * b)) * 4 * 2 ^ 2 = c ^ 2 * 2 ^ 2 + -(4 * (x * b * 2 - c) ^ 2)b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) volume
    ringb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) volumeb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) volume
  rw [h1b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)) volumeb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)) volume]b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)) volume
  apply MeasureTheory.Integrable.const_mulb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (-b * (x - c / (2 * b)) ^ 2)) volume
  apply Integrable.comp_sub_right (f := (fun x => Real.exp (- b * x ^ 2)))b:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)⊢ Integrable (fun x => Real.exp (-b * x ^ 2)) volume
  exact integrable_exp_neg_mul_sq hbAll goals completed! 🐙

lemma exp_abs_mul_gaussian_integrable (b c : ℝ) (hb : 0 < b) :
    MeasureTheory.Integrable (fun x => Real.exp (|c * x|) * Real.exp (- b * x ^ 2)) := byb:ℝc:ℝhb:0 < b⊢ Integrable (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) volume
  rw [← MeasureTheory.integrableOn_univb:ℝc:ℝhb:0 < b⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) Set.univ volumeb:ℝc:ℝhb:0 < b⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) Set.univ volume]b:ℝc:ℝhb:0 < b⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) Set.univ volume
  have h1 : Set.univ (α := ℝ) = (Set.Iic 0) ∪ Set.Ici 0 := (Set.Iic_union_Ici).symmb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) Set.univ volume
  rw [h1b:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) (Set.Iic 0 ∪ Set.Ici 0) volumeb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) (Set.Iic 0 ∪ Set.Ici 0) volume]b:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) (Set.Iic 0 ∪ Set.Ici 0) volume
  apply MeasureTheory.IntegrableOn.unionhsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) (Set.Iic 0) volumehtb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) (Set.Ici 0) volume
  ·hsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) (Set.Iic 0) volume let g := fun x => Real.exp ((- |c|) * x) * Real.exp (- b * x ^ 2)hsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) (Set.Iic 0) volume
    rw [integrableOn_congr_fun (g := g) _ measurableSet_Iichsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Iic 0) volumeb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) g (Set.Iic 0)hsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Iic 0) volumeb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) g (Set.Iic 0)]hsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Iic 0) volumeb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) g (Set.Iic 0)
    ·hsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Iic 0) volume apply MeasureTheory.IntegrableOn.left_of_union (t := Set.Ici 0)hsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Iic 0 ∪ Set.Ici 0) volume
      rw [← h1,hsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn g Set.univ volumehsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ Integrable g volume MeasureTheory.integrableOn_univhsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ Integrable g volumehsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ Integrable g volume]hsb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ Integrable g volume
      exact exp_mul_gaussian_integrable b (- |c|) hbAll goals completed! 🐙
    ·b:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) g (Set.Iic 0) intro x hxb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:x ∈ Set.Iic 0⊢ (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) x = g x
      simp only [Set.mem_Iic] at hxb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) x = g x
      simp only [neg_mul, mul_eq_mul_right_iff, Real.exp_eq_exp, Real.exp_ne_zero, or_false, g]b:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c * x| = -(|c| * x)
      rw [abs_mul,b:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c| * |x| = -(|c| * x)b:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c| * -x = -(|c| * x) abs_of_nonpos hxb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c| * -x = -(|c| * x)b:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c| * -x = -(|c| * x)]b:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c| * -x = -(|c| * x)
      ringAll goals completed! 🐙
  ·htb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) (Set.Ici 0) volume let g := fun x => Real.exp (|c| * x) * Real.exp (- b * x ^ 2)htb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) (Set.Ici 0) volume
    rw [integrableOn_congr_fun (g := g) _ measurableSet_Icihtb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Ici 0) volumeb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) g (Set.Ici 0)htb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Ici 0) volumeb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) g (Set.Ici 0)]htb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Ici 0) volumeb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) g (Set.Ici 0)
    ·htb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Ici 0) volume apply MeasureTheory.IntegrableOn.right_of_union (s := Set.Iic 0)htb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Iic 0 ∪ Set.Ici 0) volume
      rw [← h1,htb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ IntegrableOn g Set.univ volumehtb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ Integrable g volume MeasureTheory.integrableOn_univhtb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ Integrable g volumehtb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ Integrable g volume]htb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ Integrable g volume
      exact exp_mul_gaussian_integrable b (|c|) hbAll goals completed! 🐙
    ·b:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) g (Set.Ici 0) intro x hxb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:x ∈ Set.Ici 0⊢ (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) x = g x
      simp only [Set.mem_Ici] at hxb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:0 ≤ x⊢ (fun x => Real.exp |c * x| * Real.exp (-b * x ^ 2)) x = g x
      simp only [neg_mul, mul_eq_mul_right_iff, Real.exp_eq_exp, Real.exp_ne_zero, or_false, g]b:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:0 ≤ x⊢ |c * x| = |c| * x
      rw [abs_mul,b:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:0 ≤ x⊢ |c| * |x| = |c| * xAll goals completed! 🐙 abs_of_nonneg hxb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * Real.exp (-b * x ^ 2)x:ℝhx:0 ≤ x⊢ |c| * x = |c| * xAll goals completed! 🐙]All goals completed! 🐙

lemma mul_gaussian_mem_Lp_one (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) :
    MeasureTheory.MemLp (fun x => f x * Real.exp (- b * (x - c) ^ 2)) 1 volume := byf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ MemLp (fun x => f x * ↑(Real.exp (-b * (x - c) ^ 2))) 1 volume
  refine memLp_one_iff_integrable.mpr ?_f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ Integrable (fun x => f x * ↑(Real.exp (-b * (x - c) ^ 2))) volume
  let g : HilbertSpace := mk (gaussian_memHS c hb)f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯⊢ Integrable (fun x => f x * ↑(Real.exp (-b * (x - c) ^ 2))) volume
  refine (integrable_congr ?_).mp (MeasureTheory.L2.integrable_inner (𝕜 := ℂ) g (mk hf))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯⊢ (fun x => inner ℂ (↑↑g x) (↑↑(mk hf) x)) =ᵐ[volume] fun x => f x * ↑(Real.exp (-b * (x - c) ^ 2))
  simp only [RCLike.inner_apply, neg_mul, Complex.ofReal_exp, Complex.ofReal_neg,
    Complex.ofReal_mul, Complex.ofReal_pow, Complex.ofReal_sub]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯⊢ (fun x => ↑↑(mk hf) x * (starRingEnd ℂ) (↑↑g x)) =ᵐ[volume] fun x => f x * Complex.exp (-(↑b * (↑x - ↑c) ^ 2))
  refine Filter.EventuallyEq.mul (coe_mk_ae hf) ?_f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯⊢ (fun x => (starRingEnd ℂ) (↑↑g x)) =ᵐ[volume] fun x => Complex.exp (-(↑b * (↑x - ↑c) ^ 2))
  trans (fun x => (starRingEnd ℂ) (Real.exp (- b * (x - c) ^2)))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯⊢ (fun x => (starRingEnd ℂ) (↑↑g x)) =ᵐ[volume] fun x => (starRingEnd ℂ) ↑(Real.exp (-b * (x - c) ^ 2))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯⊢ (fun x => (starRingEnd ℂ) ↑(Real.exp (-b * (x - c) ^ 2))) =ᵐ[volume] fun x => Complex.exp (-(↑b * (↑x - ↑c) ^ 2))
  ·f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯⊢ (fun x => (starRingEnd ℂ) (↑↑g x)) =ᵐ[volume] fun x => (starRingEnd ℂ) ↑(Real.exp (-b * (x - c) ^ 2)) apply Filter.EventuallyEq.fun_compf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯⊢ ↑↑g =ᵐ[volume] fun x => ↑(Real.exp (-b * (x - c) ^ 2))
    simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_neg, Complex.ofReal_mul,
      Complex.ofReal_pow, Complex.ofReal_sub, g]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯⊢ ↑↑(mk ⋯) =ᵐ[volume] fun x => Complex.exp (-(↑b * (↑x - ↑c) ^ 2))
    exact AEEqFun.coeFn_mk ..All goals completed! 🐙
  ·f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯⊢ (fun x => (starRingEnd ℂ) ↑(Real.exp (-b * (x - c) ^ 2))) =ᵐ[volume] fun x => Complex.exp (-(↑b * (↑x - ↑c) ^ 2)) apply Filter.EventuallyEq.of_eqf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯⊢ (fun x => (starRingEnd ℂ) ↑(Real.exp (-b * (x - c) ^ 2))) = fun x => Complex.exp (-(↑b * (↑x - ↑c) ^ 2))
    funext xf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯x:ℝ⊢ (starRingEnd ℂ) ↑(Real.exp (-b * (x - c) ^ 2)) = Complex.exp (-(↑b * (↑x - ↑c) ^ 2))
    rw [Complex.conj_ofRealf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯x:ℝ⊢ ↑(Real.exp (-b * (x - c) ^ 2)) = Complex.exp (-(↑b * (↑x - ↑c) ^ 2))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯x:ℝ⊢ ↑(Real.exp (-b * (x - c) ^ 2)) = Complex.exp (-(↑b * (↑x - ↑c) ^ 2))]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bg:↥HilbertSpace := mk ⋯x:ℝ⊢ ↑(Real.exp (-b * (x - c) ^ 2)) = Complex.exp (-(↑b * (↑x - ↑c) ^ 2))
    simpAll goals completed! 🐙

lemma mul_gaussian_mem_Lp_two (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) :
    MeasureTheory.MemLp (fun x => f x * Real.exp (- b * (x - c) ^ 2)) 2 volume := byf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ MemLp (fun x => f x * ↑(Real.exp (-b * (x - c) ^ 2))) 2 volume
  refine MeasureTheory.MemLp.mul ?_ hf (q := ⊤)f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ MemLp (fun x => ↑(Real.exp (-b * (x - c) ^ 2))) ⊤ volume
  ·f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ MemLp (fun x => ↑(Real.exp (-b * (x - c) ^ 2))) ⊤ volume apply MeasureTheory.memLp_top_of_bound (C := Real.exp (0))hff:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ AEStronglyMeasurable (fun x => ↑(Real.exp (-b * (x - c) ^ 2))) volumehfCf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ ∀ᵐ (x : ℝ), ‖↑(Real.exp (-b * (x - c) ^ 2))‖ ≤ Real.exp 0
    ·hff:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ AEStronglyMeasurable (fun x => ↑(Real.exp (-b * (x - c) ^ 2))) volume exact gaussian_aestronglyMeasurable c hbAll goals completed! 🐙
    ·hfCf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ ∀ᵐ (x : ℝ), ‖↑(Real.exp (-b * (x - c) ^ 2))‖ ≤ Real.exp 0 apply Filter.Eventually.of_forallhfCf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ ∀ (x : ℝ), ‖↑(Real.exp (-b * (x - c) ^ 2))‖ ≤ Real.exp 0
      intro xhfCf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ ‖↑(Real.exp (-b * (x - c) ^ 2))‖ ≤ Real.exp 0
      simp only [neg_mul]hfCf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ ‖↑(Real.exp (-(b * (x - c) ^ 2)))‖ ≤ Real.exp 0
      rw [Complex.norm_realhfCf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ ‖Real.exp (-(b * (x - c) ^ 2))‖ ≤ Real.exp 0hfCf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ ‖Real.exp (-(b * (x - c) ^ 2))‖ ≤ Real.exp 0]hfCf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ ‖Real.exp (-(b * (x - c) ^ 2))‖ ≤ Real.exp 0
      simp only [Real.norm_eq_abs, Real.abs_exp, Real.exp_zero, Real.exp_le_one_iff,
        Left.neg_nonpos_iff]hfCf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ 0 ≤ b * (x - c) ^ 2
      apply mul_nonneghfC.haf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ 0 ≤ bhbf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ 0 ≤ (x - c) ^ 2
      ·hfC.haf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ 0 ≤ b exact le_of_lt hbAll goals completed! 🐙
      ·hbf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ 0 ≤ (x - c) ^ 2 exact sq_nonneg (x - c)All goals completed! 🐙

lemma abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) :
    MeasureTheory.Integrable (fun x => norm (f x) * Real.exp (- b * (x - c)^2)) := byf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ Integrable (fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) volume
  have h1 : (fun x => norm (f x) * Real.exp (- b * (x - c)^2)) =
      (fun x => norm (f x * Real.exp (- b *(x - c)^2))) := by
    funext xf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ ‖f x‖ * Real.exp (-b * (x - c) ^ 2) = ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) = fun x => ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖⊢ Integrable (fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) volume
    simp only [neg_mul, Complex.ofReal_exp, Complex.ofReal_neg, Complex.ofReal_mul,
      Complex.ofReal_pow, Complex.ofReal_sub, Complex.norm_mul, Complex.norm_exp, Complex.neg_re,
      Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, zero_mul, sub_zero, mul_eq_mul_left_iff,
      Real.exp_eq_exp, neg_inj, norm_eq_zero]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ ((x - c) ^ 2 = ((↑x - ↑c) ^ 2).re ∨ b = 0) ∨ f x = 0f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) = fun x => ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖⊢ Integrable (fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) volume
    leftf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ (x - c) ^ 2 = ((↑x - ↑c) ^ 2).re ∨ b = 0f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) = fun x => ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖⊢ Integrable (fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) volume
    leftf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ (x - c) ^ 2 = ((↑x - ↑c) ^ 2).ref:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) = fun x => ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖⊢ Integrable (fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) volume
    simp [← Complex.ofReal_sub, ← Complex.ofReal_pow]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) = fun x => ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖⊢ Integrable (fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) volumef:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) = fun x => ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖⊢ Integrable (fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) volume
  rw [h1f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) = fun x => ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖⊢ Integrable (fun x => ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖) volumef:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) = fun x => ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖⊢ Integrable (fun x => ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖) volume]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => ‖f x‖ * Real.exp (-b * (x - c) ^ 2)) = fun x => ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖⊢ Integrable (fun x => ‖f x * ↑(Real.exp (-b * (x - c) ^ 2))‖) volume
  simpa using MeasureTheory.MemLp.integrable_norm_rpow (mul_gaussian_mem_Lp_one f hf b c hb)
    one_ne_zero ENNReal.one_ne_topAll goals completed! 🐙

lemma exp_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f)
    (b c : ℝ) (hb : 0 < b) : MeasureTheory.Integrable
    (fun x => Real.exp (c * x) * norm (f x) * Real.exp (- b * x ^ 2)) := byf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume
  have h1 : (fun x => Real.exp (c * x) *
    norm (f x) * Real.exp (- b * x ^ 2))
      = (fun x => Real.exp (c^2 /(4 * b)) *
      (norm (f x) * Real.exp (- b * (x - c/(2 * b)) ^ 2))) := by
    funext xf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2) =
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume
    rw [mul_comm,f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2) * (Real.exp (c * x) * ‖f x‖) =
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2) * Real.exp (c * x) * ‖f x‖ =
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume← mul_assocf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2) * Real.exp (c * x) * ‖f x‖ =
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2) * Real.exp (c * x) * ‖f x‖ =
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2) * Real.exp (c * x) * ‖f x‖ =
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume
    trans (Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2)) * norm (f x)f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2) * Real.exp (c * x) * ‖f x‖ =
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2) * ‖f x‖f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2) * ‖f x‖ =
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume
    swapf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2) * ‖f x‖ =
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2) * Real.exp (c * x) * ‖f x‖ =
  Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2) * ‖f x‖f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume
    ·f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2) * ‖f x‖ =
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume ringAll goals completed! 🐙f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume
    rw [← Real.exp_add,f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2 + c * x) * ‖f x‖ = Real.exp (c ^ 2 / (4 * b)) * Real.exp (-b * (x - c / (2 * b)) ^ 2) * ‖f x‖f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2 + c * x) * ‖f x‖ = Real.exp (c ^ 2 / (4 * b) + -b * (x - c / (2 * b)) ^ 2) * ‖f x‖f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume ← Real.exp_addf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2 + c * x) * ‖f x‖ = Real.exp (c ^ 2 / (4 * b) + -b * (x - c / (2 * b)) ^ 2) * ‖f x‖f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2 + c * x) * ‖f x‖ = Real.exp (c ^ 2 / (4 * b) + -b * (x - c / (2 * b)) ^ 2) * ‖f x‖f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2 + c * x) * ‖f x‖ = Real.exp (c ^ 2 / (4 * b) + -b * (x - c / (2 * b)) ^ 2) * ‖f x‖f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume
    congr 1e_af:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ Real.exp (-b * x ^ 2 + c * x) = Real.exp (c ^ 2 / (4 * b) + -b * (x - c / (2 * b)) ^ 2)f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume
    simp only [neg_mul, Real.exp_eq_exp]e_af:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ -(b * x ^ 2) + c * x = c ^ 2 / (4 * b) + -(b * (x - c / (2 * b)) ^ 2)f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume
    field_simpe_af:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bx:ℝ⊢ b * x * (-(b * x) + c) * 4 * 2 ^ 2 = c ^ 2 * 2 ^ 2 + -(4 * (b * x * 2 - c) ^ 2)f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume
    ringf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volumef:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) volume
  rw [h1f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))) volumef:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))) volume]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:(fun x => Real.exp (c * x) * ‖f x‖ * Real.exp (-b * x ^ 2)) = fun x =>
  Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))⊢ Integrable (fun x => Real.exp (c ^ 2 / (4 * b)) * (‖f x‖ * Real.exp (-b * (x - c / (2 * b)) ^ 2))) volume
  exact MeasureTheory.Integrable.const_mul (abs_mul_gaussian_integrable f hf b (c / (2 * b)) hb) ..All goals completed! 🐙

lemma exp_abs_mul_abs_mul_gaussian_integrable (f : ℝ → ℂ) (hf : MemHS f) (b c : ℝ) (hb : 0 < b) :
    MeasureTheory.Integrable
    (fun x => Real.exp (|c * x|) * norm (f x) * Real.exp (- b * x ^ 2)) := byf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ Integrable (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) volume
  rw [← MeasureTheory.integrableOn_univf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) Set.univ volumef:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) Set.univ volume]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < b⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) Set.univ volume
  have h1 : Set.univ (α := ℝ) = (Set.Iic 0) ∪ Set.Ici 0 := Set.Iic_union_Ici.symmf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) Set.univ volume
  rw [h1f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) (Set.Iic 0 ∪ Set.Ici 0) volumef:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) (Set.Iic 0 ∪ Set.Ici 0) volume]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) (Set.Iic 0 ∪ Set.Ici 0) volume
  apply MeasureTheory.IntegrableOn.unionhsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) (Set.Iic 0) volumehtf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) (Set.Ici 0) volume
  ·hsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) (Set.Iic 0) volume let g := fun x => Real.exp ((- |c|) * x) * norm (f x) * Real.exp (- b * x ^ 2)hsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) (Set.Iic 0) volume
    rw [integrableOn_congr_fun (g := g) _ measurableSet_Iichsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Iic 0) volumef:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) g (Set.Iic 0)hsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Iic 0) volumef:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) g (Set.Iic 0)]hsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Iic 0) volumef:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) g (Set.Iic 0)
    ·hsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Iic 0) volume apply MeasureTheory.IntegrableOn.left_of_union (t := Set.Ici 0)hsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Iic 0 ∪ Set.Ici 0) volume
      rw [← h1,hsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn g Set.univ volumehsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Integrable g volume MeasureTheory.integrableOn_univhsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Integrable g volumehsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Integrable g volume]hsf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Integrable g volume
      exact exp_mul_abs_mul_gaussian_integrable f hf b (-|c|) hbAll goals completed! 🐙
    ·f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) g (Set.Iic 0) intro x hxf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:x ∈ Set.Iic 0⊢ (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) x = g x
      simp only [Set.mem_Iic] at hxf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) x = g x
      simp only [neg_mul, mul_eq_mul_right_iff, Real.exp_eq_exp, Real.exp_ne_zero,
        or_false, g]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c * x| = -(|c| * x) ∨ ‖f x‖ = 0
      leftf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c * x| = -(|c| * x)
      rw [abs_mul,f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c| * |x| = -(|c| * x)f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c| * -x = -(|c| * x) abs_of_nonpos hxf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c| * -x = -(|c| * x)f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c| * -x = -(|c| * x)]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (-|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:x ≤ 0⊢ |c| * -x = -(|c| * x)
      ringAll goals completed! 🐙
  ·htf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) (Set.Ici 0) volume let g := fun x => Real.exp (|c| * x) * norm (f x) * Real.exp (- b * x ^ 2)htf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) (Set.Ici 0) volume
    rw [integrableOn_congr_fun (g := g) _ measurableSet_Icihtf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Ici 0) volumef:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) g (Set.Ici 0)htf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Ici 0) volumef:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) g (Set.Ici 0)]htf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Ici 0) volumef:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) g (Set.Ici 0)
    ·htf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Ici 0) volume apply MeasureTheory.IntegrableOn.right_of_union (s := Set.Iic 0)htf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn g (Set.Iic 0 ∪ Set.Ici 0) volume
      rw [← h1,htf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ IntegrableOn g Set.univ volumehtf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Integrable g volume MeasureTheory.integrableOn_univhtf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Integrable g volumehtf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Integrable g volume]htf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Integrable g volume
      exact exp_mul_abs_mul_gaussian_integrable f hf b |c| hbAll goals completed! 🐙
    ·f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)⊢ Set.EqOn (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) g (Set.Ici 0) intro x hxf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:x ∈ Set.Ici 0⊢ (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) x = g x
      simp only [Set.mem_Ici] at hxf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:0 ≤ x⊢ (fun x => Real.exp |c * x| * ‖f x‖ * Real.exp (-b * x ^ 2)) x = g x
      simp only [neg_mul, mul_eq_mul_right_iff, Real.exp_eq_exp, Real.exp_ne_zero,
        or_false, g]f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:0 ≤ x⊢ |c * x| = |c| * x ∨ ‖f x‖ = 0
      leftf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:0 ≤ x⊢ |c * x| = |c| * x
      rw [abs_mul,f:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:0 ≤ x⊢ |c| * |x| = |c| * xAll goals completed! 🐙 abs_of_nonneg hxf:ℝ → ℂhf:MemHS fb:ℝc:ℝhb:0 < bh1:Set.univ = Set.Iic 0 ∪ Set.Ici 0g:ℝ → ℝ := fun x => Real.exp (|c| * x) * ‖f x‖ * Real.exp (-b * x ^ 2)x:ℝhx:0 ≤ x⊢ |c| * x = |c| * xAll goals completed! 🐙]All goals completed! 🐙