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

Goal state before:
pp: case insert
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ ∀ i ∈ s, MemLp (X i) 2 μ

pp: case insert.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp (X i) 2 μ

pp: case insert.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp (∑ x ∈ s, X x) 2 μ

pp: case insert.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp Y 2 μ

Tactic:
·

Goal state after:
case insert
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ ∀ i ∈ s, MemLp (X i) 2 μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEMeasurable X μ
⊢ Var[id; Measure.map X μ] = Var[X; μ]

Tactic:
by
  simp [variance_map measurable_id.aemeasurable hX]

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

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : MemLp X 2 μ
⊢ Var[X; μ] ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ Var[X; μ] ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : MemLp X 2 μ
⊢ Var[X; μ] ≤ ∫ (x : Ω), (X ^ 2) x ∂μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: case insert.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp (X i) 2 μ

pp: case insert.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp (∑ x ∈ s, X x) 2 μ

pp: case insert.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp Y 2 μ

Tactic:
·

Goal state after:
case insert.hX
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp (X i) 2 μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

pp: case neg.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ 0 ≤ᵐ[μ] fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2

pp: case neg.hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ AEStronglyMeasurable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2) μ

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ
Module: Mathlib.Probability.Independence.Integration

Goal state before:
pp: case pos
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : Integrable f (Measure.map X μ)
hg : Integrable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
⊢ ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)

pp: case neg
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : Integrable f (Measure.map X μ)
hg : Integrable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ¬∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
⊢ ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
𝕜 : Type u_2
inst✝¹⁴ : RCLike 𝕜
mΩ : MeasurableSpace Ω
μ : Measure Ω
𝓧 : Type u_3
𝓨 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst✝¹³ : MeasurableSpace 𝓧
inst✝¹² : MeasurableSpace 𝓨
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℝ E
inst✝⁹ : NormedSpace 𝕜 E
inst✝⁸ : CompleteSpace E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : CompleteSpace F
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : CompleteSpace G
X : Ω → 𝓧
Y : Ω → 𝓨
f : 𝓧 → E
g : 𝓨 → F
hXY : X ⟂ᵢ[μ] Y
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
hf : Integrable f (Measure.map X μ)
hg : Integrable g (Measure.map Y μ)
B : E →L[𝕜] F →L[𝕜] G
h : ∀ᵐ (ω : Ω) ∂μ, f (X ω) = 0
⊢ ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : ¬Integrable X μ
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : ¬Integrable X μ
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ ∫ (a : Ω), (X a - ∫ (x : Ω), X x ∂μ) ^ 2 ∂μ ≤ ∫ (x : Ω), (X ^ 2) x ∂μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: case insert.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp (∑ x ∈ s, X x) 2 μ

pp: case insert.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp Y 2 μ

Tactic:
·

Goal state after:
case insert.hY
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp (∑ x ∈ s, X x) 2 μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ 0 ≤ ∫ (x : Ω), (X ^ 2) x ∂μ

pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ ¬Integrable (fun a ↦ (X a - ∫ (x : Ω), X x ∂μ) ^ 2) μ

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ 0 ≤ ∫ (x : Ω), (X ^ 2) x ∂μ
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: case insert.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp Y 2 μ

Tactic:
·

Goal state after:
case insert.hZ
Ω : Type u_1
mΩ : MeasurableSpace Ω
Y : Ω → ℝ
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s✝ : Finset ι
inst✝ : IsFiniteMeasure μ
hY : MemLp Y 2 μ
i : ι
s : Finset ι
hi : i ∉ s
h_ind : (∀ i ∈ s, MemLp (X i) 2 μ) → cov[∑ i ∈ s, X i, Y; μ] = ∑ i ∈ s, cov[X i, Y; μ]
hX : ∀ i_1 ∈ insert i s, MemLp (X i_1) 2 μ
⊢ MemLp Y 2 μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case neg.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ 0 ≤ᵐ[μ] fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2

pp: case neg.hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ AEStronglyMeasurable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2) μ

Tactic:
·

Goal state after:
case neg.hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ 0 ≤ᵐ[μ] fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case neg.hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ AEStronglyMeasurable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2) μ

Tactic:
·

Goal state after:
case neg.hfm
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ AEStronglyMeasurable (fun ω ↦ (X ω - ∫ (x : Ω), X x ∂μ) ^ 2) μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst✝ : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
⊢ ∑ i ∈ s, cov[X i, ∑ j ∈ t, Y j; μ] = ∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ]

pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst✝ : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
⊢ MemLp (∑ j ∈ t, Y j) 2 μ

Tactic:
·

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst✝ : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
⊢ ∑ i ∈ s, cov[X i, ∑ j ∈ t, Y j; μ] = ∑ i ∈ s, ∑ j ∈ t, cov[X i, Y j; μ]
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), (X ^ 2) x ∂μ) = ENNReal.ofReal (∫ (a : Ω), ↑‖X a ^ 2‖₊ ∂μ)

pp: case pos.e_a.hfi
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ Integrable (fun x ↦ ↑‖X x ^ 2‖₊) μ

Tactic:
·

Goal state after:
case pos.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), (X ^ 2) x ∂μ) = ENNReal.ofReal (∫ (a : Ω), ↑‖X a ^ 2‖₊ ∂μ)
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos.e_a.hfi
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ Integrable (fun x ↦ ↑‖X x ^ 2‖₊) μ

Tactic:
·

Goal state after:
case pos.e_a.hfi
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ Integrable (fun x ↦ ↑‖X x ^ 2‖₊) μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)

Tactic:
·

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ - ENNReal.ofReal ((∫ (x : Ω), X x ∂μ) ^ 2)
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst✝ : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
⊢ MemLp (∑ j ∈ t, Y j) 2 μ

Tactic:
·

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
s : Finset ι
inst✝ : IsFiniteMeasure μ
ι' : Type u_3
Y : ι' → Ω → ℝ
t : Finset ι'
hX : ∀ i ∈ s, MemLp (X i) 2 μ
hY : ∀ i ∈ t, MemLp (Y i) 2 μ
⊢ MemLp (∑ j ∈ t, Y j) 2 μ
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x ↦ ∫ (x : Ω), X x ∂μ) μ
⊢ μ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} = μ {x | ↑c ≤ ‖(X - fun x ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ}

pp: case e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x ↦ ∫ (x : Ω), X x ∂μ) μ
⊢ eVar[X; μ] / ↑c ^ 2 = (↑c)⁻¹ ^ ENNReal.toReal 2 * eLpNorm (X - fun x ↦ ∫ (x : Ω), X x ∂μ) 2 μ ^ ENNReal.toReal 2

Tactic:
·

Goal state after:
case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : ↑c ≠ 0
B : AEStronglyMeasurable (fun x ↦ ∫ (x : Ω), X x ∂μ) μ
⊢ μ {ω | ↑c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} = μ {x | ↑c ≤ ‖(X - fun x ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ}
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ μ {ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} = μ {ω | ↑c.toNNReal ≤ |X ω - ∫ (x : Ω), X x ∂μ|}

pp: case e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ eVar[X; μ] / ENNReal.ofReal (c ^ 2) = eVar[X; μ] / ↑c.toNNReal ^ 2

Tactic:
·

Goal state after:
case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ μ {ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} = μ {ω | ↑c.toNNReal ≤ |X ω - ∫ (x : Ω), X x ∂μ|}
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ eVar[X; μ] / ENNReal.ofReal (c ^ 2) = eVar[X; μ] / ↑c.toNNReal ^ 2

Tactic:
·

Goal state after:
case e'_4
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ eVar[X; μ] / ENNReal.ofReal (c ^ 2) = eVar[X; μ] / ↑c.toNNReal ^ 2
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : X =ᵐ[μ] 0
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]

pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᵐ[μ] 0
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : X =ᵐ[μ] 0
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᵐ[μ] 0
this : IsProbabilityMeasure μ
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]

Tactic:
variance_add hX hY,

Goal state after:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᵐ[μ] 0
this : IsProbabilityMeasure μ
⊢ Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ] = Var[X; μ] + Var[Y; μ]
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]

pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᵐ[μ] 0
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
⊢ 0 = ∑ i ∈ s, Var[X i; μ]

pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
⊢ ∑ i ∈ s, X i =ᵐ[μ] 0

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
⊢ 0 = ∑ i ∈ s, Var[X i; μ]
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
⊢ ∑ i ∈ s, X i =ᵐ[μ] 0

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
⊢ ∑ i ∈ s, X i =ᵐ[μ] 0
Module: Mathlib.Probability.Moments.Covariance

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ∀ᵐ (ω : Ω) ∂μ, X ω = 0
⊢ cov[X, Y; μ] = 0

pp: case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ¬∀ᵐ (ω : Ω) ∂μ, X ω = 0
⊢ cov[X, Y; μ] = 0

Tactic:
·

Goal state after:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X ⟂ᵢ[μ] Y
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h' : ∀ᵐ (ω : Ω) ∂μ, X ω = 0
⊢ cov[X, Y; μ] = 0
Module: Mathlib.Probability.Moments.Variance

Goal state before:
pp: case neg.inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
j : ι
hj2 : ¬X j =ᵐ[μ] 0
hs : ∀ i ∈ {j}, MemLp (X i) 2 μ
h : (↑{j}).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ {j}, X i =ᵐ[μ] 0
hj1 : j ∈ {j}
⊢ Var[∑ i ∈ {j}, X i; μ] = ∑ i ∈ {j}, Var[X i; μ]

pp: case neg.inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᵐ[μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᵐ[μ] 0
h' : s.Nontrivial
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]

Tactic:
·

Goal state after:
case neg.inl
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
j : ι
hj2 : ¬X j =ᵐ[μ] 0
hs : ∀ i ∈ {j}, MemLp (X i) 2 μ
h : (↑{j}).Pairwise fun i j ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ {j}, X i =ᵐ[μ] 0
hj1 : j ∈ {j}
⊢ Var[∑ i ∈ {j}, X i; μ] = ∑ i ∈ {j}, Var[X i; μ]