-- Mathlib/Probability/Variance.lean
theorem IndepFun.variance_add [IsProbabilityMeasure μ] {X Y : Ω → ℝ} (hX : MemLp X 2 μ)
    (hY : MemLp Y 2 μ) (h : IndepFun X Y μ) : variance (X + Y) μ = variance X μ + variance Y μ :=
  calc
    variance (X + Y) μ = μ[fun a => X a ^ 2 + Y a ^ 2 + 2 * X a * Y a] - μ[X + Y] ^ 2

Proof state:
case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable (fun a => Y a ^ 2) μ

Tactic:
exact hY.integrable_sq

Result:
no goals

Proof state:
case e_a.e_a.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ ∫ (x : Ω), (X * Y) x ∂μ = (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ

Tactic:
exact h.integral_mul_of_integrable (hX.integrable one_le_two) (hY.integrable one_le_two)

Result:
no goals

Proof state:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable (fun a => X a ^ 2) μ

Tactic:
exact hX.integrable_sq

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ ∫ (x : Ω), (fun a => X a ^ 2 + Y a ^ 2 + 2 * X a * Y a) x ∂μ - (∫ (x : Ω), (X + Y) x ∂μ) ^ 2 =
    ∫ (x : Ω), (X ^ 2) x ∂μ + ∫ (x : Ω), (Y ^ 2) x ∂μ + 2 * ∫ (x : Ω), (X * Y) x ∂μ -
      (∫ (x : Ω), X x ∂μ + ∫ (x : Ω), Y x ∂μ) ^ 2

Tactic:
simp only [Pi.add_apply, Pi.pow_apply, Pi.mul_apply, mul_assoc]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ ∫ (x : Ω), X x ^ 2 + Y x ^ 2 + 2 * (X x * Y x) ∂μ - (∫ (x : Ω), X x + Y x ∂μ) ^ 2 =
    ∫ (x : Ω), X x ^ 2 ∂μ + ∫ (x : Ω), Y x ^ 2 ∂μ + 2 * ∫ (x : Ω), X x * Y x ∂μ -
      (∫ (x : Ω), X x ∂μ + ∫ (x : Ω), Y x ∂μ) ^ 2

Proof state:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable X μ

Tactic:
exact hX.integrable one_le_two

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Var[X + Y; μ] = ∫ (x : Ω), (fun a => X a ^ 2 + Y a ^ 2 + 2 * X a * Y a) x ∂μ - (∫ (x : Ω), (X + Y) x ∂μ) ^ 2

Tactic:
simp [variance_def' (hX.add hY), add_sq']

Result:
no goals

Proof state:
case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable (fun x => 2 * (X x * Y x)) μ

Tactic:
apply Integrable.const_mul

Result:
case hg.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable (fun x => X x * Y x) μ

Proof state:
case hg.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable (fun x => X x * Y x) μ

Tactic:
exact h.integrable_mul (hX.integrable one_le_two) (hY.integrable one_le_two)

Result:
no goals

Proof state:
case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable Y μ

Tactic:
exact hY.integrable one_le_two

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ + ∫ (x : Ω), (Y ^ 2) x ∂μ + 2 * ((∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) -
      (∫ (x : Ω), X x ∂μ + ∫ (x : Ω), Y x ∂μ) ^ 2 =
    Var[X; μ] + Var[Y; μ]

Tactic:
simp only [variance_def', hX, hY, Pi.pow_apply]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ ∫ (x : Ω), X x ^ 2 ∂μ + ∫ (x : Ω), Y x ^ 2 ∂μ + 2 * ((∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) -
      (∫ (x : Ω), X x ∂μ + ∫ (x : Ω), Y x ∂μ) ^ 2 =
    ∫ (x : Ω), X x ^ 2 ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2 + (∫ (x : Ω), Y x ^ 2 ∂μ - (∫ (x : Ω), Y x ∂μ) ^ 2)

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ + ∫ (x : Ω), (Y ^ 2) x ∂μ + 2 * ∫ (x : Ω), (X * Y) x ∂μ -
      (∫ (x : Ω), X x ∂μ + ∫ (x : Ω), Y x ∂μ) ^ 2 =
    ∫ (x : Ω), (X ^ 2) x ∂μ + ∫ (x : Ω), (Y ^ 2) x ∂μ + 2 * ((∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) -
      (∫ (x : Ω), X x ∂μ + ∫ (x : Ω), Y x ∂μ) ^ 2

Tactic:
congr

Result:
case e_a.e_a.e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ ∫ (x : Ω), (X * Y) x ∂μ = (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ

Proof state:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable (fun x => X x ^ 2 + Y x ^ 2) μ

Tactic:
exact hX.integrable_sq.add hY.integrable_sq

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ ∫ (x : Ω), X x ^ 2 + Y x ^ 2 + 2 * (X x * Y x) ∂μ - (∫ (x : Ω), X x + Y x ∂μ) ^ 2 =
    ∫ (x : Ω), X x ^ 2 ∂μ + ∫ (x : Ω), Y x ^ 2 ∂μ + 2 * ∫ (x : Ω), X x * Y x ∂μ -
      (∫ (x : Ω), X x ∂μ + ∫ (x : Ω), Y x ∂μ) ^ 2

Tactic:
rw [integral_add, integral_add, integral_add, integral_mul_left]

Result:
case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable X μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable Y μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable (fun a => X a ^ 2) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable (fun a => Y a ^ 2) μ

case hf
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable (fun x => X x ^ 2 + Y x ^ 2) μ

case hg
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ Integrable (fun x => 2 * (X x * Y x)) μ

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝ : IsProbabilityMeasure μ
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : IndepFun X Y μ
⊢ ∫ (x : Ω), X x ^ 2 ∂μ + ∫ (x : Ω), Y x ^ 2 ∂μ + 2 * ((∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ) -
      (∫ (x : Ω), X x ∂μ + ∫ (x : Ω), Y x ∂μ) ^ 2 =
    ∫ (x : Ω), X x ^ 2 ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2 + (∫ (x : Ω), Y x ^ 2 ∂μ - (∫ (x : Ω), Y x ∂μ) ^ 2)

Tactic:
ring

Result:
no goals