awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ (↑(↑v : ℝ) : ℂ) ≠ 0

Tactic:
have : (v : ℂ) ≠ 0 := by simpa
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
this : (↑(↑v : ℝ) : ℂ) ≠ 0
e_z :
  -(HPow.hPow (β := ℕ) (↑μ : ℂ) 2 * 4) +
      HPow.hPow (α := ℂ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) ((↑(↑v : ℝ) : ℂ) * z + (↑μ : ℂ)) 2 =
    4 * (↑(↑v : ℝ) : ℂ) * z * ((↑μ : ℂ) * 2 + (↑(↑v : ℝ) : ℂ) * z)
⊢ -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
      HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) =
    z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2

Tactic:
simp [field]
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
this : (↑(↑v : ℝ) : ℂ) ≠ 0
⊢ -(HPow.hPow (β := ℕ) (↑μ : ℂ) 2 * 4) +
      HPow.hPow (α := ℂ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) ((↑(↑v : ℝ) : ℂ) * z + (↑μ : ℂ)) 2 =
    4 * (↑(↑v : ℝ) : ℂ) * z * ((↑μ : ℂ) * 2 + (↑(↑v : ℝ) : ℂ) * z)

Tactic:
ring
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
rw : NeZero (gaussianReal μ v)
⊢ NeZero (R := Measure ℝ) (Measure.map X p)

Tactic:
rw [hX]
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
⊢ NeZero (gaussianReal μ v)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
⊢ AEMeasurable X p

Tactic:
have hX_meas : AEMeasurable X p := aemeasurable_of_map_neZero (by rw [hX]; infer_instance)
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
hX_meas : AEMeasurable X p
rw :
  complexMGF (m := Real.measurableSpace) id (Measure.map X p) z =
    cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
rw₁ : complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
rw₂ rw₃ :
  cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2) =
    cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
⊢ complexMGF X p z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)

Tactic:
rw [← complexMGF_id_map hX_meas, hX, complexMGF_id_gaussianReal]

Premises used: ProbabilityTheory.complexMGF_id_map, ProbabilityTheory.complexMGF_id_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
rw :
  cexp ((↑t : ℂ) * I * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 / 2) =
    cexp ((↑t : ℂ) * (↑μ : ℂ) * I - (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
⊢ charFun (gaussianReal μ v) t = cexp ((↑t : ℂ) * (↑μ : ℂ) * I - (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)

Tactic:
rw [← complexMGF_id_mul_I, complexMGF_id_gaussianReal]

Premises used: ProbabilityTheory.complexMGF_id_mul_I, ProbabilityTheory.complexMGF_id_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
e_z :
  (↑t : ℂ) * I * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 / 2 =
    (↑t : ℂ) * (↑μ : ℂ) * I - (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2
⊢ cexp ((↑t : ℂ) * I * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 / 2) =
    cexp ((↑t : ℂ) * (↑μ : ℂ) * I - (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)

Tactic:
congr
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
e_z :
  (↑t : ℂ) * I * (↑μ : ℂ) + -((↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2) / 2 =
    (↑t : ℂ) * (↑μ : ℂ) * I + -((↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
⊢ (↑t : ℂ) * I * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 / 2 =
    (↑t : ℂ) * (↑μ : ℂ) * I - (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2

Tactic:
simp only [mul_pow, I_sq, mul_neg, mul_one, sub_eq_add_neg]

Premises used: sub_eq_add_neg, Complex.I_sq, mul_one, mul_pow, mul_neg
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ (↑t : ℂ) * I * (↑μ : ℂ) + -((↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2) / 2 =
    (↑t : ℂ) * (↑μ : ℂ) * I + -((↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)

Tactic:
ring_nf
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
suffices : (↑(mgf X p t) : ℂ) = (↑(rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) : ℂ)
⊢ mgf X p t = rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
suffices (mgf X p t : ℂ) = rexp (μ * t + ↑v * t ^ 2 / 2) from mod_cast this
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
rw : NeZero (gaussianReal μ v)
⊢ NeZero (R := Measure ℝ) (Measure.map X p)

Tactic:
rw [hX]
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
⊢ NeZero (gaussianReal μ v)

Tactic:
infer_instance
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
⊢ AEMeasurable X p

Tactic:
have hX_meas : AEMeasurable X p := aemeasurable_of_map_neZero (by rw [hX]; infer_instance)
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hX_meas : AEMeasurable X p
rw :
  cexp ((↑t : ℂ) * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2) =
    (↑(rexp (t * μ + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) : ℂ)
⊢ (↑(mgf X p t) : ℂ) = (↑(rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) : ℂ)

Tactic:
rw [← mgf_id_map hX_meas, ← complexMGF_ofReal, hX, complexMGF_id_gaussianReal, mul_comm μ]

Premises used: mul_comm, ProbabilityTheory.complexMGF_id_gaussianReal, ProbabilityTheory.complexMGF_ofReal, ProbabilityTheory.mgf_id_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hX_meas : AEMeasurable X p
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ :
  rexp (t * μ + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) = rexp (t * μ + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ cexp ((↑t : ℂ) * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2) =
    (↑(rexp (t * μ + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) : ℂ)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : ∀ (t : ℝ), mgf (fun (x : ℝ) ↦ x) (gaussianReal μ v) t = rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ mgf (fun (x : ℝ) ↦ x) (gaussianReal μ v) = fun (t : ℝ) ↦ rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
ext t
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
h : Measure.map (fun (x : ℝ) ↦ x) (gaussianReal μ v) = gaussianReal μ v
⊢ mgf (fun (x : ℝ) ↦ x) (gaussianReal μ v) t = rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
rw [mgf_gaussianReal]

Premises used: ProbabilityTheory.mgf_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ Measure.map (fun (x : ℝ) ↦ x) (gaussianReal μ v) = gaussianReal μ v

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ mgf id (gaussianReal μ v) = fun (t : ℝ) ↦ rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
mgf_fun_id_gaussianReal

Premises used: ProbabilityTheory.mgf_fun_id_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
rw : Real.log (mgf X p t) = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
rw₁ : Real.log (rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
rw₂ rw₃ : μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
⊢ cgf X p t = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2

Tactic:
rw [cgf, mgf_gaussianReal hX t, Real.log_exp]

Premises used: Real.log_exp, ProbabilityTheory.cgf, ProbabilityTheory.mgf_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
rw : 0 < rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ Integrable (ε := ℝ) (fun (x : ℝ) ↦ rexp (t * x)) (gaussianReal μ v)

Tactic:
rw [← mgf_pos_iff, mgf_gaussianReal (μ := μ) (v := v) (by simp)]

Premises used: ProbabilityTheory.mgf_gaussianReal, ProbabilityTheory.mgf_pos_iff
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ 0 < rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
Real.exp_pos _

Premises used: Real.exp_pos
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ 0 < rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
exact Real.exp_pos _

Premises used: Real.exp_pos
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h : ∀ (x : ℝ), x ∈ integrableExpSet id (gaussianReal μ v) ↔ Membership.mem (γ := Set ℝ) Set.univ x
⊢ integrableExpSet id (gaussianReal μ v) = Set.univ

Tactic:
ext
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
x : ℝ
⊢ x ∈ integrableExpSet id (gaussianReal μ v) ↔ Membership.mem (γ := Set ℝ) Set.univ x

Tactic:
simpa [integrableExpSet] using integrable_exp_mul_gaussianReal _

Premises used: ProbabilityTheory.integrableExpSet, ProbabilityTheory.integrable_exp_mul_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ integrableExpSet (fun (x : ℝ) ↦ x) (gaussianReal μ v) = Set.univ

Tactic:
integrableExpSet_id_gaussianReal

Premises used: ProbabilityTheory.integrableExpSet_id_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ 0 ∈ interior (integrableExpSet (fun (x : ℝ) ↦ x) (gaussianReal μ v))

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
rw :
  rexp (μ * 0 + (↑v : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) 0 2 / 2) *
      deriv (fun (t : ℝ) ↦ μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0 =
    μ
⊢ ∫ (x : ℝ), x ∂gaussianReal μ v = μ

Tactic:
rw [← deriv_mgf_zero (by simp), mgf_fun_id_gaussianReal, _root_.deriv_exp (by fun_prop)]

Premises used: deriv_exp, ProbabilityTheory.mgf_fun_id_gaussianReal, ProbabilityTheory.deriv_mgf_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
simp : deriv (fun (t : ℝ) ↦ μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0 = μ
⊢ rexp (μ * 0 + (↑v : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) 0 2 / 2) *
      deriv (fun (t : ℝ) ↦ μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0 =
    μ

Tactic:
simp only [mul_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, zero_div,
    add_zero, Real.exp_zero, one_mul]

Premises used: OfNat.ofNat_ne_zero, zero_div, ne_eq, MulZeroClass.mul_zero, Real.exp_zero, add_zero, not_false_eq_true, zero_pow, one_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (E := ℝ) (HMul.hMul μ) 0

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : ℝ) ↦ μ) 0

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : ℝ) ↦ y) 0

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
rw :
  HMul.hMul (α := ℝ) (deriv (fun (y : ℝ) ↦ μ) 0) 0 + μ * deriv (fun (y : ℝ) ↦ y) 0 +
      deriv (fun (t : ℝ) ↦ (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0 =
    μ
⊢ deriv (fun (t : ℝ) ↦ μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0 = μ

Tactic:
rw [deriv_fun_add (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]

Premises used: deriv_fun_mul, deriv_fun_add
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ HMul.hMul (α := ℝ) (deriv (fun (y : ℝ) ↦ μ) 0) 0 + μ * deriv (fun (y : ℝ) ↦ y) 0 +
      deriv (fun (t : ℝ) ↦ (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0 =
    μ

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
rw : ∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - ∫ (x : ℝ), x ∂gaussianReal μ v) 2 ∂gaussianReal μ v = (↑v : ℝ)
⊢ Var[fun (x : ℝ) ↦ x; gaussianReal μ v] = (↑v : ℝ)

Tactic:
rw [variance_eq_integral measurable_id'.aemeasurable]

Premises used: ProbabilityTheory.variance_eq_integral, Measurable.aemeasurable, measurable_id'
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
simp : ∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v = (↑v : ℝ)
⊢ ∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - ∫ (x : ℝ), x ∂gaussianReal μ v) 2 ∂gaussianReal μ v = (↑v : ℝ)

Tactic:
simp only [integral_id_gaussianReal]

Premises used: ProbabilityTheory.integral_id_gaussianReal
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ AEMeasurable (β := ℝ) (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := Real.measurableSpace) (fun (ω : ℝ) ↦ HPow.hPow (β := ℕ) ω 2)
    (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
rw rw₁ :
  Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v)
    (∫ (x : ℝ), HPow.hPow (β := ℕ) (x - μ) 2 ∂gaussianReal μ v)
⊢ Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)) fun (ω : ℝ) ↦
      HPow.hPow (β := ℕ) ω 2)

Tactic:
rw [integral_map (by fun_prop) (by fun_prop)]

Premises used: MeasureTheory.integral_map
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)) fun (ω : ℝ) ↦
      HPow.hPow (β := ℕ) ω 2)
    (∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v)

Tactic:
simp [gaussianReal_map_sub_const]

Premises used: ProbabilityTheory.gaussianReal_map_sub_const
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
rw :
  Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v)
    (∫ (x : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℕ) (fun (x : ℝ) ↦ x) 2 x ∂gaussianReal 0 v)
h : 0 ∈ interior (integrableExpSet (fun (x : ℝ) ↦ x) (gaussianReal 0 v))
⊢ ∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v = iteratedDeriv 2 (mgf (fun (x : ℝ) ↦ x) (gaussianReal 0 v)) 0

Tactic:
rw [iteratedDeriv_mgf_zero]

Premises used: ProbabilityTheory.iteratedDeriv_mgf_zero
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v)
    (∫ (x : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℕ) (fun (x : ℝ) ↦ x) 2 x ∂gaussianReal 0 v)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ 0 ∈ interior (integrableExpSet (fun (x : ℝ) ↦ x) (gaussianReal 0 v))

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
rw : deriv (𝕜 := ℝ) (deriv fun (t : ℝ) ↦ rexp (0 * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0 = (↑v : ℝ)
⊢ iteratedDeriv 2 (mgf (fun (x : ℝ) ↦ x) (gaussianReal 0 v)) 0 = (↑v : ℝ)

Tactic:
rw [mgf_fun_id_gaussianReal, iteratedDeriv_succ, iteratedDeriv_one]

Premises used: iteratedDeriv_succ, ProbabilityTheory.mgf_fun_id_gaussianReal, iteratedDeriv_one
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
simp : deriv (𝕜 := ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0 = (↑v : ℝ)
⊢ deriv (𝕜 := ℝ) (deriv fun (t : ℝ) ↦ rexp (0 * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0 = (↑v : ℝ)

Tactic:
simp only [zero_mul, zero_add]

Premises used: MulZeroClass.zero_mul, zero_add
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
h :
  ∀ (t : ℝ),
    deriv (fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) t =
      (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ Eq (α := (x : ℝ) → ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) fun (t : ℝ) ↦
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
ext t
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) t

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
h :
  rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * deriv (fun (t : ℝ) ↦ (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) t =
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ deriv (fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) t =
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
rw [_root_.deriv_exp (by fun_prop)]

Premises used: deriv_exp
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
h :
  rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * ((↑v : ℝ) * (2 * t) / 2) =
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * deriv (fun (t : ℝ) ↦ (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) t =
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
simp only [deriv_div_const, differentiableAt_const, differentiableAt_fun_id, Nat.cast_ofNat,
        DifferentiableAt.fun_pow, deriv_fun_mul, deriv_const', zero_mul, deriv_fun_pow,
        Nat.add_one_sub_one, pow_one, deriv_id'', mul_one, zero_add]

Premises used: Nat.cast_ofNat, Nat.add_one_sub_one, deriv_const', deriv_fun_mul, MulZeroClass.zero_mul, deriv_id'', DifferentiableAt.fun_pow, zero_add, pow_one, differentiableAt_fun_id, differentiableAt_const, deriv_fun_pow, mul_one, deriv_div_const
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * ((↑v : ℝ) * (2 * t) / 2) =
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
ring
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
⊢ Eq (α := (x : ℝ) → ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) fun (t : ℝ) ↦
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)

Tactic:
have : deriv (fun t ↦ rexp (v * t ^ 2 / 2)) = fun t ↦ v * t * rexp (v * t ^ 2 / 2) := by
      ext t
      rw [_root_.deriv_exp (by fun_prop)]
      simp only [deriv_div_const, differentiableAt_const, differentiableAt_fun_id, Nat.cast_ofNat,
        DifferentiableAt.fun_pow, deriv_fun_mul, deriv_const', zero_mul, deriv_fun_pow,
        Nat.add_one_sub_one, pow_one, deriv_id'', mul_one, zero_add]
      ring
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
this :
  Eq (α := (x : ℝ) → ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) fun (t : ℝ) ↦
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ DifferentiableAt ℝ (E := ℝ) (HMul.hMul (↑v : ℝ)) 0

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
this :
  Eq (α := (x : ℝ) → ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) fun (t : ℝ) ↦
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ DifferentiableAt ℝ (F := ℝ) (fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
this :
  Eq (α := (x : ℝ) → ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) fun (t : ℝ) ↦
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : ℝ) ↦ (↑v : ℝ)) 0

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
this :
  Eq (α := (x : ℝ) → ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) fun (t : ℝ) ↦
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : ℝ) ↦ y) 0

Tactic:
fun_prop
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
this :
  Eq (α := (x : ℝ) → ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) fun (t : ℝ) ↦
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
rw :
  (HMul.hMul (α := ℝ) (deriv (fun (y : ℝ) ↦ (↑v : ℝ)) 0) 0 + (↑v : ℝ) * deriv (fun (y : ℝ) ↦ y) 0) *
        rexp ((↑v : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) 0 2 / 2) +
      (↑v : ℝ) * 0 * deriv (fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0 =
    (↑v : ℝ)
⊢ deriv (𝕜 := ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0 = (↑v : ℝ)

Tactic:
rw [this, deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]

Premises used: deriv_fun_mul
-- Module: Mathlib.Probability.Distributions.Gaussian.Real
Goal:
μ : ℝ
v : ℝ≥0
this :
  Eq (α := (x : ℝ) → ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) fun (t : ℝ) ↦
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ (HMul.hMul (α := ℝ) (deriv (fun (y : ℝ) ↦ (↑v : ℝ)) 0) 0 + (↑v : ℝ) * deriv (fun (y : ℝ) ↦ y) 0) *
        rexp ((↑v : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) 0 2 / 2) +
      (↑v : ℝ) * 0 * deriv (fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0 =
    (↑v : ℝ)

Tactic:
simp