mathlib-initiative/mathlib-tactics huggingface dataset:
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:
this

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 ∂μ⟫ ∂μ

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 ∂μ⟫ ∂μ
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
⊢ ∫ (x : E), ⟪u, L x - L (∫ (x : E), x ∂μ)⟫ * ⟪v, L x - L (∫ (x : E), x ∂μ)⟫ ∂μ =
    ∫ (z : E),
      ⟪(ContinuousLinearMap.adjoint L) u, z - ∫ (x : E), x ∂μ⟫ *
        ⟪(ContinuousLinearMap.adjoint L) v, z - ∫ (x : E), x ∂μ⟫ ∂μ

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
⊢ ∫ (x : E), ⟪u, L x - L (∫ (x : E), x ∂μ)⟫ * ⟪v, L x - L (∫ (x : E), x ∂μ)⟫ ∂μ =
    ∫ (z : E),
      ⟪(ContinuousLinearMap.adjoint L) u, z - ∫ (x : E), x ∂μ⟫ *
        ⟪(ContinuousLinearMap.adjoint L) v, z - ∫ (x : E), x ∂μ⟫ ∂μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

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

Tactic:
[

Goal state after:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
t : ℝ
⊢ charFun (gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂) t = charFun (gaussianReal (m₁ + m₂) (v₁ + v₂)) t
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₁ v₁ ∗ Measure.map Y P = 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:
hY,

Goal state after:
Ω : 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₁ v₁ ∗ gaussianReal m₂ v₂ = gaussianReal (m₁ + m₂) (v₁ + v₂)

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.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✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
⊢ IsGaussian μ ↔ ∀ (t : E), charFun μ t = cexp ((∫ (x : E), ↑⟪t, 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✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
⊢ IsGaussian μ ↔ ∀ (t : E), charFun μ t = cexp ((∫ (x : E), ↑⟪t, x⟫ ∂μ) * I - ↑Var[fun x ↦ ⟪t, x⟫; μ] / 2)
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[fun ω ↦ ⟪∑ i, ⟪(basisFun ι ℝ) i, x⟫ • (basisFun ι ℝ) i, toLp 2 fun x ↦ X x ω⟫, fun ω ↦
      ⟪∑ i, ⟪(basisFun ι ℝ) i, y⟫ • (basisFun ι ℝ) i, toLp 2 fun x ↦ X x ω⟫; μ] =
    ∑ x_1, ∑ x_2, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ]

Tactic:
[

Goal state after:
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
x y : EuclideanSpace ℝ ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[fun ω ↦ ⟪∑ i, ⟪(basisFun ι ℝ) i, x⟫ • (basisFun ι ℝ) i, toLp 2 fun x ↦ X x ω⟫, fun ω ↦
      ⟪∑ i, ⟪(basisFun ι ℝ) i, y⟫ • (basisFun ι ℝ) i, toLp 2 fun x ↦ X x ω⟫; μ] =
    ∑ x_1, ∑ x_2, x.ofLp x_1 * y.ofLp x_2 * cov[X x_1, X x_2; μ]
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
hμ : MemLp id 2 μ
x y : E
⊢ ∫ (x_1 : E), ⟪y, ⟪x, x_1⟫ • x_1⟫ ∂μ =
    (((uncenteredCovarianceBilinDual μ).bilinearComp (toDualMap ℝ E).toContinuousLinearMap
          (toDualMap ℝ E).toContinuousLinearMap)
        x)
      y

Tactic:
[

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
⊢ ∫ (x_1 : E), ⟪y, ⟪x, x_1⟫ • x_1⟫ ∂μ =
    (((uncenteredCovarianceBilinDual μ).bilinearComp (toDualMap ℝ E).toContinuousLinearMap
          (toDualMap ℝ E).toContinuousLinearMap)
        x)
      y
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 μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ c + x) μ)

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
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ c + x) μ)
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: case pos.refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
⊢ ⟪↑(covarianceOperator μ) x, y⟫ = ⟪x, ↑(covarianceOperator μ) y⟫

Tactic:
[

Goal state after:
case pos.refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : CompleteSpace E
hμ : MemLp id 2 μ
x y : E
⊢ ⟪↑(covarianceOperator μ) x, y⟫ = ⟪x, ↑(covarianceOperator μ) y⟫
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 μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ x - c) μ)

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
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ x - c) μ)
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 μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ c - x) μ)

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
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ c - x) μ)
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
⊢ charFunDual (Measure.map (⇑(ContinuousLinearMap.rotation θ)) (μ.prod μ)) L = charFunDual (μ.prod μ) L

Tactic:
[

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
⊢ charFunDual (Measure.map (⇑(ContinuousLinearMap.rotation θ)) (μ.prod μ)) L = charFunDual (μ.prod μ) L
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: case e_a.e_a
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 μ
inst✝¹ : SecondCountableTopologyEither E F
ν : Measure F
inst✝ : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inl ℝ E F
hL₁ : L₁ = L ∘SL ContinuousLinearMap.inl ℝ E F
L₂ : F →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inr ℝ E F
hL₂ : L₂ = L ∘SL ContinuousLinearMap.inr ℝ E F
⊢ ∫ (x : E), ↑(L₁ x) ∂μ + ∫ (x : F), ↑(L₂ x) ∂ν = ∫ (x : E × F), ↑(L x) ∂μ.prod ν

Tactic:
[

Goal state after:
case e_a.e_a
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 μ
inst✝¹ : SecondCountableTopologyEither E F
ν : Measure F
inst✝ : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inl ℝ E F
hL₁ : L₁ = L ∘SL ContinuousLinearMap.inl ℝ E F
L₂ : F →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inr ℝ E F
hL₂ : L₂ = L ∘SL ContinuousLinearMap.inr ℝ E F
⊢ ∫ (x : E), ↑(L₁ x) ∂μ + ∫ (x : F), ↑(L₂ x) ∂ν = ∫ (x : E × F), ↑(L x) ∂μ.prod ν
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✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
s : Set (StrongDual 𝕜 E)
hs : Bornology.IsVonNBounded 𝕜 s
⊢ ∃ r, ∀ x ∈ s, ‖(toLpₗ μ p) x‖ ≤ r

Tactic:
[

Goal state after:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : OpensMeasurableSpace E
μ : Measure E
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
s : Set (StrongDual 𝕜 E)
hs : Bornology.IsVonNBounded 𝕜 s
⊢ ∃ r, ∀ x ∈ s, ‖(toLpₗ μ p) x‖ ≤ r
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: case e_a
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    Real.cos θ • L ∘SL ContinuousLinearMap.inl ℝ E E - Real.sin θ • L ∘SL ContinuousLinearMap.inr ℝ E E
⊢ Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E); μ] +
      Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E); μ] =
    Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] + Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ]

Tactic:
have h2 : (L.comp (.rotation θ)).comp (.inr ℝ E E)
      = Real.sin θ • L.comp (.inl ℝ E E) + Real.cos θ • L.comp (.inr ℝ E E) := by
    ext x
    simp only [ContinuousLinearMap.comp_apply, ContinuousLinearMap.inr_apply,
      ContinuousLinearMap.rotation_apply, smul_zero, zero_add, add_apply, smul_apply,
      ContinuousLinearMap.inl_apply, smul_eq_mul]
    rw [← L.comp_inl_add_comp_inr]
    simp

Goal state after:
case e_a
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
h1 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E =
    Real.cos θ • L ∘SL ContinuousLinearMap.inl ℝ E E - Real.sin θ • L ∘SL ContinuousLinearMap.inr ℝ E E
h2 :
  (L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E =
    Real.sin θ • L ∘SL ContinuousLinearMap.inl ℝ E E + Real.cos θ • L ∘SL ContinuousLinearMap.inr ℝ E E
⊢ Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E); μ] +
      Var[⇑((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E); μ] =
    Var[⇑(L ∘SL ContinuousLinearMap.inl ℝ E E); μ] + Var[⇑(L ∘SL ContinuousLinearMap.inr ℝ E E); μ]
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (fun x ↦ ‖L₁ x‖ * ‖L₂ x‖) μ

Tactic:
[

Goal state after:
case refine_1
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (fun x ↦ ‖L₁ x‖ * ‖L₂ x‖) μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (fun x ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) μ

Tactic:
[

Goal state after:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (fun x ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (fun x ↦ ‖x‖ * (‖L₂‖ * ‖x‖)) μ

Tactic:
[

Goal state after:
case refine_2
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
L₁ L₂ : StrongDual ℝ E
h : MemLp id 2 μ
⊢ Integrable (fun x ↦ ‖x‖ * (‖L₂‖ * ‖x‖)) μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
h_Lp : MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) p μ
this : id = fun x ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
⊢ MemLp id p μ

Tactic:
this

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
h_Lp : MemLp (fun x ↦ x - ∫ (y : E), y ∂μ) p μ
this : id = fun x ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ
⊢ MemLp (fun x ↦ x - ∫ (x : E), x ∂μ + ∫ (x : E), x ∂μ) p μ
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

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

pp: case h
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ MemLp id 2 μ

Tactic:
L.integral_comp_id_comm'

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

E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ Integrable id μ

case h
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
⊢ MemLp id 2 μ
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: a : ℝ
n : ℕ
⊢ normThreshold a (n + 1) ^ 2 ≤ a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)

Tactic:
[

Goal state after:
a : ℝ
n : ℕ
⊢ normThreshold a (n + 1) ^ 2 ≤ a ^ 2 * (1 + √2) ^ 2 * 2 ^ (n + 2)
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ charFun (Measure.map (⇑L) μ) t = charFun (gaussianReal (L m) ((f L) L).toNNReal) t

Tactic:
[

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
x✝ : ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
L : E →L[ℝ] ℝ
t : ℝ
⊢ charFun (Measure.map (⇑L) μ) t = charFun (gaussianReal (L m) ((f L) L).toNNReal) t
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
h' : IsGaussian μ
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ

Tactic:
[

Goal state after:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : SecondCountableTopology E
inst✝⁴ : CompleteSpace E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
m : E
f : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((f L) L) / 2)
h' : IsGaussian μ
⊢ m = ∫ (x : E), x ∂μ ∧ f = covarianceBilinDual μ