-- Mathlib/Probability/Variance.lean
theorem IndepFun.variance_sum [IsProbabilityMeasure μ] {ι : Type*} {X : ι → Ω → ℝ}
    {s : Finset ι} (hs : ∀ i ∈ s, MemLp (X i) 2 μ)
    (h : Set.Pairwise ↑s fun i j => IndepFun (X i) (X j) μ) :
    variance (∑ i ∈ s, X i) μ = ∑ i ∈ s, variance (X i) μ

Proof state:
case insert
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ ∫ (x : Ω), ((X k + ∑ x ∈ s, X x) ^ 2) x ∂μ - (∫ (x : Ω), (X k + ∑ x ∈ s, X x) x ∂μ) ^ 2 =
    Var[X k; μ] + ∑ x ∈ s, Var[X x; μ]

Tactic:
simp only [add_sq']

Result:
case insert
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ ∫ (x : Ω), (X k ^ 2 + (∑ x ∈ s, X x) ^ 2 + 2 * X k * ∑ x ∈ s, X x) x ∂μ - (∫ (x : Ω), (X k + ∑ x ∈ s, X x) x ∂μ) ^ 2 =
    Var[X k; μ] + ∑ x ∈ s, Var[X x; μ]

Proof state:
case hf.hg.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ MemLp (∑ i ∈ s, X i) 2 μ

Tactic:
exact memLp_finset_sum' _ fun i hi => hs _ (mem_insert_of_mem hi)

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
i : ι
hi : i ∈ s
⊢ IndepFun (X k) (X i) μ

Tactic:
apply h (mem_insert_self _ _) (mem_insert_of_mem hi)

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
i : ι
hi : i ∈ s
⊢ k ≠ i

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ ∑ i ∈ s, ∫ (a : Ω), 2 * (X k a * X i a) ∂μ - 2 * ((∫ (x : Ω), X k x ∂μ) * ∫ (x : Ω), ∑ c ∈ s, X c x ∂μ) = 0

Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
i : ι
hi : i ∈ s
⊢ Integrable (fun x => 2 * (X k x * X i x)) μ

Tactic:
swap

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
i : ι
hi : i ∈ s
⊢ Integrable (fun x => 2 * (X k x * X i x)) μ

Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ ∑ i ∈ s, ∫ (a : Ω), 2 * (X k a * X i a) ∂μ - 2 * ((∫ (x : Ω), X k x ∂μ) * ∫ (x : Ω), ∑ c ∈ s, X c x ∂μ) = 0

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
i : ι
hi : i ∈ s
⊢ Integrable (fun x => 2 * (X k x * X i x)) μ

Tactic:
apply Integrable.const_mul _ (2 : ℝ)

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
i : ι
hi : i ∈ s
⊢ Integrable (fun x => X k x * X i x) μ

Proof state:
case empty
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
hs : ∀ i ∈ ∅, MemLp (X i) 2 μ
h : (↑∅).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ Var[∑ i ∈ ∅, X i; μ] = ∑ i ∈ ∅, Var[X i; μ]

Tactic:
simp only [Finset.sum_empty, variance_zero]

Result:
no goals

Proof state:
case hg.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ MemLp (∑ i ∈ s, X i) 2 μ

Tactic:
exact memLp_finset_sum' _ fun i hi => hs _ (mem_insert_of_mem hi)

Result:
no goals

Proof state:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
⊢ Integrable (X k) μ

Tactic:
exact MemLp.integrable one_le_two (hs _ (mem_insert_self _ _))

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
ι : Type u_2
X : ι → Ω → ℝ
k : ι
s : Finset ι
ks : k ∉ s
IH :
  (∀ i ∈ s, MemLp (X i) 2 μ) →
    ((↑s).Pairwise fun i j => IndepFun (X i) (X j) μ) → Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
hs : ∀ i ∈ insert k s, MemLp (X i) 2 μ
h : (↑(insert k s)).Pairwise fun i j => IndepFun (X i) (X j) μ
i : ι
hi : i ∈ s
⊢ Integrable (X i) μ

Tactic:
exact MemLp.integrable one_le_two (hs _ (mem_insert_of_mem hi))

Result:
no goals