-- 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:
Ω : 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_1 ∈ s, 2 * (X k x * X x_1 x) ∂μ - 2 * ((∫ (x : Ω), X k x ∂μ) * ∫ (x : Ω), ∑ c ∈ s, X c x ∂μ) = 0

Tactic:
rw [integral_finset_sum s fun i 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 ∈ 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)) μ

Proof state:
case hY
Ω : 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
⊢ AEStronglyMeasurable (X i) μ

Tactic:
exact MemLp.aestronglyMeasurable (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) μ
⊢ ∫ (x : Ω), (X k ^ 2) x ∂μ + ∫ (x : Ω), ((∑ i ∈ s, X i) ^ 2) x ∂μ + ∫ (x : Ω), (2 * X k * ∑ i ∈ s, X i) x ∂μ -
      (∫ (x : Ω), X k x ∂μ + ∫ (x : Ω), (∑ i ∈ s, X i) x ∂μ) ^ 2 =
    Var[X k; μ] + Var[∑ i ∈ s, X i; μ] +
      (∫ (x : Ω), (2 * X k * ∑ i ∈ s, X i) x ∂μ - (2 * ∫ (x : Ω), X k x ∂μ) * ∫ (x : Ω), (∑ i ∈ s, X i) x ∂μ)

Tactic:
rw [variance_def' (hs _ (mem_insert_self _ _)),
  variance_def' (memLp_finset_sum' _ fun i hi => hs _ (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) μ
⊢ ∫ (x : Ω), (X k ^ 2) x ∂μ + ∫ (x : Ω), ((∑ i ∈ s, X i) ^ 2) x ∂μ + ∫ (x : Ω), (2 * X k * ∑ i ∈ s, X i) x ∂μ -
      (∫ (x : Ω), X k x ∂μ + ∫ (x : Ω), (∑ i ∈ s, X i) x ∂μ) ^ 2 =
    ∫ (x : Ω), (X k ^ 2) x ∂μ - (∫ (x : Ω), X k x ∂μ) ^ 2 +
        (∫ (x : Ω), ((∑ i ∈ s, X i) ^ 2) x ∂μ - (∫ (x : Ω), (∑ i ∈ s, X i) x ∂μ) ^ 2) +
      (∫ (x : Ω), (2 * X k * ∑ i ∈ s, X i) x ∂μ - (2 * ∫ (x : Ω), X k x ∂μ) * ∫ (x : Ω), (∑ i ∈ s, X i) x ∂μ)

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) μ
⊢ Integrable (fun a => ∑ c ∈ s, (X k * X c) a) μ

Tactic:
apply integrable_finset_sum _ fun i 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
⊢ Integrable (X k * X 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 : ι
hi : i ∈ s
⊢ Integrable (X k * X i) μ

Tactic:
apply IndepFun.integrable_mul _ (MemLp.integrable one_le_two (hs _ (mem_insert_self _ _)))
  (MemLp.integrable one_le_two (hs _ (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
⊢ IndepFun (X k) (X 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

Tactic:
rw [integral_finset_sum s fun i hi =>
    MemLp.integrable one_le_two (hs _ (mem_insert_of_mem hi)),
  mul_sum, mul_sum, ← sum_sub_distrib]

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) μ
⊢ ∑ x ∈ s, (∫ (a : Ω), 2 * (X k a * X x a) ∂μ - 2 * ((∫ (x : Ω), X k x ∂μ) * ∫ (a : Ω), X x a ∂μ)) = 0