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

Goal state before:
pp: case convert_5
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
⊢ 0 ∈ interior (integrableExpSet (fun x ↦ ‖x‖ ^ 2) μ)

Tactic:
obtain ⟨C, hC_pos, hC⟩ := exists_integrable_exp_sq μ

Goal state after:
case convert_5
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
⊢ 0 ∈ interior (integrableExpSet (fun x ↦ ‖x‖ ^ 2) μ)
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
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
⊢ AEStronglyMeasurable (fun x ↦ rexp (-C * ‖x‖ ^ 2)) μ

Tactic:
by

Goal state after:
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
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
x✝ : E
⊢ 0 x✝ ≤ (fun x ↦ rexp (-C * ‖x‖ ^ 2)) x✝

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ IsGaussian (multivariateGaussian μ S)

Tactic:
by

Goal state after:
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
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
⊢ Integrable (fun x ↦ rexp (-C * ‖x‖ ^ 2)) μ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ AEMeasurable (fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x) (stdGaussian (EuclideanSpace ℝ ι))

Tactic:
by

Goal state after:
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
⊢ ∫⁻ (x : E) in closedBall 0 (t (n + 1)) \ closedBall 0 (t n), ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    ∫⁻ (x : E) in closedBall 0 (t (n + 1)) \ closedBall 0 (t n), ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) ∂μ

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ AEStronglyMeasurable (fun x ↦ x)
    (Measure.map (fun x ↦ μ + (toEuclideanCLM (CFC.sqrt S)) x) (stdGaussian (EuclideanSpace ℝ ι)))

Tactic:
by

Goal state after:
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
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
hC_neg : Integrable (fun x ↦ rexp (-C * ‖x‖ ^ 2)) μ
⊢ Set.Ioo (-C) C ⊆ interior (integrableExpSet (fun x ↦ ‖x‖ ^ 2) μ)

Tactic:
by

Goal state after:
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
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0
C : ℝ
hC_pos : 0 < C
hC : Integrable (fun x ↦ rexp (C * ‖x‖ ^ 2)) μ
hC_neg : Integrable (fun x ↦ rexp (-C * ‖x‖ ^ 2)) μ
h_subset : Set.Ioo (-C) C ⊆ interior (integrableExpSet (fun x ↦ ‖x‖ ^ 2) μ)
⊢ -C < 0

Tactic:
by

Goal state after:
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
⊢ ∫⁻ (x : E) in closedBall 0 (t (n + 1)) \ closedBall 0 (t n), ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) ∂μ =
    ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) * μ (closedBall 0 (t (n + 1)) \ closedBall 0 (t n))

Tactic:
by

Goal state after:
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
inst✝² : CompleteSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp id p μ

Tactic:
by

Goal state after:
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
⊢ 1 ≠ ∞

Tactic:
by

Goal state after:
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
⊢ 2 ≠ ∞

Tactic:
by

Goal state after:
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
L : StrongDual ℝ E
⊢ 1 ≠ ∞

Tactic:
by

Goal state after:
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
⊢ ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) * μ (closedBall 0 (t (n + 1)) \ closedBall 0 (t n)) ≤
    ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) * μ {x | t n < ‖x‖}

Tactic:
by

Goal state after:
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (L : StrongDual ℝ E), Var[⇑L; μ] = 0
⊢ μ = Measure.dirac (∫ (x : E), x ∂μ)

Tactic:
by

Goal state after:
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
⊢ ∃ L, Var[⇑L; μ] ≠ 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ Measurable ⇑(toEuclideanCLM (CFC.sqrt S))

Tactic:
by

Goal state after:
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[⇑L; μ] ≠ 0
⊢ NullSingletonClass (Measure.map (⇑L) μ)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ ∫ (x : EuclideanSpace ℝ ι), x ∂multivariateGaussian μ S = μ

Tactic:
by

Goal state after:
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[⇑L; μ] ≠ 0
⊢ (Measure.map (⇑L) μ) {L x} = 0

Tactic:
by

Goal state after:
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
L : StrongDual ℝ E
hL : Var[⇑L; μ] ≠ 0
hL_zero : (Measure.map (⇑L) μ) {L x} = 0
⊢ Measurable ⇑L

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
⊢ ∫ (x : EuclideanSpace ℝ ι), id x ∂multivariateGaussian μ S = μ

Tactic:
by

Goal state after:
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
h : ∀ (x : E), μ ≠ Measure.dirac x
x : E
⊢ μ {x} = 0

Tactic:
by

Goal state after:
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
⊢ ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) * μ {x | t n < ‖x‖} ≤
    ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) * c * ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * 2 ^ n))

Tactic:
by

Goal state after:
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hμ : ∫ (x : E), id x ∂μ = 0
L : StrongDual ℝ E
⊢ charFunDual μ L = cexp (-↑Var[⇑L; μ] / 2)

Tactic:
by

Goal state after:
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✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hμ : ∫ (x : E), id x ∂μ = 0
θ : ℝ
⊢ Measure.map (⇑(ContinuousLinearMap.rotation θ)) (μ.prod μ) = μ.prod μ

Tactic:
by

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
⊢ Measurable ⇑(toEuclideanCLM (CFC.sqrt S))

Tactic:
by

Goal state after:
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
⊢ ENNReal.ofReal (rexp (C * t (n + 1) ^ 2)) * c * ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * 2 ^ n)) ≤
    ENNReal.ofReal (rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n)) * c *
      ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * 2 ^ n))

Tactic:
by

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✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
mE : MeasurableSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
h : X =ᵐ[P] Y
⊢ IsGaussian (Measure.map Y P)

Tactic:
← Measure.map_congr h

Goal state after:
Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
mE : MeasurableSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
h : X =ᵐ[P] Y
⊢ IsGaussian (Measure.map X P)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module ℝ E
mE : MeasurableSpace E
X Y : Ω → E
hX : HasGaussianLaw X P
h : X =ᵐ[P] Y
⊢ IsGaussian (Measure.map Y P)

Tactic:
by

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

Goal state before:
pp: E : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
μ : Measure E
inst✝ : IsGaussian μ
⊢ IsGaussian (Measure.map id μ)

Tactic:
by

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✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
μ : Measure E
hX : HasLaw X μ P
inst✝ : IsGaussian μ
⊢ IsGaussian (Measure.map X P)

Tactic:
by

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✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module ℝ E
mE : MeasurableSpace E
X : Ω → E
F : Type u_5
inst✝⁴ : TopologicalSpace F
inst✝³ : AddCommMonoid F
inst✝² : Module ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : OpensMeasurableSpace F
L : E →L[ℝ] F
hX : HasGaussianLaw X P
hL : Measurable ⇑L
⊢ IsGaussian (Measure.map (⇑L ∘ X) P)

Tactic:
by

Goal state after:
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
inst✝ : IsFiniteMeasure μ
⊢ IsGaussian μ ↔ ∃ m f, f.toBilinForm.IsPosSemidef ∧ ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)

Tactic:
by

Goal state after:
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
⊢ 0 ≤ rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n)

Tactic:
by

Goal state after:
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
inst✝ : IsFiniteMeasure μ
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
⊢ ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((g L) L) / 2)

Tactic:
by

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, (toEuclideanCLM (CFC.sqrt S)) ((ContinuousLinearMap.adjoint (toEuclideanCLM (CFC.sqrt S))) y)⟫ =
    x.ofLp ⬝ᵥ S *ᵥ y.ofLp

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:
IsSelfAdjoint.adjoint_eq,

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
⊢ ⟪x, (toEuclideanCLM (CFC.sqrt S)) ((toEuclideanCLM (CFC.sqrt S)) y)⟫ = x.ofLp ⬝ᵥ S *ᵥ y.ofLp

ι : 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.HasGaussianLaw.Basic

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

Tactic:
by

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
inst✝¹ : Subsingleton E
inst✝ : IsProbabilityMeasure P
⊢ AEMeasurable X P

Tactic:
by

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
inst✝¹ : Subsingleton E
inst✝ : IsProbabilityMeasure P
⊢ IsGaussian (Measure.map X P)

Tactic:
by

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✝ : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
⊢ AEStronglyMeasurable (fun x ↦ ↑((fun x ↦ ⟪t, x⟫) x)) (Measure.map X P)

Tactic:
by

Goal state after:
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
inst✝ : IsFiniteMeasure μ
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
this : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((g L) L) / 2)
x y : StrongDual ℝ E
⊢ (g.toBilinForm x) y = (g.toBilinForm y) x

Tactic:
by

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✝ : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
⊢ AEMeasurable (fun x ↦ ⟪t, x⟫) (Measure.map X P)

Tactic:
by

Goal state after:
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
inst✝ : IsFiniteMeasure μ
m : E
f : E →L[ℝ] E →L[ℝ] ℝ
hf : f.toBilinForm.IsPosSemidef
h : ∀ (t : E), charFun μ t = cexp (↑⟪t, m⟫ * I - ↑((f t) t) / 2)
g : StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ :=
  f.bilinearComp (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
    (InnerProductSpace.toDual ℝ E).symm.toLinearIsometry.toContinuousLinearMap
this : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp (↑(L m) * I - ↑((g L) L) / 2)
x : StrongDual ℝ E
⊢ 0 ≤ (g.toBilinForm x) x

Tactic:
by

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✝ : InnerProductSpace ℝ E
t : E
hX : HasGaussianLaw X P
⊢ charFun (Measure.map X P) t = cexp (↑(∫ (x : Ω), (fun ω ↦ ⟪t, X ω⟫) x ∂P) * I - ↑Var[fun ω ↦ ⟪t, X ω⟫; P] / 2)

Tactic:
by

Goal state after:
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
⊢ ENNReal.ofReal (rexp (2⁻¹ * Real.log (c.toReal / (1 - c).toReal) * 2 ^ n)) * c *
      ENNReal.ofReal (rexp (-Real.log (c / (1 - c)).toReal * 2 ^ n)) =
    c * ENNReal.ofReal (rexp (-2⁻¹ * Real.log (c / (1 - c)).toReal * 2 ^ n))

Tactic:
by

Goal state after: