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

Tactic:
rw [mul_sum, sum_fn]

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

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 ^ 2 + (∑ i ∈ s, X i) ^ 2) μ

Tactic:
apply Integrable.add

Result:
case hf.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 ^ 2) μ

case hf.hg
Ω : 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 ((∑ i ∈ s, X i) ^ 2) μ

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

Tactic:
rw [integral_add', integral_add', integral_add']

Result:
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) μ

case hg
Ω : 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 (∑ i ∈ s, X i) μ

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 ^ 2) μ

case hg
Ω : 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 ((∑ i ∈ s, X i) ^ 2) μ

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 ^ 2 + (∑ i ∈ s, X i) ^ 2) μ

case hg
Ω : 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 (2 * X k * ∑ i ∈ s, X i) μ

Proof state:
case hX
Ω : 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 k) μ

Tactic:
exact MemLp.aestronglyMeasurable (hs _ (mem_insert_self _ _))

Result:
no goals

Proof state:
case hg
Ω : 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 (2 * (X k * ∑ i ∈ s, X i)) μ

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

Proof state:
case hf.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 ^ 2) μ

Tactic:
exact MemLp.integrable_sq (hs _ (mem_insert_self _ _))

Result:
no goals