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

pp: case e_6.e'_2
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:
·

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

pp: case 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
⊢ ↑Var[⇑L₁; μ] / 2 + ↑Var[⇑L₂; ν] / 2 = ↑Var[⇑L; μ.prod ν] / 2

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.Distributions.Fernique

Goal state before:
pp: case e_6.e'_2
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:
·

Goal state after:
case e_6.e'_2
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.Basic

Goal state before:
pp: case 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
⊢ ↑Var[⇑L₁; μ] / 2 + ↑Var[⇑L₂; ν] / 2 = ↑Var[⇑L; μ.prod ν] / 2

Tactic:
·

Goal state after:
case 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
⊢ ↑Var[⇑L₁; μ] / 2 + ↑Var[⇑L₂; ν] / 2 = ↑Var[⇑L; μ.prod ν] / 2
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
x✝¹ x✝ : StrongDual ℝ E
⊢ ((uncenteredCovarianceBilinDual 0) x✝¹) x✝ = (0 x✝¹) x✝

Tactic:
have : Subsingleton (Lp ℝ 2 (0 : Measure E)) := ⟨fun x y ↦ Lp.ext_iff.2 rfl⟩

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : OpensMeasurableSpace E
x✝¹ x✝ : StrongDual ℝ E
this : Subsingleton ↥(Lp ℝ 2 0)
⊢ ((uncenteredCovarianceBilinDual 0) x✝¹) x✝ = (0 x✝¹) 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✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
this : b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
⊢ (‖p.1 + p.2‖ - ‖p.1 - p.2‖) * 2 = √2 ^ 2 * (‖p.1 + p.2‖ - ‖p.1 - p.2‖)

Tactic:
Real.sq_sqrt (by positivity)

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✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
this : b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
⊢ (‖p.1 + p.2‖ - ‖p.1 - p.2‖) * 2 = 2 * (‖p.1 + p.2‖ - ‖p.1 - p.2‖)
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case neg
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 μ
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ

pp: case pos
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 μ
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ

Tactic:
·

Goal state after:
case neg
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 μ
⊢ ‖((uncenteredCovarianceBilinDual μ) L₁) L₂‖ ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 2 ∂μ
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‖) μ

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‖) μ

pp: case refine_3
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 μ
x : E
⊢ (fun x ↦ ‖L₁ x‖ * ‖L₂ x‖) x ≤ (fun x ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) 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‖) μ

pp: case refine_3
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 μ
x : E
⊢ (fun x ↦ ‖L₁ x‖ * ‖L₂ x‖) x ≤ (fun x ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) 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.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✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
⊢ b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2

Tactic:
calc b - a < ‖p.1 + p.2‖ / √2 - a := by gcongr
      _ ≤ ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 := by gcongr

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

Goal state before:
pp: case refine_3
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 μ
x : E
⊢ (fun x ↦ ‖L₁ x‖ * ‖L₂ x‖) x ≤ (fun x ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) x

Tactic:
·

Goal state after:
case refine_3
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 μ
x : E
⊢ (fun x ↦ ‖L₁ x‖ * ‖L₂ x‖) x ≤ (fun x ↦ ‖L₁‖ * ‖x‖ * ‖L₂‖ * ‖x‖) x
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case h₁
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 μ
x : E
⊢ ‖L₁ x‖ ≤ ‖L₁‖ * ‖x‖

pp: case h₂
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 μ
x : E
⊢ ‖L₂ x‖ ≤ ‖L₂‖ * ‖x‖

Tactic:
·

Goal state after:
case h₁
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 μ
x : E
⊢ ‖L₁ x‖ ≤ ‖L₁‖ * ‖x‖
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case h₂
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 μ
x : E
⊢ ‖L₂ x‖ ≤ ‖L₂‖ * ‖x‖

Tactic:
·

Goal state after:
case h₂
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 μ
x : E
⊢ ‖L₂ x‖ ≤ ‖L₂‖ * ‖x‖
Module: Mathlib.Probability.Moments.CovarianceBilinDual

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

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (fun x ↦ x - c) p μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
⊢ MemLp (fun x ↦ c) p μ

Tactic:
·

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

Goal state before:
pp: case neg.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
h_Lp : MemLp (fun x ↦ x - c) 0 μ
⊢ MemLp (fun x ↦ c) 0 μ

pp: case neg.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (fun x ↦ x - c) p μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
⊢ MemLp (fun x ↦ c) p μ

Tactic:
·

Goal state after:
case neg.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
h_Lp : MemLp (fun x ↦ x - c) 0 μ
⊢ MemLp (fun x ↦ c) 0 μ
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case neg.inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
h_Lp : MemLp (fun x ↦ x - c) ∞ μ
hp0 : ∞ ≠ 0
⊢ MemLp (fun x ↦ c) ∞ μ

pp: case neg.inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
p : ℝ≥0∞
c : E := ∫ (x : E), x ∂μ
h_Lp : MemLp (fun x ↦ x - c) p μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
hp0 : p ≠ 0
hptop : p ≠ ∞
⊢ MemLp (fun x ↦ c) p μ

Tactic:
·

Goal state after:
case neg.inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this : id = fun x ↦ x - c + c
hx : ¬c = 0
h_Lp : MemLp (fun x ↦ x - c) ∞ μ
hp0 : ∞ ≠ 0
⊢ MemLp (fun x ↦ c) ∞ μ
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
⊢ Integrable id μ

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:
·

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
⊢ Integrable id μ
Module: Mathlib.Probability.Distributions.Gaussian.CharFun

Goal state before:
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:
·

Goal state after:
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: case ha
a : ℝ
n : ℕ
⊢ 0 ≤ √2 ^ (n + 2) - 1

pp: case hab
a : ℝ
n : ℕ
⊢ √2 ^ (n + 2) - 1 ≤ √2 ^ (n + 2)

Tactic:
·

Goal state after:
case ha
a : ℝ
n : ℕ
⊢ 0 ≤ √2 ^ (n + 2) - 1
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: case hab
a : ℝ
n : ℕ
⊢ √2 ^ (n + 2) - 1 ≤ √2 ^ (n + 2)

Tactic:
·

Goal state after:
case hab
a : ℝ
n : ℕ
⊢ √2 ^ (n + 2) - 1 ≤ √2 ^ (n + 2)
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case neg.inr.inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖y‖ ≤ ‖c‖ / 2
⊢ ‖c‖ ^ ↑p ≤ 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 2 ^ ↑p * ‖y - c‖ ^ ↑p

pp: case neg.inr.inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖c‖ / 2 ≤ ‖y‖
⊢ ‖c‖ ^ ↑p ≤ 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 2 ^ ↑p * ‖y - c‖ ^ ↑p

Tactic:
·

Goal state after:
case neg.inr.inr.inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖y‖ ≤ ‖c‖ / 2
⊢ ‖c‖ ^ ↑p ≤ 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 2 ^ ↑p * ‖y - c‖ ^ ↑p
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: a : ℝ
n : ℕ
⊢ (√2 ^ 2) ^ (n + 2) = 2 ^ (n + 2)

Tactic:
Real.sq_sqrt (by positivity)

Goal state after:
a : ℝ
n : ℕ
⊢ 2 ^ (n + 2) = 2 ^ (n + 2)
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case neg.inr.inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖c‖ / 2 ≤ ‖y‖
⊢ ‖c‖ ^ ↑p ≤ 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 2 ^ ↑p * ‖y - c‖ ^ ↑p

Tactic:
·

Goal state after:
case neg.inr.inr.inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
mE : MeasurableSpace E
μ : Measure E
inst✝ : NormedSpace ℝ E
c : E := ∫ (x : E), x ∂μ
this✝ : id = fun x ↦ x - c + c
hx : ¬c = 0
I : Integrable (fun x ↦ ‖x‖) μ
y : E
p : ℝ≥0
h_Lp : MemLp (fun x ↦ x - c) (↑p) μ
hp0 : ↑p ≠ 0
this : Integrable (fun x ↦ 2 ^ (↑p).toReal * ‖x - c‖ ^ (↑p).toReal) μ
h✝ : ‖c‖ / 2 ≤ ‖y‖
⊢ ‖c‖ ^ ↑p ≤ 2 * ‖c‖ ^ (↑p - 1) * ‖y‖ + 2 ^ ↑p * ‖y - c‖ ^ ↑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✝ : 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 : ℝ
⊢ t * (t * (f L) L) / 2 = (f L) L * t ^ 2 / 2

pp: case hr
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 : ℝ
⊢ 0 ≤ (f L) L

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 : ℝ
⊢ t * (t * (f L) L) / 2 = (f L) L * t ^ 2 / 2
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 : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ 0 < c.toReal

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 : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ 0 < (1 - c).toReal

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 : ℕ
c : ℝ≥0∞ := μ {x | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ 0 < c.toReal
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: case e_f
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : IsGaussian μ
inst✝ : SecondCountableTopology E
L : StrongDual ℝ E
x : E
⊢ ∫ (a : E), L x ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ +
      ∫ (a : E), L a ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ =
    L x + ∫ (y : E), L y ∂Measure.map (⇑(ContinuousLinearEquiv.neg ℝ)) μ

Tactic:
simp [-ContinuousLinearEquiv.coe_neg, integral_const, smul_eq_mul]

Goal state after: