mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω ↦ ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ ‖↑(|X a| ^ p) * cexp (z * ↑(X a))‖) μ

Tactic:
;

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω ↦ ↑(|X ω| ^ p) * cexp (z * ↑(X ω))) μ

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ ‖↑(|X a| ^ p) * cexp (z * ↑(X a))‖) μ
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω ↦ ↑(X ω ^ p) * cexp (z * ↑(X ω))) μ

pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ ‖↑(X a ^ p) * cexp (z * ↑(X a))‖) μ

Tactic:
;

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ AEStronglyMeasurable (fun ω ↦ ↑(X ω ^ p) * cexp (z * ↑(X ω))) μ

Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
p : ℝ
hp : 0 ≤ p
hX : AEMeasurable X μ
⊢ Integrable (fun a ↦ ‖↑(X a ^ p) * cexp (z * ↑(X a))‖) μ
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: μ : Measure ℝ
h : IsGaussian μ
⊢ gaussianReal (∫ (x : ℝ), (ContinuousLinearMap.id ℝ ℝ) x ∂μ) Var[⇑(ContinuousLinearMap.id ℝ ℝ); μ].toNNReal =
    gaussianReal (∫ (x : ℝ), id x ∂μ) Var[id; μ].toNNReal

Tactic:
;

Goal state after:
μ : Measure ℝ
h : IsGaussian μ
⊢ gaussianReal (∫ (x : ℝ), (ContinuousLinearMap.id ℝ ℝ) x ∂μ) Var[⇑(ContinuousLinearMap.id ℝ ℝ); μ].toNNReal =
    gaussianReal (∫ (x : ℝ), id x ∂μ) Var[id; μ].toNNReal
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
⊢ NeZero (gaussianReal μ v)

Tactic:
;

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
⊢ NeZero (gaussianReal μ v)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (Measure.map (⇑L) μ)
⊢ IsGaussian μ

Tactic:
refine ⟨fun L ↦ ?_⟩

Goal state after:
E : Type u_1
inst✝³ : TopologicalSpace E
inst✝² : AddCommMonoid E
inst✝¹ : Module ℝ E
mE : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
μ : Measure E
h : ∀ (L : E →L[ℝ] ℝ), IsGaussian (Measure.map (⇑L) μ)
L : StrongDual ℝ E
⊢ Measure.map (⇑L) μ = gaussianReal (∫ (x : E), L x ∂μ) Var[⇑L; μ].toNNReal
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
⊢ NeZero (gaussianReal μ v)

Tactic:
;

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
⊢ NeZero (gaussianReal μ v)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

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

Tactic:
;

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : MeasurableSpace E
inst✝⁴ : BorelSpace E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
μ : Measure E
L : E ≃L[ℝ] F
h : IsGaussian (Measure.map (⇑L) μ)
this : μ = Measure.map (⇑L.symm) (Measure.map (⇑L) μ)
⊢ IsGaussian (Measure.map (⇑L.symm) (Measure.map (⇑L) μ))
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v p : ℝ≥0
⊢ MemLp id (↑p) (gaussianReal μ v)

Tactic:
exact memLp_id_gaussianReal p

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

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

Tactic:
;

Goal state after:
μ₁ : ℝ
v₁ : ℝ≥0
⊢ gaussianReal μ₁ v₁ = gaussianReal μ₁ v₁
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
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
⊢ MemLp.toLp (⇑u + ⇑v) ⋯ = MemLp.toLp ⇑u ⋯ + MemLp.toLp ⇑v ⋯

Tactic:
;

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
u v : StrongDual 𝕜 E
⊢ MemLp.toLp (⇑u + ⇑v) ⋯ = MemLp.toLp ⇑u ⋯ + MemLp.toLp ⇑v ⋯
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
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ MemLp.toLp (c • ⇑L) ⋯ = id c • MemLp.toLp ⇑L ⋯

Tactic:
;

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ MemLp.toLp (c • ⇑L) ⋯ = id c • MemLp.toLp ⇑L ⋯
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ Measure.map X P ≠ 0

Tactic:
;

Goal state after:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ Measure.map X P ≠ 0
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
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ c • MemLp.toLp ⇑L ?hf = id c • MemLp.toLp ⇑L ⋯

pp: case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ MemLp (⇑L) p μ

Tactic:
;

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ c • MemLp.toLp ⇑L ?hf = id c • MemLp.toLp ⇑L ⋯

case hf
E : Type u_1
inst✝² : NormedAddCommGroup E
mE : MeasurableSpace E
μ✝ : Measure E
p✝ : ℝ≥0∞
𝕜 : Type u_2
inst✝¹ : NontriviallyNormedField 𝕜
inst✝ : NormedSpace 𝕜 E
μ : Measure E
p : ℝ≥0∞
h_Lp : MemLp id p μ
c : 𝕜
L : StrongDual 𝕜 E
⊢ MemLp (⇑L) p μ
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ Measure.map Y P ≠ 0

Tactic:
;

Goal state after:
case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ Measure.map Y P ≠ 0
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₁ v₁)

Tactic:
;

Goal state after:
case σf
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₁ v₁)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₂ v₂)

Tactic:
;

Goal state after:
case σg
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ SigmaFinite (gaussianReal m₂ v₂)
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
X Y : Ω → ℝ
hXY : X ⟂ᵢ[P] Y
hX : Measure.map X P = gaussianReal m₁ v₁
hY : Measure.map Y P = gaussianReal m₂ v₂
⊢ Measure.map (X + Y) P = gaussianReal (m₁ + m₂) (v₁ + v₂)

Tactic:
rw [hXY.map_add_eq_map_conv_map₀', hX, hY, gaussianReal_conv_gaussianReal]
  · apply AEMeasurable.of_map_ne_zero; simp [NeZero.ne, hX]
  · apply AEMeasurable.of_map_ne_zero; simp [NeZero.ne, hY]
  · rw [hX]; apply IsFiniteMeasure.toSigmaFinite
  · rw [hY]; apply IsFiniteMeasure.toSigmaFinite

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
inst✝ : IsProbabilityMeasure μ
c x✝² x✝¹ : E
h : MemLp (id ∘ fun x ↦ c + x) 2 μ
x✝ : E
⊢ id x✝ = ((fun x ↦ -c) + id ∘ fun x ↦ c + x) x✝

Tactic:
;

Goal state after:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
μ : Measure E
inst✝¹ : CompleteSpace E
inst✝ : IsProbabilityMeasure μ
c x✝² x✝¹ : E
h : MemLp (id ∘ fun x ↦ c + x) 2 μ
x✝ : E
⊢ id x✝ = ((fun x ↦ -c) + id ∘ fun x ↦ c + x) x✝
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case hb
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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ essSup (fun x ↦ ‖L‖ₑ * ‖x‖ₑ) μ ≠ ∞

pp: case h
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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ essSup (fun x ↦ ‖L x‖ₑ) μ ≤ essSup (fun x ↦ ‖L‖ₑ * ‖x‖ₑ) μ

Tactic:
· rw [ENNReal.essSup_const_mul]
      exact ENNReal.mul_ne_top (by simp) h_Lp.eLpNorm_ne_top

Goal state after:
case h
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
hp : ¬p = 0
hp_top : p = ∞
h_Lp : MemLp id ∞ μ
⊢ essSup (fun x ↦ ‖L x‖ₑ) μ ≤ essSup (fun x ↦ ‖L‖ₑ * ‖x‖ₑ) μ
Module: Mathlib.Probability.Moments.CovarianceBilin

Goal state before:
pp: ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[(fun u ↦ u.ofLp i) ∘ fun ω ↦ toLp 2 fun x ↦ X x ω, (fun u ↦ u.ofLp j) ∘ fun ω ↦ toLp 2 fun x ↦ X x ω; μ] =
    cov[X i, X j; μ]

Tactic:
;

Goal state after:
ι : Type u_2
Ω : Type u_3
inst✝¹ : Fintype ι
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : ι → Ω → ℝ
hX : ∀ (i : ι), MemLp (X i) 2 μ
i j : ι
this : ∀ (i : ι), AEMeasurable (X i) μ
⊢ cov[(fun u ↦ u.ofLp i) ∘ fun ω ↦ toLp 2 fun x ↦ X x ω, (fun u ↦ u.ofLp j) ∘ fun ω ↦ toLp 2 fun x ↦ X x ω; μ] =
    cov[X i, X j; μ]
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
L : StrongDual ℝ E
x✝ : E
⊢ (⇑L ∘ fun x ↦ x + c) x✝ = L x✝ + L c

Tactic:
;

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
L : StrongDual ℝ E
x✝ : E
⊢ (⇑L ∘ fun x ↦ x + c) x✝ = L x✝ + L c
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
hμ : ¬MemLp id 2 μ
⊢ (↑(covarianceOperator μ)).IsPositive

pp: case pos
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 μ)).IsPositive

Tactic:
;

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
hμ : ¬MemLp id 2 μ
⊢ (↑(covarianceOperator μ)).IsPositive

case pos
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 μ)).IsPositive
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ x + c) μ)

Tactic:
;

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ x + c) μ)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ x + -c) μ)

Tactic:
;

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
⊢ IsGaussian (Measure.map (fun x ↦ x + -c) μ)
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case hz
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
x : E
⊢ 0 ≤ p.toReal

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
x : E
⊢ ‖L x‖ₑ ^ p.toReal ≤ (‖L‖ₑ * ‖x‖ₑ) ^ p.toReal

Tactic:
;

Goal state after:
case hz
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
x : E
⊢ 0 ≤ p.toReal

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
x : E
⊢ ‖L x‖ₑ ^ p.toReal ≤ (‖L‖ₑ * ‖x‖ₑ) ^ p.toReal
Module: Mathlib.Probability.Moments.CovarianceBilinDual

Goal state before:
pp: case hf
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
⊢ Measurable fun x ↦ ‖x‖ₑ ^ p.toReal

Tactic:
;

Goal state after:
case hf
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
⊢ Measurable fun x ↦ ‖x‖ₑ ^ p.toReal
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:
;

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 ^ 2 * (‖p.1 + p.2‖ - ‖p.1 - p.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
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‖)

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

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 ∂μ
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 μ
⊢ 0 ≤ ‖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 μ
⊢ 0 ≤ ‖L₁‖ * ‖L₂‖ * ∫ (x : E), ‖x‖ ^ 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
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
⊢ (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 ≤ min ‖p.1‖ ‖p.2‖

Tactic:
have := norm_add_sub_norm_sub_le_two_mul_min p.1 p.2
      linarith

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

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

Tactic:
;

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