mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ MemLp (⇑L) 1 μ

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ MemLp (⇑L) 1 μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

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

Tactic:
]

Goal state after:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ rexp (↑v * t ^ 2 / 2) * deriv (fun t ↦ ↑v * t ^ 2 / 2) t = ↑v * t * rexp (↑v * t ^ 2 / 2)
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[fun x ↦ x; μ]

Tactic:
]

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

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

Tactic:
]

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)
⊢ (deriv (fun y ↦ ↑v) 0 * 0 + ↑v * deriv (fun y ↦ y) 0) * rexp (↑v * 0 ^ 2 / 2) +
      ↑v * 0 * deriv (fun t ↦ rexp (↑v * t ^ 2 / 2)) 0 =
    ↑v

Tactic:
]

Goal state after:
μ : ℝ
v : ℝ≥0
this : (deriv fun t ↦ rexp (↑v * t ^ 2 / 2)) = fun t ↦ ↑v * t * rexp (↑v * t ^ 2 / 2)
⊢ (deriv (fun y ↦ ↑v) 0 * 0 + ↑v * deriv (fun y ↦ y) 0) * rexp (↑v * 0 ^ 2 / 2) +
      ↑v * 0 * deriv (fun t ↦ rexp (↑v * t ^ 2 / 2)) 0 =
    ↑v
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 (Measure.map (⇑L.symm) (Measure.map (⇑L) μ))

Tactic:
]

Goal state after:
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 (Measure.map (⇑L.symm) (Measure.map (⇑L) μ))
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
⊢ ∫ (z : F),
      ⟪u, z - ∫ (x : F), id x ∂Measure.map (⇑L) μ⟫ * ⟪v, z - ∫ (x : F), id x ∂Measure.map (⇑L) μ⟫ ∂Measure.map (⇑L) μ =
    ∫ (z : E),
      ⟪(ContinuousLinearMap.adjoint L) u, z - ∫ (x : E), id x ∂μ⟫ *
        ⟪(ContinuousLinearMap.adjoint L) v, z - ∫ (x : E), id x ∂μ⟫ ∂μ

pp: case h
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
⊢ MemLp id 2 (Measure.map (⇑L) μ)

Tactic:
]

Goal state after:
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
⊢ ∫ (z : F),
      ⟪u, z - ∫ (x : F), id x ∂Measure.map (⇑L) μ⟫ * ⟪v, z - ∫ (x : F), id x ∂Measure.map (⇑L) μ⟫ ∂Measure.map (⇑L) μ =
    ∫ (z : E),
      ⟪(ContinuousLinearMap.adjoint L) u, z - ∫ (x : E), id x ∂μ⟫ *
        ⟪(ContinuousLinearMap.adjoint L) v, z - ∫ (x : E), id x ∂μ⟫ ∂μ

case h
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
⊢ MemLp id 2 (Measure.map (⇑L) μ)
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) μ)
⊢ μ = Measure.map (⇑L.symm ∘ ⇑L) μ

Tactic:
]

Goal state after:
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) μ)
⊢ μ = Measure.map (⇑L.symm ∘ ⇑L) μ
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 (Measure.map (⇑L) μ) 1

Tactic:
]

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 =
    charFun (gaussianReal (∫ (x : E), L x ∂μ) Var[⇑L; μ].toNNReal) 1

Tactic:
]

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
⊢ cexp (↑1 * ↑(∫ (x : E), L x ∂μ) * I - ↑↑Var[⇑L; μ].toNNReal * ↑1 ^ 2 / 2) =
    cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ cexp (↑1 * ↑(∫ (x : E), L x ∂μ) * I - ↑↑Var[⇑L; μ].toNNReal * ↑1 ^ 2 / 2) =
    cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Real

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

Tactic:
]

Goal state after:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
⊢ ∫ (x : ℝ), x ∂gaussianReal μ₂ v₂ = ∫ (x : ℝ), x ∂gaussianReal μ₂ v₂ ∧ v₁ = v₂
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ ↑(∫ (x : E), L x ∂μ) = ↑(∫ (x : E), L x ∂μ)

Tactic:
]

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

Goal state before:
pp: μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
⊢ Var[id; gaussianReal μ₂ v₂] = Var[id; gaussianReal μ₂ v₂]

Tactic:
]

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

Goal state before:
pp: μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : ⇑L = fun x ↦ L 1 * x
⊢ gaussianReal (L 1 * μ) (NNReal.mk (L 1 ^ 2) ⋯ * v) =
    gaussianReal ((fun x ↦ L 1 * x) μ) (((fun x ↦ L 1 * x) 1 ^ 2).toNNReal * v)

Tactic:
]

Goal state after:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : ⇑L = fun x ↦ L 1 * x
⊢ gaussianReal (L 1 * μ) (NNReal.mk (L 1 ^ 2) ⋯ * v) =
    gaussianReal ((fun x ↦ L 1 * x) μ) (((fun x ↦ L 1 * x) 1 ^ 2).toNNReal * v)
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✝ : IsFiniteMeasure μ
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
L : StrongDual ℝ E
u : ℝ
⊢ cexp ((∫ (x : E), ↑((u • L) x) ∂μ) * I - ↑Var[⇑(u • L); μ] / 2) =
    cexp (↑u * ↑(∫ (x : E), L x ∂μ) * I - ↑↑Var[⇑L; μ].toNNReal * ↑u ^ 2 / 2)

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
L : StrongDual ℝ E
u : ℝ
⊢ cexp ((∫ (x : E), ↑((u • L) x) ∂μ) * I - ↑Var[⇑(u • L); μ] / 2) =
    cexp (↑u * ↑(∫ (x : E), L x ∂μ) * I - ↑↑Var[⇑L; μ].toNNReal * ↑u ^ 2 / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Real

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

Tactic:
]

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

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

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

Tactic:
]

Goal state after:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ ↑((L 1 ^ 2).toNNReal * v) = ↑(L 1 ^ 2).toNNReal * ↑v

μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ AEMeasurable (⇑L) (gaussianReal μ v)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
⊢ cexp (↑t * ↑m₁ * Complex.I - ↑↑v₁ * ↑t ^ 2 / 2 + (↑t * ↑m₂ * Complex.I - ↑↑v₂ * ↑t ^ 2 / 2)) =
    cexp (↑t * ↑(m₁ + m₂) * Complex.I - ↑↑(v₁ + v₂) * ↑t ^ 2 / 2)

Tactic:
]

Goal state after:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
⊢ cexp (↑t * ↑m₁ * Complex.I - ↑↑v₁ * ↑t ^ 2 / 2 + (↑t * ↑m₂ * Complex.I - ↑↑v₂ * ↑t ^ 2 / 2)) =
    cexp (↑t * ↑(m₁ + m₂) * Complex.I - ↑↑(v₁ + v₂) * ↑t ^ 2 / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

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

Tactic:
]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
⊢ MemLp.toLp (⇑u + ⇑v) ⋯ = MemLp.toLp ⇑u ⋯ + MemLp.toLp ⇑v ⋯

Tactic:
MemLp.toLp_add

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
⊢ MemLp.toLp ⇑u ?hf + MemLp.toLp ⇑v ?hg = MemLp.toLp ⇑u ⋯ + MemLp.toLp ⇑v ⋯

case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
⊢ MemLp (⇑u) p μ

case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
⊢ MemLp (⇑v) p μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
⊢ MemLp.toLp ⇑u ?hf + MemLp.toLp ⇑v ?hg = MemLp.toLp ⇑u ⋯ + MemLp.toLp ⇑v ⋯

pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
⊢ MemLp (⇑u) p μ

pp: case hg
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
⊢ MemLp (⇑v) p μ

Tactic:
]

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ gaussianReal (m₁ + m₂) (v₁ + v₂) = gaussianReal (m₁ + m₂) (v₁ + v₂)

pp: case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ AEMeasurable X P

pp: case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ AEMeasurable Y P

pp: case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (Measure.map X P)

pp: case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (Measure.map Y P)

Tactic:
]

Goal state after:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ AEMeasurable X P

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ AEMeasurable Y P

case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (Measure.map X P)

case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (Measure.map Y P)
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ c • MemLp.toLp ⇑L ?hf = id c • MemLp.toLp ⇑L ⋯

pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ MemLp (⇑L) p μ

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ c • MemLp.toLp ⇑L ?hf = id c • MemLp.toLp ⇑L ⋯

case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ MemLp (⇑L) p μ
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
L : StrongDual ℝ E
u : ℝ
⊢ ↑Var[⇑(u • L); μ] = ↑Var[fun ω ↦ u * L ω; μ]

Tactic:
]

Goal state after:
case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
L : StrongDual ℝ E
u : ℝ
⊢ ↑Var[⇑(u • L); μ] = ↑Var[fun ω ↦ u * L ω; μ]
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case pos
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
⊢ ∫ (x_1 : E),
      ⟪x, c + x_1 - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ *
        ⟪y, c + x_1 - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ ∂μ =
    ∫ (z : E), ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫ ∂μ

Tactic:
]

Goal state after:
case pos
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
⊢ ∫ (x_1 : E),
      ⟪x, c + x_1 - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ *
        ⟪y, c + x_1 - ∫ (x : E), id x ∂Measure.map (fun x ↦ c + x) μ⟫ ∂μ =
    ∫ (z : E), ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫ ∂μ
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case pos.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ ⟪x, c + z - ∫ (x : E), id (c + x) ∂μ⟫ * ⟪y, c + z - ∫ (x : E), id (c + x) ∂μ⟫ =
    ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫

Tactic:
]

Goal state after:
case pos.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ ⟪x, c + z - ∫ (x : E), id (c + x) ∂μ⟫ * ⟪y, c + z - ∫ (x : E), id (c + x) ∂μ⟫ =
    ⟪x, z - ∫ (x : E), id x ∂μ⟫ * ⟪y, z - ∫ (x : E), id x ∂μ⟫
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₁ v₁)

Tactic:
]

Goal state after:
case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₁ v₁)
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case pos.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ ⟪x, c + z - (∫ (a : E), c ∂μ + ∫ (a : E), a ∂μ)⟫ * ⟪y, c + z - (∫ (a : E), c ∂μ + ∫ (a : E), a ∂μ)⟫ =
    ⟪x, z - ∫ (x : E), x ∂μ⟫ * ⟪y, z - ∫ (x : E), x ∂μ⟫

pp: case pos.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ Integrable (fun x ↦ x) μ

Tactic:
]

Goal state after:
case pos.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ ⟪x, c + z - (∫ (a : E), c ∂μ + ∫ (a : E), a ∂μ)⟫ * ⟪y, c + z - (∫ (a : E), c ∂μ + ∫ (a : E), a ∂μ)⟫ =
    ⟪x, z - ∫ (x : E), x ∂μ⟫ * ⟪y, z - ∫ (x : E), x ∂μ⟫

case pos.e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : MemLp id 2 μ
x y : E
h_Lp : MemLp id 2 (Measure.map (fun x ↦ c + x) μ)
z : E
⊢ Integrable (fun x ↦ x) μ
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
t : E
⊢ cexp ((∫ (x : E), ↑(((toDualMap ℝ E) t) x) ∂μ) * I - ↑Var[⇑((toDualMap ℝ E) t); μ] / 2) =
    cexp ((∫ (x : E), ↑((fun x ↦ ⟪t, x⟫) x) ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)

Tactic:
]

Goal state after:
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
t : E
⊢ cexp ((∫ (x : E), ↑(((toDualMap ℝ E) t) x) ∂μ) * I - ↑Var[⇑((toDualMap ℝ E) t); μ] / 2) =
    cexp ((∫ (x : E), ↑((fun x ↦ ⟪t, x⟫) x) ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₂ v₂)

Tactic:
]

Goal state after:
case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₂ v₂)
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
x✝¹ x✝ : E
⊢ (0 x✝¹) x✝ = (0 x✝¹) x✝

pp: case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
x✝¹ x✝ : E
⊢ ¬MemLp id 2 (Measure.map (fun x ↦ c + x) μ)

Tactic:
]

Goal state after:
case neg
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c : E
h : ¬MemLp id 2 μ
x✝¹ x✝ : E
⊢ ¬MemLp id 2 (Measure.map (fun x ↦ c + x) μ)