mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero : ∀ (x : ℝ), x ≠ 0 → (innerₗ ℝ) x ≠ 0
w : ℝ
h :
  ∫ (ω : Ω), cexp (↑(Multiplicative.toAdd w) * ↑(X ω) * I) ∂μ =
    ∫ (ω : Ω'), cexp (↑(Multiplicative.toAdd w) * ↑(Y ω) * I) ∂μ'
⊢ AEStronglyMeasurable (fun v ↦ cexp (↑w * ↑v * I)) (Measure.map X μ)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : ∫ (x : Ω), X x ∂μ = 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
hu : UniqueDiffOn ℝ (Set.Icc 0 t)
x✝ : ℝ
⊢ derivWithin (cgf X μ) (Set.Icc 0 t) 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
inner_ne_zero : ∀ (x : ℝ), x ≠ 0 → (innerₗ ℝ) x ≠ 0
w : ℝ
h :
  ∫ (ω : Ω), cexp (↑(Multiplicative.toAdd w) * ↑(X ω) * I) ∂μ =
    ∫ (ω : Ω'), cexp (↑(Multiplicative.toAdd w) * ↑(Y ω) * I) ∂μ'
⊢ AEStronglyMeasurable (fun v ↦ cexp (↑w * ↑v * I)) (Measure.map Y μ')

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), ∃ m v, Measure.map (⇑L) μ = gaussianReal m v
⊢ IsGaussian μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
⊢ mgf X p t = rexp (μ * t + ↑v * t ^ 2 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.MGFAnalytic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
inst✝ : IsZeroOrProbabilityMeasure μ
ht : 0 < t
hc : ∫ (x : Ω), X x ∂μ = 0
hs : Set.Icc 0 t ⊆ interior (integrableExpSet X μ)
⊢ ∃ u ∈ Set.Ioo 0 t, cgf X μ t = iteratedDeriv 2 (cgf X μ) u * t ^ 2 / 2

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
Y : Ω' → ℝ
μ' : Measure Ω'
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
hX : AEMeasurable X μ
hY : AEMeasurable Y μ'
h : complexMGF X μ = complexMGF Y μ'
⊢ Measure.map X μ = Measure.map Y μ'

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ mgf (fun x ↦ x) (gaussianReal μ v) = fun t ↦ rexp (μ * t + ↑v * t ^ 2 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
mF : MeasurableSpace F
inst✝¹ : OpensMeasurableSpace F
μ : Measure E
L : E →L[ℝ] F
inst✝ : IsGaussian μ
hL : Measurable ⇑L
L' : F →L[ℝ] ℝ
⊢ Measurable ⇑L'

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.ComplexMGF

Goal state before:
pp: μ μ' : Measure ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure μ'
h : complexMGF id μ = complexMGF id μ'
⊢ μ = μ'

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
⊢ cgf X p t = μ * t + ↑v * t ^ 2 / 2

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
t : ℝ
⊢ Measure.map (fun x ↦ x) (gaussianReal μ v) = gaussianReal μ v

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ covarianceBilin 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
μ : Measure E
h : ¬MemLp id 2 μ
⊢ covarianceBilin μ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
t : ℝ
⊢ Integrable (fun x ↦ rexp (t * x)) (gaussianReal μ v)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ integrableExpSet id (gaussianReal μ v) = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
mF : MeasurableSpace F
inst✝¹ : OpensMeasurableSpace F
μ : Measure E
L : E →L[ℝ] F
inst✝ : IsGaussian μ
hL : Measurable ⇑L
⊢ IsGaussian (Measure.map (⇑L) μ)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ 0 ∈ interior (integrableExpSet (fun x ↦ x) (gaussianReal μ v))

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
x y : E
⊢ ((covarianceBilin μ) x) y = ∫ (z : E), ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫ ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (fun t ↦ μ * t + ↑v * t ^ 2 / 2) 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
x : E
L : StrongDual ℝ E
⊢ Measure.map (⇑L) (Measure.dirac x) = gaussianReal (∫ (x : E), L x ∂Measure.dirac x) Var[⇑L; Measure.dirac x].toNNReal

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (HMul.hMul μ) 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (fun t ↦ ↑v * t ^ 2 / 2) 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
μ : Measure E
x y : E
⊢ ((covarianceBilin μ) x) y = ((covarianceBilin μ) y) x

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (fun y ↦ μ) 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ DifferentiableAt ℝ (fun y ↦ y) 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ ∫ (x : ℝ), x ∂gaussianReal μ v = μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
x : E
⊢ ((covarianceBilin μ) x) x = Var[fun u ↦ ⟪x, u⟫; μ]

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : Subsingleton E
inst✝ : IsProbabilityMeasure μ
⊢ IsGaussian μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ AEMeasurable (fun x ↦ x - μ) (gaussianReal μ v)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ AEStronglyMeasurable (fun ω ↦ ω ^ 2) (Measure.map (fun x ↦ x - μ) (gaussianReal μ v))

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
p : ℝ≥0∞
hp : p ≠ ∞
⊢ AEStronglyMeasurable id (Measure.map (⇑L) μ)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ ∫ (ω : ℝ), (ω - μ) ^ 2 ∂gaussianReal μ v = ∫ (ω : ℝ), ω ^ 2 ∂Measure.map (fun x ↦ x - μ) (gaussianReal μ v)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
p : ℝ≥0∞
hp : p ≠ ∞
⊢ AEMeasurable (⇑L) μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ ∫ (ω : ℝ), ω ^ 2 ∂Measure.map (fun x ↦ x - μ) (gaussianReal μ v) = ∫ (ω : ℝ), ω ^ 2 ∂gaussianReal 0 v

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
x y : E
⊢ ((covarianceBilin μ) x) y = cov[fun u ↦ ⟪x, u⟫, fun u ↦ ⟪y, u⟫; μ]

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ ∫ (ω : ℝ), ω ^ 2 ∂gaussianReal 0 v = iteratedDeriv 2 (mgf (fun x ↦ x) (gaussianReal 0 v)) 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp (⇑L) p μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
t : ℝ
⊢ DifferentiableAt ℝ (fun t ↦ ↑v * t ^ 2 / 2) t

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ 1 ≠ ∞

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
this : (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)
⊢ DifferentiableAt ℝ (HMul.hMul ↑v) 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
this : (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)
⊢ DifferentiableAt ℝ (fun t ↦ rexp (↑v * t ^ 2 / 2)) 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ Integrable (⇑L) μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case pos
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
⊢ x * y * Var[fun x ↦ x; μ] = x * y * Var[id; μ]

Tactic:
Function.id_def

Goal state after:
case pos
μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
h : MemLp id 2 μ
⊢ x * y * Var[fun x ↦ x; μ] = x * y * Var[fun x ↦ x; μ]
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x y : ℝ
⊢ ((covarianceBilin μ) x) y = x * y * Var[id; μ]

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
this : (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)
⊢ DifferentiableAt ℝ (fun y ↦ ↑v) 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
L : E →L[ℝ] F
⊢ Measurable ⇑L

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: μ : Measure ℝ
inst✝ : IsFiniteMeasure μ
x : ℝ
⊢ ((covarianceBilin μ) x) x = x ^ 2 * Var[id; μ]

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
μ : Measure E
x : E
⊢ 0 ≤ ((covarianceBilin μ) x) x

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
this : (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)
⊢ DifferentiableAt ℝ (fun y ↦ y) 0

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ iteratedDeriv 2 (mgf (fun x ↦ x) (gaussianReal 0 v)) 0 = ↑v

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:

Tactic:
∫ ω, (ω - μ) ^ 2 ∂gaussianReal μ v
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal μ v).map (fun x ↦ x - μ) := by
    rw [integral_map (by fun_prop) (by fun_prop)]
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal 0 v) := by simp [gaussianReal_map_sub_const]
  _ = iteratedDeriv 2 (mgf (fun x ↦ x) (gaussianReal 0 v)) 0 := by
    rw [iteratedDeriv_mgf_zero] <;> simp
  _ = v := by
    rw [mgf_fun_id_gaussianReal, iteratedDeriv_succ, iteratedDeriv_one]
    simp only [zero_mul, zero_add]
    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
    rw [this, deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]
    simp

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
μ : Measure E
L : E ≃L[ℝ] F
h : IsGaussian (Measure.map (⇑L) μ)
this : μ = Measure.map (⇑L.symm) (Measure.map (⇑L) μ)
⊢ IsGaussian μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
⊢ Var[fun x ↦ x; gaussianReal μ v] = ↑v

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
μ : Measure E
L : E ≃L[ℝ] F
h : IsGaussian (Measure.map (⇑L) μ)
⊢ Measurable ⇑L.symm

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v p : ℝ≥0
⊢ 0 ∈ interior (integrableExpSet id (gaussianReal μ v))

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
μ : Measure E
L : E ≃L[ℝ] F
h : IsGaussian (Measure.map (⇑L) μ)
⊢ Measurable ⇑L

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp id p (gaussianReal μ v)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
μ : Measure E
L : E ≃L[ℝ] F
⊢ IsGaussian (Measure.map (⇑L) μ) ↔ IsGaussian μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ charFunDual μ L = charFun (Measure.map (⇑L) μ) 1

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
⊢ μ₁ = μ₂ ∧ v₁ = v₂ → gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
⊢ μ₁ = μ₂ ∧ v₁ = v₂ → gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂

Tactic:
by rintro ⟨rfl, rfl⟩; rfl

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ charFun (Measure.map (⇑L) μ) 1 = charFun (gaussianReal (∫ (x : E), L x ∂μ) Var[⇑L; μ].toNNReal) 1

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
this : ↑v₁ = ↑v₂
⊢ v₁ = v₂

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
⊢ gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂ ↔ μ₁ = μ₂ ∧ v₁ = v₂

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ 1 ≤ 2

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ ⇑L = fun x ↦ L 1 * x

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ charFun (gaussianReal (∫ (x : E), L x ∂μ) Var[⇑L; μ].toNNReal) 1 = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Measure.map (⇑L) (gaussianReal μ v) = gaussianReal (L μ) ((L 1 ^ 2).toNNReal * v)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ AEMeasurable (⇑L) (gaussianReal μ v)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ AEStronglyMeasurable (fun x ↦ x) (Measure.map (⇑L) (gaussianReal μ v))

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ ∫ (x : ℝ), L x ∂gaussianReal μ v = ∫ (x : ℝ), x ∂Measure.map (⇑L) (gaussianReal μ v)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ ∫ (x : ℝ), L x ∂gaussianReal μ v = L μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Var[⇑L; gaussianReal μ v] = ↑(L 1 ^ 2).toNNReal * ↑v

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
⊢ gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂ = gaussianReal (m₁ + m₂) (v₁ + v₂)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEStronglyMeasurable id (Measure.map (⇑L) μ)

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ AEMeasurable (⇑L) μ

Tactic:
by

Goal state after:
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: E : Type u_1
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : InnerProductSpace ℝ E
inst✝⁹ : MeasurableSpace E
inst✝⁸ : BorelSpace E
μ : Measure E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace ℝ F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : BorelSpace F
inst✝³ : SecondCountableTopology F
inst✝² : CompleteSpace F
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
h : MemLp id 2 μ
L : E →L[ℝ] F
u v : F
⊢ ((covarianceBilin (Measure.map (⇑L) μ)) u) v =
    ((covarianceBilin μ) ((ContinuousLinearMap.adjoint L) u)) ((ContinuousLinearMap.adjoint L) v)

Tactic:
by

Goal state after: