-- Mathlib/Probability/Distributions/Gaussian.lean
@[fun_prop]
lemma integrable_gaussianPDFReal (μ : ℝ) (v : ℝ≥0) :
    Integrable (gaussianPDFReal μ v)

Proof state:
μ : ℝ
v : ℝ≥0
⊢ Integrable (gaussianPDFReal μ v) ℙ

Tactic:
rw [gaussianPDFReal_def]

Result:
μ : ℝ
v : ℝ≥0
⊢ Integrable (fun x => (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

Proof state:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
⊢ Integrable g ℙ

Tactic:
suffices g = fun x ↦ (√(2 * π * v))⁻¹ * rexp (- (2 * v)⁻¹ * x ^ 2) by
  rw [this]
  refine (integrable_exp_neg_mul_sq ?_).const_mul (√(2 * π * v))⁻¹
  simp [lt_of_le_of_ne (zero_le _) (Ne.symm hv)]

Result:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
⊢ g = fun x => (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)

Proof state:
case h
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
x : ℝ
⊢ -x ^ 2 / (2 * ↑v) = -((↑v)⁻¹ * 2⁻¹ * x ^ 2) ∨ √(2 * π) = 0

Tactic:
rw [mul_comm]

Result:
case h
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
x : ℝ
⊢ -x ^ 2 / (↑v * 2) = -((↑v)⁻¹ * 2⁻¹ * x ^ 2) ∨ √(2 * π) = 0

Proof state:
case h
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
x : ℝ
⊢ g x = (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)

Tactic:
simp only [g, zero_lt_two, mul_nonneg_iff_of_pos_left, NNReal.zero_le_coe, Real.sqrt_mul',
  mul_inv_rev, NNReal.coe_mul, NNReal.coe_inv, NNReal.coe_ofNat, neg_mul, mul_eq_mul_left_iff,
  Real.exp_eq_exp, mul_eq_zero, inv_eq_zero, Real.sqrt_eq_zero, NNReal.coe_eq_zero, hv,
  false_or]

Result:
case h
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
x : ℝ
⊢ -x ^ 2 / (2 * ↑v) = -((↑v)⁻¹ * 2⁻¹ * x ^ 2) ∨ √(2 * π) = 0

Proof state:
case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ Integrable (fun x => (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

Tactic:
simp [hv]

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
⊢ g = fun x => (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)

Tactic:
ext x

Result:
case h
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
x : ℝ
⊢ g x = (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)

Proof state:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
this : g = fun x => (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)
⊢ Integrable g ℙ

Tactic:
rw [this]

Result:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
this : g = fun x => (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)
⊢ Integrable (fun x => (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)) ℙ

Proof state:
case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
hg : Integrable g ℙ
⊢ Integrable (fun x => (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

Tactic:
exact Integrable.comp_sub_right hg μ

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
⊢ Integrable (fun x => (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

Tactic:
by_cases hv : v = 0

Result:
case pos
μ : ℝ
v : ℝ≥0
hv : v = 0
⊢ Integrable (fun x => (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ Integrable (fun x => (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

Proof state:
case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
⊢ Integrable (fun x => (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

Tactic:
have hg : Integrable g := by
  suffices g = fun x ↦ (√(2 * π * v))⁻¹ * rexp (- (2 * v)⁻¹ * x ^ 2) by
    rw [this]
    refine (integrable_exp_neg_mul_sq ?_).const_mul (√(2 * π * v))⁻¹
    simp [lt_of_le_of_ne (zero_le _) (Ne.symm hv)]
  ext x
  simp only [g, zero_lt_two, mul_nonneg_iff_of_pos_left, NNReal.zero_le_coe, Real.sqrt_mul',
    mul_inv_rev, NNReal.coe_mul, NNReal.coe_inv, NNReal.coe_ofNat, neg_mul, mul_eq_mul_left_iff,
    Real.exp_eq_exp, mul_eq_zero, inv_eq_zero, Real.sqrt_eq_zero, NNReal.coe_eq_zero, hv,
    false_or]
  rw [mul_comm]
  left
  field_simp

Result:
case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
hg : Integrable g ℙ
⊢ Integrable (fun x => (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

Proof state:
case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
⊢ Integrable (fun x => (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

Tactic:
let g : ℝ → ℝ := fun x ↦ (√(2 * π * v))⁻¹ * rexp (- x ^ 2 / (2 * v))

Result:
case neg
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
⊢ Integrable (fun x => (√(2 * π * ↑v))⁻¹ * rexp (-(x - μ) ^ 2 / (2 * ↑v))) ℙ

Proof state:
case h
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
x : ℝ
⊢ -x ^ 2 / (↑v * 2) = -((↑v)⁻¹ * 2⁻¹ * x ^ 2) ∨ √(2 * π) = 0

Tactic:
left

Result:
case h.h
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
x : ℝ
⊢ -x ^ 2 / (↑v * 2) = -((↑v)⁻¹ * 2⁻¹ * x ^ 2)

Proof state:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
this : g = fun x => (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)
⊢ Integrable (fun x => (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)) ℙ

Tactic:
refine (integrable_exp_neg_mul_sq ?_).const_mul (√(2 * π * v))⁻¹

Result:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
this : g = fun x => (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)
⊢ 0 < ↑(2 * v)⁻¹

Proof state:
case h.h
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
x : ℝ
⊢ -x ^ 2 / (↑v * 2) = -((↑v)⁻¹ * 2⁻¹ * x ^ 2)

Tactic:
field_simp

Result:
no goals

Proof state:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x => (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
this : g = fun x => (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)
⊢ 0 < ↑(2 * v)⁻¹

Tactic:
simp [lt_of_le_of_ne (zero_le _) (Ne.symm hv)]

Result:
no goals