mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ ⋯.measurableSpace ≤ hτ.measurableSpace

Tactic:
IsStoppingTime.measurableSpace_min_const

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ IsStoppingTime.measurableSpace ?hτ ⊓ ↑ℱ i ≤ hτ.measurableSpace

case hτ
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁴ : LinearOrder ι
μ : Measure Ω
ℱ : Filtration ι m
τ : Ω → WithTop ι
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : Ω → E
hτ : IsStoppingTime ℱ τ
i : ι
inst✝ : SigmaFinite (μ.trim ⋯)
⊢ IsStoppingTime ℱ τ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
⊢ g = fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)

Tactic:
ext x

Goal state after:
μ : ℝ
v : ℝ≥0
hv : ¬v = 0
g : ℝ → ℝ := fun x ↦ (√(2 * π * ↑v))⁻¹ * rexp (-x ^ 2 / (2 * ↑v))
x : ℝ
⊢ g x = (√(2 * π * ↑v))⁻¹ * rexp (-↑(2 * v)⁻¹ * x ^ 2)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
hv : v ≠ 0
⊢ Function.support (gaussianPDF μ v) = Set.univ

Tactic:
ext x

Goal state after:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
x : ℝ
⊢ x ∈ Function.support (gaussianPDF μ v) ↔ x ∈ Set.univ
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: case e'_7
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsGaussian μ
L : StrongDual ℝ E
p : ℝ≥0∞
hp : p ≠ ∞
⊢ p = ↑p.toNNReal

Tactic:
simp [hp]

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

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

Tactic:
rw [Measure.map_map (by fun_prop) (by fun_prop)]

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.Real

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

Tactic:
rw [← variance_id_gaussianReal (μ := μ₁) (v := v₁),
    ← variance_id_gaussianReal (μ := μ₂) (v := v₂), h]

Goal state after:
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); μ] = ↑(max Var[⇑L; μ] 0) * ↑u ^ 2

Tactic:
rw [max_eq_left (variance_nonneg _ _), mul_comm, ← ofReal_pow, ← ofReal_mul,
      ← variance_const_mul]
    congr

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

Goal state before:
pp: case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
p : ℝ≥0∞
𝕜 : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 E
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : p = 0
⊢ (eLpNorm (⇑L) p μ).toReal ≤ ‖L‖ * (eLpNorm id p μ).toReal

Tactic:
simp [hp]

Goal state after:
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✝ = ((covarianceBilin μ) 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:
covarianceBilin_of_not_memLp h

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
⊢ (0 x✝¹) x✝ = (0 x✝¹) x✝

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) μ)
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
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this : ‖(toLpₗ μ p) L‖ ≤ (‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ).toReal ^ p.toReal⁻¹
⊢ p ≠ 0

Tactic:
simp [hp]

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
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
⊢ p ≠ 0

Tactic:
simp [hp]

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

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

Tactic:
ext x

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 : E
⊢ (covarianceOperator μ) x = 0 x
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
inst✝ : OpensMeasurableSpace E
L : StrongDual 𝕜 E
h_Lp : MemLp id p μ
hp : ¬p = 0
hp_top : ¬p = ∞
h0 : 0 < p.toReal
this : ∫⁻ (x : E), ‖L x‖ₑ ^ p.toReal ∂μ ≤ ‖L‖ₑ ^ p.toReal * ∫⁻ (x : E), ‖x‖ₑ ^ p.toReal ∂μ
h : eLpNorm id p μ ≠ ∞
⊢ p ≠ 0

Tactic:
simp [hp]

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

Goal state before:
pp: case e_6
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ ⇑(ContinuousLinearMap.rotation (-(π / 4))) ⁻¹' {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} =
    {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}

Tactic:
simp only [Set.preimage_ofPred_eq, ContinuousLinearMap.rotation_apply, Real.cos_neg,
      Real.cos_pi_div_four, Real.sin_neg, Real.sin_pi_div_four, neg_smul, neg_neg]

Goal state after:
case e_6
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ {a_1 | ‖(√2 / 2) • a_1.1 + -((√2 / 2) • a_1.2)‖ ≤ a ∧ b < ‖(√2 / 2) • a_1.1 + (√2 / 2) • a_1.2‖} =
    {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case e_6.e'_1
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
⊢ ‖(√2 / 2) • p.1 + -((√2 / 2) • p.2)‖ = ‖p.1 - p.2‖ / √2

Tactic:
← sub_eq_add_neg,

Goal state after:
case e_6.e'_1
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
⊢ ‖(√2 / 2) • p.1 - (√2 / 2) • p.2‖ = ‖p.1 - p.2‖ / √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
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopology E
inst✝ : CompleteSpace E
hμ : ∀ (L : StrongDual ℝ E), ∫ (x : E), L x ∂μ = 0
θ : ℝ
L : StrongDual ℝ (E × E)
⊢ (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

Tactic:
ext x

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)
x : E
⊢ ((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inl ℝ E E) x =
    (Real.cos θ • L ∘SL ContinuousLinearMap.inl ℝ E E - Real.sin θ • L ∘SL ContinuousLinearMap.inr ℝ E E) 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)
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
⊢ (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

Tactic:
ext x

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)
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
x : E
⊢ ((L ∘SL ContinuousLinearMap.rotation θ) ∘SL ContinuousLinearMap.inr ℝ E E) x =
    (Real.sin θ • L ∘SL ContinuousLinearMap.inl ℝ E E + Real.cos θ • L ∘SL ContinuousLinearMap.inr ℝ E E) 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
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint :
  (∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)) ∧
    Integrable (fun x ↦ ∫ (y : E), ‖rexp (C * ‖x + y‖ ^ 2)‖ ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ) μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC : ∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (-id) μ)
y : E
hy : Integrable ((fun y_1 ↦ rexp (C * ‖y + y_1‖ ^ 2)) ∘ (-id)) μ
x : E
⊢ ‖x - y‖ = ‖y + -x‖

Tactic:
← sub_eq_add_neg,

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : SecondCountableTopology E
μ : Measure E
inst✝ : IsGaussian μ
C C' : ℝ
hint :
  (∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ)) ∧
    Integrable (fun x ↦ ∫ (y : E), ‖rexp (C * ‖x + y‖ ^ 2)‖ ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ) μ
hC'_pos : 0 < C'
hC'_lt : C' < C
hC : ∀ᵐ (x : E) ∂μ, Integrable (fun y ↦ rexp (C * ‖x + y‖ ^ 2)) (Measure.map (-id) μ)
y : E
hy : Integrable ((fun y_1 ↦ rexp (C * ‖y + y_1‖ ^ 2)) ∘ (-id)) μ
x : E
⊢ ‖x - y‖ = ‖y - x‖
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
L : StrongDual ℝ E
⊢ (⇑L ∘ fun x ↦ ∑ i, x i • (stdOrthonormalBasis ℝ E) i) = ∑ i, fun x ↦ L ((stdOrthonormalBasis ℝ E) i) * x i

Tactic:
ext x

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
L : StrongDual ℝ E
x : Fin (finrank ℝ E) → ℝ
⊢ (⇑L ∘ fun x ↦ ∑ i, x i • (stdOrthonormalBasis ℝ E) i) x = (∑ i, fun x ↦ L ((stdOrthonormalBasis ℝ E) i) * x i) x
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
μ : EuclideanSpace ℝ ι
S : Matrix ι ι ℝ
hS : S.PosSemidef
i : ι
⊢ Var[fun x ↦ x.ofLp i; multivariateGaussian μ S] = S i i

Tactic:
rw [← covariance_self, covariance_eval_multivariateGaussian hS]

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
s : ↥I
⊢ Var[fun x ↦ x s; projectiveFamily I] = ↑↑s

Tactic:
by
  rw [← covariance_self, covariance_eval_projectiveFamily, min_self]
  exact aemeasurable_id.eval s

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_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
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
ha_lt : μ {x | ‖x‖ ≤ a} < 1
hc'_lt : c' < 1
⊢ Set.univ = closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n)

Tactic:
ext x

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
ht_int_zero :
  ∫⁻ (x : E) in closedBall 0 a, ENNReal.ofReal (rexp (C * ‖x‖ ^ 2)) ∂μ ≤
    μ {x | ‖x‖ ≤ a} * ENNReal.ofReal (rexp (logRatio c'))
ha : ¬μ {x | ‖x‖ ≤ a} = 1
ha_lt : μ {x | ‖x‖ ≤ a} < 1
hc'_lt : c' < 1
x : E
⊢ x ∈ Set.univ ↔ x ∈ closedBall 0 a ∪ ⋃ n, closedBall 0 (t (n + 1)) \ closedBall 0 (t n)
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
I : Finset T
⊢ ∑ i ∈ I, X i = ∑ i, fun ω ↦ I.restrict (fun x ↦ X x ω) i

Tactic:
simp [I.sum_attach X]

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 μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
h_neg : a < 0
⊢ {x | ‖x‖ ≤ a} = ∅

Tactic:
ext x

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 μ
c : ℝ≥0∞
hc : c ≤ μ {x | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
h_neg : a < 0
x : E
⊢ x ∈ {x | ‖x‖ ≤ a} ↔ x ∈ ∅
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
⊢ IndepFun (fun ω i ↦ X i ω) Y κ P

Tactic:
let πX := {s : Set Ω | ∃ t ∈ squareCylinders (fun i ↦ {s : Set (𝓧 i) | MeasurableSet s}),
      (fun ω i ↦ X i ω) ⁻¹' t = s}

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
⊢ IndepFun (fun ω i ↦ X i ω) Y κ P
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
⊢ MeasurableSpace.comap (fun ω i ↦ X i ω) MeasurableSpace.pi = generateFrom πX

Tactic:
generateFrom_squareCylinders.symm,

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
𝓧 : S → Type u_5
𝓨 : Type u_6
inst✝² : (i : S) → MeasurableSpace (𝓧 i)
inst✝¹ : MeasurableSpace 𝓨
X : (i : S) → Ω → 𝓧 i
Y : Ω → 𝓨
hX : ∀ (i : S), Measurable (X i)
hY : Measurable Y
h : ∀ (I : Finset S), IndepFun (fun ω i ↦ X (↑i) ω) Y κ P
inst✝ : IsZeroOrMarkovKernel κ
πX : Set (Set Ω) := {s | ∃ t ∈ squareCylinders fun i ↦ {s | MeasurableSet s}, (fun ω i ↦ X i ω) ⁻¹' t = s}
πX_pi : IsPiSystem πX
⊢ MeasurableSpace.comap (fun ω i ↦ X i ω) (generateFrom (squareCylinders fun i ↦ {s | MeasurableSet s})) =
    generateFrom πX
Module: Mathlib.Probability.Independence.Process.Basic

Goal state before:
pp: S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
s : Finset S
f : S → Set Ω
g : (i : S) → Set ((fun i ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i = f i
h3 : ⋂ i ∈ s, f i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i
h3' : ∀ (a : α), ∏ i ∈ s, (κ a) (f i) = ∏ i ∈ s, (κ a) ((fun i ω j ↦ X' i j ω) i ⁻¹' g i)
⊢ ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i)

Tactic:
simp_rw [h3, h3']

Goal state after:
S : Type u_1
Ω : Type u_3
mΩ : MeasurableSpace Ω
α : Type u_4
mα : MeasurableSpace α
κ : Kernel α Ω
P : Measure α
T : S → Type u_5
𝓧 : (i : S) → T i → Type u_6
inst✝ : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)
X X' : (i : S) → (j : T i) → Ω → 𝓧 i j
h1 : iIndepFun (fun i ω j ↦ X i j ω) κ P
h2 : ∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j
s : Finset S
f : S → Set Ω
g : (i : S) → Set ((fun i ↦ (j : T i) → 𝓧 i j) i)
mg : ∀ i ∈ s, MeasurableSet (g i)
hg : ∀ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i = f i
h3 : ⋂ i ∈ s, f i = ⋂ i ∈ s, (fun i ω j ↦ X' i j ω) i ⁻¹' g i
h3' : ∀ (a : α), ∏ i ∈ s, (κ a) (f i) = ∏ i ∈ s, (κ a) ((fun i ω j ↦ X' i j ω) i ⁻¹' g i)
⊢ ∀ᵐ (a : α) ∂P, (κ a) (⋂ i ∈ s, (fun ω j ↦ X' i j ω) ⁻¹' g i) = ∏ x ∈ s, (κ a) ((fun ω j ↦ X' x j ω) ⁻¹' g x)
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
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
h_le : ∀ (a : ℝ), μ {x | ‖x‖ ≤ a} ≤ 2⁻¹
⊢ Set.univ = ⋃ a, {x | ‖x‖ ≤ ↑a}

Tactic:
ext x

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
h_le : ∀ (a : ℝ), μ {x | ‖x‖ ≤ a} ≤ 2⁻¹
x : E
⊢ x ∈ Set.univ ↔ x ∈ ⋃ a, {x | ‖x‖ ≤ ↑a}