mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ gaussianReal (∫ (x : Ω), id (X x) ∂P) Var[id ∘ X; P].toNNReal = gaussianReal (∫ (x : Ω), X x ∂P) Var[X; P].toNNReal

pp: case hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEMeasurable id (Measure.map X P)

pp: case hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEMeasurable X P

pp: case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEMeasurable X P

pp: case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEStronglyMeasurable id (Measure.map X P)

Tactic:
]

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ gaussianReal (∫ (x : Ω), id (X x) ∂P) Var[id ∘ X; P].toNNReal = gaussianReal (∫ (x : Ω), X x ∂P) Var[X; P].toNNReal

case hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEMeasurable id (Measure.map X P)

case hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEMeasurable X P

case hφ
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEMeasurable X P

case hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
X : Ω → ℝ
h : HasGaussianLaw X P
⊢ AEStronglyMeasurable id (Measure.map X P)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c * a⁻¹ ^ 2
⊢ c *
      ENNReal.ofReal
        (rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n + -Real.log (c / (1 - c)).toReal * 2 ^ n)) =
    c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_gt : 2⁻¹ < μ {x | ‖x‖ ≤ a}
ha_lt : μ {x | ‖x‖ ≤ a} < 1
n : ℕ
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c * a⁻¹ ^ 2
⊢ c *
      ENNReal.ofReal
        (rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n + -Real.log (c / (1 - c)).toReal * 2 ^ n)) =
    c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
⊢ cexp (↑(∫ (x : Ω), (fun x ↦ ⟪t, x⟫) (X x) ∂P) * I - ↑Var[fun x ↦ ⟪t, X x⟫; P] / 2) =
    cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)

Tactic:
]

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ x.ofLp ⬝ᵥ S *ᵥ y.ofLp = x.ofLp ⬝ᵥ S *ᵥ y.ofLp

pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ IsSelfAdjoint (toEuclideanCLM (CFC.sqrt S))

pp: case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ MemLp id 2 (stdGaussian (EuclideanSpace ℝ ι))

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ IsSelfAdjoint (toEuclideanCLM (CFC.sqrt S))

case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
x y : EuclideanSpace ℝ ι
h : (fun x ↦ μ + x) ∘ ⇑(toEuclideanCLM (CFC.sqrt S)) = fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x
⊢ MemLp id 2 (stdGaussian (EuclideanSpace ℝ ι))
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✝² : InnerProductSpace ℝ E
ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
hm : ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν
hv : covarianceBilin μ = covarianceBilin ν
t : E
⊢ cexp (↑⟪t, ∫ (x : E), id x ∂μ⟫ * I - ↑(((covarianceBilin μ) t) t) / 2) =
    cexp (↑⟪t, ∫ (x : E), id x ∂ν⟫ * I - ↑(((covarianceBilin ν) t) t) / 2)

Tactic:
hm,

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✝² : InnerProductSpace ℝ E
ν : Measure E
inst✝¹ : IsGaussian μ
inst✝ : IsGaussian ν
hm : ∫ (x : E), id x ∂μ = ∫ (x : E), id x ∂ν
hv : covarianceBilin μ = covarianceBilin ν
t : E
⊢ cexp (↑⟪t, ∫ (x : E), id x ∂ν⟫ * I - ↑(((covarianceBilin μ) t) t) / 2) =
    cexp (↑⟪t, ∫ (x : E), id x ∂ν⟫ * I - ↑(((covarianceBilin ν) t) t) / 2)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
this : covMatrix I = Matrix.of fun s t ↦ ℙ.real (Icc 0 ↑↑s ∩ Icc 0 ↑↑t)
⊢ (Matrix.of fun s t ↦ ℙ.real (Icc 0 ↑↑s ∩ Icc 0 ↑↑t)).PosSemidef

Tactic:
]

Goal state after:
I : Finset ℝ≥0
this : covMatrix I = Matrix.of fun s t ↦ ℙ.real (Icc 0 ↑↑s ∩ Icc 0 ↑↑t)
⊢ (Matrix.of fun s t ↦ ℙ.real (Icc 0 ↑↑s ∩ Icc 0 ↑↑t)).PosSemidef
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
⊢ Measure.map (toLp 2 ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) (multivariateGaussian 0 (covMatrix I)) =
    multivariateGaussian 0 (covMatrix I)

pp: case hg
I : Finset ℝ≥0
⊢ Measurable (toLp 2)

pp: case hf
I : Finset ℝ≥0
⊢ Measurable ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm

Tactic:
]

Goal state after:
I : Finset ℝ≥0
⊢ Measure.map (toLp 2 ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm) (multivariateGaussian 0 (covMatrix I)) =
    multivariateGaussian 0 (covMatrix I)

case hg
I : Finset ℝ≥0
⊢ Measurable (toLp 2)

case hf
I : Finset ℝ≥0
⊢ Measurable ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
f g : (↥I → ℝ) → ℝ
⊢ cov[f ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm, g ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm;
      multivariateGaussian 0 (covMatrix I)] =
    cov[f ∘ ofLp, g ∘ ofLp; multivariateGaussian 0 (covMatrix I)]

Tactic:
]

Goal state after:
I : Finset ℝ≥0
f g : (↥I → ℝ) → ℝ
⊢ cov[f ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm, g ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm;
      multivariateGaussian 0 (covMatrix I)] =
    cov[f ∘ ofLp, g ∘ ofLp; multivariateGaussian 0 (covMatrix I)]
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ ((EuclideanSpace.basisFun ι ℝ) i).ofLp ⬝ᵥ S *ᵥ ((EuclideanSpace.basisFun ι ℝ) j).ofLp = S i j

pp: case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ MemLp id 2 (multivariateGaussian μ S)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ ((EuclideanSpace.basisFun ι ℝ) i).ofLp ⬝ᵥ S *ᵥ ((EuclideanSpace.basisFun ι ℝ) j).ofLp = S i j

case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i j : ι
this : ∀ (i : ι), (fun x ↦ x.ofLp i) = fun x ↦ ⟪(EuclideanSpace.basisFun ι ℝ) i, x⟫
⊢ MemLp id 2 (multivariateGaussian μ S)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
f : (↥I → ℝ) → ℝ
⊢ Var[f ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm; multivariateGaussian 0 (covMatrix I)] =
    Var[f ∘ ofLp; multivariateGaussian 0 (covMatrix I)]

Tactic:
]

Goal state after:
I : Finset ℝ≥0
f : (↥I → ℝ) → ℝ
⊢ Var[f ∘ ⇑(MeasurableEquiv.toLp 2 (↥I → ℝ)).symm; multivariateGaussian 0 (covMatrix I)] =
    Var[f ∘ ofLp; multivariateGaussian 0 (covMatrix I)]
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
⊢ μ (closedBall 0 a) * ENNReal.ofReal (rexp (C * a ^ 2)) = μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))

Tactic:
]

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
⊢ μ (closedBall 0 a) * ENNReal.ofReal (rexp (C * a ^ 2)) = μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I✝ J I : Finset ℝ≥0
⊢ IsGaussian (Measure.map (⇑(EuclideanSpace.equiv ↥I ℝ)) (multivariateGaussian 0 (covMatrix I)))

Tactic:
]

Goal state after:
I✝ J I : Finset ℝ≥0
⊢ IsGaussian (Measure.map (⇑(EuclideanSpace.equiv ↥I ℝ)) (multivariateGaussian 0 (covMatrix I)))
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ S i i = S i i

pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ AEMeasurable (fun x ↦ x.ofLp i) (multivariateGaussian μ S)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ AEMeasurable (fun x ↦ x.ofLp i) (multivariateGaussian μ S)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
⊢ cexp (↑(∫ (x : Ω), L (X x) ∂P) * I - ↑Var[fun x ↦ L (X x); P] / 2) =
    cexp (↑(∫ (x : Ω), (fun x ↦ L (X x)) x ∂P) * I - ↑Var[fun x ↦ L (X x); P] / 2)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
⊢ 0 = 0

pp: case h
I : Finset ℝ≥0
s : ↥I
⊢ Integrable id (projectiveFamily I)

Tactic:
]

Goal state after:
case h
I : Finset ℝ≥0
s : ↥I
⊢ Integrable id (projectiveFamily I)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ gaussianReal ((EuclideanSpace.proj i) (∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S))
      Var[⇑(EuclideanSpace.proj i); multivariateGaussian μ S].toNNReal =
    gaussianReal (μ.ofLp i) (S i i).toNNReal

pp: case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ Integrable id (multivariateGaussian μ S)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ gaussianReal ((EuclideanSpace.proj i) (∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S))
      Var[⇑(EuclideanSpace.proj i); multivariateGaussian μ S].toNNReal =
    gaussianReal (μ.ofLp i) (S i i).toNNReal

case h
ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ Integrable id (multivariateGaussian μ S)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
⊢ ↑(min ↑s ↑t) = ↑(min ↑s ↑t)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
⊢ ↑↑s = ↑↑s

pp: I : Finset ℝ≥0
s : ↥I
⊢ AEMeasurable (fun x ↦ x s) (projectiveFamily I)

Tactic:
]

Goal state after:
I : Finset ℝ≥0
s : ↥I
⊢ AEMeasurable (fun x ↦ x s) (projectiveFamily I)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s : ↥I
⊢ gaussianReal 0 ↑s = gaussianReal 0 ↑s

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case pos
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : μ {x | ‖x‖ ≤ a} = 1
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ ∫⁻ (x : E) in Set.univ, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ =
    ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ

Tactic:
]

Goal state after:
case pos
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : μ {x | ‖x‖ ≤ a} = 1
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ ∫⁻ (x : E) in Set.univ, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ =
    ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: case hm
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ (EuclideanSpace.restrict₂ hJI) μ = (EuclideanSpace.restrict₂ hJI) μ

pp: case hm.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ Integrable id (multivariateGaussian μ S)

Tactic:
]

Goal state after:
case hm.h
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ Integrable id (multivariateGaussian μ S)
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: I : Finset ℝ≥0
s t : ↥I
⊢ gaussianReal (∫ (a : ↥I → ℝ), a s ∂projectiveFamily I - ∫ (a : ↥I → ℝ), a t ∂projectiveFamily I)
      (↑↑s - 2 * ↑(min ↑s ↑t) + ↑↑t).toNNReal =
    gaussianReal 0 (nndist ↑s ↑t)

pp: case hf
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x s) (projectiveFamily I)

pp: case hg
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x t) (projectiveFamily I)

pp: case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

pp: case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

pp: I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)

Tactic:
]

Goal state after:
I : Finset ℝ≥0
s t : ↥I
⊢ gaussianReal (∫ (a : ↥I → ℝ), a s ∂projectiveFamily I - ∫ (a : ↥I → ℝ), a t ∂projectiveFamily I)
      (↑↑s - 2 * ↑(min ↑s ↑t) + ↑↑t).toNNReal =
    gaussianReal 0 (nndist ↑s ↑t)

case hf
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x s) (projectiveFamily I)

case hg
I : Finset ℝ≥0
s t : ↥I
⊢ Integrable (fun x ↦ x t) (projectiveFamily I)

case hX
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x s) 2 (projectiveFamily I)

case hY
I : Finset ℝ≥0
s t : ↥I
⊢ MemLp (fun x ↦ x t) 2 (projectiveFamily I)

I : Finset ℝ≥0
s t : ↥I
⊢ HasGaussianLaw (fun x ↦ x s - x t) (projectiveFamily I)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: case hv
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ (covarianceBilin (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))).toBilinForm =
    (covarianceBilin
        (multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ)
          (S.submatrix (fun i ↦ ⟨↑i, ⋯⟩) fun i ↦ ⟨↑i, ⋯⟩))).toBilinForm

Tactic:
]

Goal state after:
case hv
ι : Type u_2
inst✝ : DecidableEq ι
I J : Finset ι
μ : EuclideanSpace ℝ ↥I
S : Matrix ↥I ↥I ℝ
hS : S.PosSemidef
hJI : J ⊆ I
⊢ (covarianceBilin (Measure.map (⇑(EuclideanSpace.restrict₂ hJI)) (multivariateGaussian μ S))).toBilinForm =
    (covarianceBilin
        (multivariateGaussian ((EuclideanSpace.restrict₂ hJI) μ)
          (S.submatrix (fun i ↦ ⟨↑i, ⋯⟩) fun i ↦ ⟨↑i, ⋯⟩))).toBilinForm
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case pos
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ Set.univ =ᵐ[μ] closedBall 0 a

pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : μ {x | ‖x‖ ≤ a} = 1
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ Measurable fun x ↦ ‖x‖ ≤ a

Tactic:
]

Goal state after:
case pos
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ Set.univ =ᵐ[μ] closedBall 0 a

E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : μ {x | ‖x‖ ≤ a} = 1
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ Measurable fun x ↦ ‖x‖ ≤ a
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t

pp: case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ 2 * min ↑s ↑t ≤ ↑s + ↑t

Tactic:
]

Goal state after:
case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t

case e_v
I : Finset ℝ≥0
s t : ↥I
⊢ 2 * min ↑s ↑t ≤ ↑s + ↑t
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case pos
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ μ (closedBall 0 a)ᶜ = 0

Tactic:
]

Goal state after:
case pos
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
a : ℝ
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
ha_pos : 0 < a
c' : ℝ≥0∞
hc' : c' ≤ μ {x | ‖x‖ ≤ a}
hc'_gt : 2⁻¹ < c'
t : ℕ → ℝ := normThreshold a
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
C : ℝ := logRatio c' * a⁻¹ ^ 2
hc'_le : c' ≤ 1
ha : ∀ᵐ (a_1 : E) ∂μ, ‖a_1‖ ≤ a
ht_int_zero : ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤ ENNReal.ofReal (rexp (logRatio c'))
⊢ μ (closedBall 0 a)ᶜ = 0
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
X : Ω → E
inst✝ : NormedSpace ℝ E
L : StrongDual ℝ E
hX : HasGaussianLaw X P
⊢ cexp (↑(∫ (x : Ω), (fun x ↦ L (X x)) x ∂P) * I - ↑Var[fun x ↦ L (X x); P] / 2) =
    cexp (↑(∫ (ω : Ω), L (X ω) ∂P) * I - ↑Var[fun ω ↦ L (X ω); P] / 2)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily

Goal state before:
pp: case e'_2
I : Finset ℝ≥0
s t : ↥I
this : ∀ (s t : ↥I), ↑s ≤ ↑t → ↑s + ↑t - 2 * min ↑s ↑t = nndist ↑s ↑t
hst : ¬↑s ≤ ↑t
⊢ ↑t + ↑s - 2 * min ↑t ↑s = ↑t + ↑s - 2 * min ↑t ↑s

Tactic:
]

Goal state after: