awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
hμm : ¬IsFiniteMeasure μ
⊢ Var[fun (x : Ω) ↦ c; μ | m] = 0

Tactic:
simp [condVar, condExp_of_not_integrable, integrable_const_iff_isFiniteMeasure hc,
      integrable_const_iff_isFiniteMeasure <| pow_ne_zero _ hc, hμm, Pi.pow_def]

Premises used: pow_ne_zero, MeasureTheory.condExp_of_not_integrable, MeasureTheory.integrable_const_iff_isFiniteMeasure, ProbabilityTheory.condVar, Pi.pow_def
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ StronglyMeasurable Var[X; μ | m]

Tactic:
stronglyMeasurable_condExp

Premises used: MeasureTheory.stronglyMeasurable_condExp, ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
h₁ :
  ∀ (ω : Ω) (hω : X ω = Y ω) (hω' : μ[X | m] ω = μ[Y | m] ω),
    HPow.hPow (β := ℕ) (X - μ[X | m]) 2 ω = HPow.hPow (β := ℕ) (Y - μ[Y | m]) 2 ω
⊢ HPow.hPow (β := ℕ) (X - μ[X | m]) 2 =ᶠ[ae μ] HPow.hPow (β := ℕ) (Y - μ[Y | m]) 2

Tactic:
filter_upwards [h, condExp_congr_ae h] with ω hω hω'

Premises used: MeasureTheory.condExp_congr_ae
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
ω : Ω
hω : X ω = Y ω
hω' : μ[X | m] ω = μ[Y | m] ω
h₁ : HPow.hPow (β := ℕ) (Y ω - μ[X | m] ω) 2 = HPow.hPow (β := ℕ) (Y ω - μ[Y | m] ω) 2
h₂ h₃ : HPow.hPow (β := ℕ) (Y ω - μ[Y | m] ω) 2 = HPow.hPow (β := ℕ) (Y ω - μ[Y | m] ω) 2
⊢ HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2 = HPow.hPow (β := ℕ) (Y ω - μ[Y | m] ω) 2

Tactic:
rw [hω, hω']
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
hm : m ≤ m₀
X : Ω → ℝ
μ : Measure Ω
hμm : SigmaFinite (μ.trim hm)
hX : AEStronglyMeasurable X μ
hXint : Integrable (HPow.hPow (β := ℕ) (X - μ[X | m]) 2) μ
⊢ Var[X; μ | m] =ᶠ[ae μ] HPow.hPow (β := ℕ) (X - μ[X | m]) 2

Tactic:
condExp_of_aestronglyMeasurable' _ ((continuous_pow _).comp_aestronglyMeasurable
    (hX.sub stronglyMeasurable_condExp.aestronglyMeasurable)) hXint

Premises used: MeasureTheory.condExp_of_aestronglyMeasurable', ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ Integrable Var[X; μ | m] μ

Tactic:
integrable_condExp

Premises used: MeasureTheory.integrable_condExp, ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
hm : m ≤ m₀
X : Ω → ℝ
μ : Measure Ω
s : Set Ω
inst : SigmaFinite (μ.trim hm)
hX : Integrable (HPow.hPow (β := ℕ) (X - μ[X | m]) 2) μ
hs : MeasurableSet s
⊢ Eq (α := ℝ) (∫ (ω : Ω) in s, Var[X; μ | m] ω ∂μ) (∫ (ω : Ω) in s, HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2 ∂μ)

Tactic:
setIntegral_condExp _ hX hs

Premises used: MeasureTheory.setIntegral_condExp, ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
rw :
  μ[HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m] =
    μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m]
rw₁ rw₂ :
  μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] =
    μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m]
⊢ Var[X; μ | m] = μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m]

Tactic:
rw [condVar, sub_sq]

Premises used: sub_sq, ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ Integrable (HPow.hPow (β := ℕ) X 2) μ

Tactic:
have aux₀ : Integrable (X ^ 2) μ := hX.integrable_sq
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
rw : Integrable (2 * (X * μ[X | m])) μ
⊢ Integrable (2 * X * μ[X | m]) μ

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
⊢ Integrable (2 * (X * μ[X | m])) μ

Tactic:
(memLp_one_iff_integrable.1 <| hX.condExp.mul hX).const_mul _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.MemLp.mul, MeasureTheory.MemLp.condExp, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
⊢ Integrable (2 * (X * μ[X | m])) μ

Tactic:
exact (memLp_one_iff_integrable.1 <| hX.condExp.mul hX).const_mul _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.MemLp.mul, MeasureTheory.MemLp.condExp, Iff.mp, MeasureTheory.memLp_one_iff_integrable
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
⊢ Integrable (2 * X * μ[X | m]) μ

Tactic:
have aux₁ : Integrable (2 * X * μ[X | m]) μ := by
        rw [mul_assoc]
        exact (memLp_one_iff_integrable.1 <| hX.condExp.mul hX).const_mul _
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
⊢ Integrable (HPow.hPow (β := ℕ) μ[X | m] 2) μ

Tactic:
have aux₂ : Integrable (μ[X | m] ^ 2) μ := hX.condExp.integrable_sq
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
aux₂ : Integrable (HPow.hPow (β := ℕ) μ[X | m] 2) μ
h :
  ∀ (ω : Ω)
    (hω₀ :
      μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] ω =
        (μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] | m] + μ[HPow.hPow (β := ℕ) μ[X | m] 2 | m]) ω)
    (hω₁ :
      μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] | m] ω = (μ[HPow.hPow (β := ℕ) X 2 | m] - μ[2 * X * μ[X | m] | m]) ω)
    (hω₂ : μ[2 * X * μ[X | m] | m] ω = (μ[2 * X | m] * μ[X | m]) ω)
    (hω₃ : μ[OfNat.ofNat 2 * X | m] ω = HMul.hMul (α := Ω → ℝ) (OfNat.ofNat 2) μ[X | m] ω),
    μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] ω =
      (μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2) ω
⊢ μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] =ᶠ[ae μ]
    μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2

Tactic:
filter_upwards [condExp_add (m := m) (aux₀.sub aux₁) aux₂, condExp_sub (m := m) aux₀ aux₁,
        condExp_mul_of_stronglyMeasurable_right stronglyMeasurable_condExp aux₁
          ((hX.integrable one_le_two).const_mul _), condExp_ofNat (m := m) 2 X]
        with ω hω₀ hω₁ hω₂ hω₃

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.MemLp.integrable, MeasureTheory.condExp_mul_of_stronglyMeasurable_right, MeasureTheory.condExp_ofNat, MeasureTheory.Integrable.sub, MeasureTheory.condExp_add, MeasureTheory.stronglyMeasurable_condExp, one_le_two, OfNat.ofNat, MeasureTheory.condExp_sub
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
aux₂ : Integrable (HPow.hPow (β := ℕ) μ[X | m] 2) μ
ω : Ω
hω₀ :
  μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] ω =
    (μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] | m] + μ[HPow.hPow (β := ℕ) μ[X | m] 2 | m]) ω
hω₁ : μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] | m] ω = (μ[HPow.hPow (β := ℕ) X 2 | m] - μ[2 * X * μ[X | m] | m]) ω
hω₂ : μ[2 * X * μ[X | m] | m] ω = (μ[2 * X | m] * μ[X | m]) ω
hω₃ : μ[OfNat.ofNat 2 * X | m] ω = HMul.hMul (α := Ω → ℝ) (OfNat.ofNat 2) μ[X | m] ω
h : OfNat.ofNat 2 * μ[X | m] ω * μ[X | m] ω = 2 * HPow.hPow (β := ℕ) (μ[X | m] ω) 2
⊢ μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] ω =
    (μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2) ω

Tactic:
simp [hω₀, hω₁, hω₂, hω₃,
        condExp_of_stronglyMeasurable hm (stronglyMeasurable_condExp.pow _) aux₂]

Premises used: MeasureTheory.condExp_of_stronglyMeasurable, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.pow
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
aux₂ : Integrable (HPow.hPow (β := ℕ) μ[X | m] 2) μ
ω : Ω
hω₀ :
  μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] ω =
    (μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] | m] + μ[HPow.hPow (β := ℕ) μ[X | m] 2 | m]) ω
hω₁ : μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] | m] ω = (μ[HPow.hPow (β := ℕ) X 2 | m] - μ[2 * X * μ[X | m] | m]) ω
hω₂ : μ[2 * X * μ[X | m] | m] ω = (μ[2 * X | m] * μ[X | m]) ω
hω₃ : μ[OfNat.ofNat 2 * X | m] ω = HMul.hMul (α := Ω → ℝ) (OfNat.ofNat 2) μ[X | m] ω
⊢ OfNat.ofNat 2 * μ[X | m] ω * μ[X | m] ω = 2 * HPow.hPow (β := ℕ) (μ[X | m] ω) 2

Tactic:
simp [mul_assoc, sq]

Premises used: mul_assoc, sq
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2 =
    μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2

Tactic:
ring
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
μ₁ : Var[X; μ | m] = μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m]
μ₂ :
  μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] =ᶠ[ae μ]
    μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2
μ₃ :
  μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2 =
    μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2
⊢ Var[X; μ | m] =ᶠ[ae μ] μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2

Tactic:
calc
    Var[X; μ | m]
    _ = μ[X ^ 2 - 2 * X * μ[X | m] + μ[X | m] ^ 2 | m] := by rw [condVar, sub_sq]
    _ =ᵐ[μ] μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2 := by
      have aux₀ : Integrable (X ^ 2) μ := hX.integrable_sq
      have aux₁ : Integrable (2 * X * μ[X | m]) μ := by
        rw [mul_assoc]
        exact (memLp_one_iff_integrable.1 <| hX.condExp.mul hX).const_mul _
      have aux₂ : Integrable (μ[X | m] ^ 2) μ := hX.condExp.integrable_sq
      filter_upwards [condExp_add (m := m) (aux₀.sub aux₁) aux₂, condExp_sub (m := m) aux₀ aux₁,
        condExp_mul_of_stronglyMeasurable_right stronglyMeasurable_condExp aux₁
          ((hX.integrable one_le_two).const_mul _), condExp_ofNat (m := m) 2 X]
        with ω hω₀ hω₁ hω₂ hω₃
      simp [hω₀, hω₁, hω₂, hω₃,
        condExp_of_stronglyMeasurable hm (stronglyMeasurable_condExp.pow _) aux₂]
      simp [mul_assoc, sq]
    _ = μ[X ^ 2 | m] - μ[X | m] ^ 2 := by ring
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h :
  ∀ (ω : Ω) (hω : Var[X; μ | m] ω = (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) ω),
    Var[X; μ | m] ω ≤ μ[HPow.hPow (β := ℕ) X 2 | m] ω
⊢ Var[X; μ | m] ≤ᶠ[ae μ] μ[HPow.hPow (β := ℕ) X 2 | m]

Tactic:
filter_upwards [condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX] with ω hω

Premises used: ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
ω : Ω
hω : Var[X; μ | m] ω = μ[HPow.hPow (β := ℕ) X 2 | m] ω - HPow.hPow (β := ℕ) (μ[X | m] ω) 2
nlinarith :
  μ[HPow.hPow (β := ℕ) X 2 | m] ω < Var[X; μ | m] ω →
    0 - HPow.hPow (β := ℕ) (μ[X | m] ω) 2 +
          (Var[X; μ | m] ω - (μ[HPow.hPow (β := ℕ) X 2 | m] ω - HPow.hPow (β := ℕ) (μ[X | m] ω) 2)) +
        (μ[HPow.hPow (β := ℕ) X 2 | m] ω - Var[X; μ | m] ω) =
      0
⊢ Var[X; μ | m] ω ≤ μ[HPow.hPow (β := ℕ) X 2 | m] ω

Tactic:
nlinarith
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
e_a :
  Eq (α := ℝ) (∫ (x : Ω), Var[X; μ | m] x ∂μ)
    (∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ)
e_a₁ :
  Var[μ[X | m]; μ] =
    ∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2
⊢ ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] =
    ∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2)

Tactic:
congr 1
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Eq (α := ℝ) (∫ (x : Ω), Var[X; μ | m] x ∂μ)
    (∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ)

Tactic:
integral_congr_ae <| condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX

Premises used: MeasureTheory.integral_congr_ae, ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Eq (α := ℝ) (∫ (x : Ω), Var[X; μ | m] x ∂μ)
    (∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ)

Tactic:
exact integral_congr_ae <| condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX

Premises used: MeasureTheory.integral_congr_ae, ProbabilityTheory.condVar_ae_eq_condExp_sq_sub_sq_condExp
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Var[μ[X | m]; μ] =
    ∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2

Tactic:
variance_eq_sub hX.condExp

Premises used: ProbabilityTheory.variance_eq_sub, MeasureTheory.MemLp.condExp
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Var[μ[X | m]; μ] =
    ∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2

Tactic:
exact variance_eq_sub hX.condExp

Premises used: ProbabilityTheory.variance_eq_sub, MeasureTheory.MemLp.condExp
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
rw : Integrable (HPow.hPow (β := ℕ) μ[X | m] 2) μ
⊢ ∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ) +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)

Tactic:
rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm]

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.integral_condExp, MeasureTheory.integral_sub'
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Integrable (HPow.hPow (β := ℕ) μ[X | m] 2) μ

Tactic:
hX.condExp.integrable_sq

Premises used: MeasureTheory.MemLp.integrable_sq, MeasureTheory.MemLp.condExp
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ Integrable (HPow.hPow (β := ℕ) μ[X | m] 2) μ

Tactic:
exact hX.condExp.integrable_sq

Premises used: MeasureTheory.MemLp.integrable_sq, MeasureTheory.MemLp.condExp
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
rw :
  HSub.hSub (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ) +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
    ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
⊢ HSub.hSub (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ) +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
    Var[X; μ]

Tactic:
rw [variance_eq_sub hX]

Premises used: ProbabilityTheory.variance_eq_sub
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ HSub.hSub (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ) +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
    ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2

Tactic:
ring
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsProbabilityMeasure μ
hX : MemLp X 2 μ
μ₁ :
  ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] =
    ∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2)
μ₂ :
  ∫ (x : Ω), (μ[HPow.hPow (β := ℕ) X 2 | m] - HPow.hPow (β := ℕ) μ[X | m] 2) x ∂μ +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), μ[X | m] x ∂μ) 2) =
    HSub.hSub (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ) +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
μ₃ :
  HSub.hSub (α := ℝ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ) +
      (∫ (x : Ω), HPow.hPow (β := ℕ) μ[X | m] 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
    Var[X; μ]
⊢ ∫ (x : Ω), Var[X; μ | m] x ∂μ + Var[μ[X | m]; μ] = Var[X; μ]

Tactic:
calc
    μ[Var[X; μ | m]] + Var[μ[X | m]; μ]
    _ = μ[(μ[X ^ 2 | m] - μ[X | m] ^ 2 : Ω → ℝ)] + (μ[μ[X | m] ^ 2] - μ[μ[X | m]] ^ 2) := by
      congr 1
      · exact integral_congr_ae <| condVar_ae_eq_condExp_sq_sub_sq_condExp hm hX
      · exact variance_eq_sub hX.condExp
    _ = μ[X ^ 2] - μ[μ[X | m] ^ 2] + (μ[μ[X | m] ^ 2] - μ[X] ^ 2) := by
      rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm]
      exact hX.condExp.integrable_sq
    _ = Var[X; μ] := by rw [variance_eq_sub hX]; ring

Premises used: HSub.hSub, MeasureTheory.condExp, HPow.hPow, MeasureTheory.integral, OfNat.ofNat
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ : MeasurableSpace Ω
μ : Measure Ω
inst : NeZero μ
X : Ω → ℝ
⊢ Var[X; μ | ⊥] = fun (x : Ω) ↦ ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂μ) 2 ∂μ

Tactic:
simp [condVar, condExp_bot', average, measureReal_def]

Premises used: MeasureTheory.average, MeasureTheory.measureReal_def, MeasureTheory.condExp_bot', ProbabilityTheory.condVar
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inl :
  condVar (m₀ := m₀) ⊥ X 0 =ᶠ[ae (F := Measure Ω) 0] fun (x : Ω) ↦
    ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂0) 2 ∂0
inr :
  ∀ (hμ : NeZero μ), Var[X; μ | ⊥] =ᶠ[ae μ] fun (x : Ω) ↦ ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂μ) 2 ∂μ
⊢ Var[X; μ | ⊥] =ᶠ[ae μ] fun (x : Ω) ↦ ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂μ) 2 ∂μ

Tactic:
obtain rfl | hμ := eq_zero_or_neZero μ

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
inl : condVar (m₀ := m₀) ⊥ X 0 =ᶠ[⊥] fun (x : Ω) ↦ ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂0) 2 ∂0
⊢ condVar (m₀ := m₀) ⊥ X 0 =ᶠ[ae (F := Measure Ω) 0] fun (x : Ω) ↦
    ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂0) 2 ∂0

Tactic:
rw [ae_zero]

Premises used: MeasureTheory.ae_zero
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
⊢ condVar (m₀ := m₀) ⊥ X 0 =ᶠ[⊥] fun (x : Ω) ↦ ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂0) 2 ∂0

Tactic:
eventually_bot

Premises used: Filter.EventuallyEq, Filter.eventually_bot
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
⊢ condVar (m₀ := m₀) ⊥ X 0 =ᶠ[⊥] fun (x : Ω) ↦ ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂0) 2 ∂0

Tactic:
exact eventually_bot

Premises used: Filter.eventually_bot
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hμ : NeZero μ
⊢ Var[X; μ | ⊥] =ᶠ[ae μ] fun (x : Ω) ↦ ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂μ) 2 ∂μ

Tactic:
.of_forall <| congr_fun (condVar_bot' X)

Premises used: Filter.EventuallyEq, Filter.Eventually.of_forall, ProbabilityTheory.condVar_bot', congr_fun
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hμ : NeZero μ
⊢ Var[X; μ | ⊥] =ᶠ[ae μ] fun (x : Ω) ↦ ⨍ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ⨍ (ω' : Ω), X ω' ∂μ) 2 ∂μ

Tactic:
exact .of_forall <| congr_fun (condVar_bot' X)

Premises used: ProbabilityTheory.condVar_bot', congr_fun
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEMeasurable X μ
⊢ Var[X; μ | ⊥] = fun (_ω : Ω) ↦ Var[X; μ]

Tactic:
simp [condVar_bot', average_eq_integral, variance_eq_integral hX]

Premises used: ProbabilityTheory.variance_eq_integral, MeasureTheory.average_eq_integral, ProbabilityTheory.condVar_bot'
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ μ[HPow.hPow (β := ℕ) (c • X - μ[c • X | m]) 2 | m] =ᶠ[ae μ]
    μ[HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m]

Tactic:
condExp_congr_ae ?_

Premises used: MeasureTheory.condExp_congr_ae
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
refine :
  HPow.hPow (β := ℕ) (c • X - μ[c • X | m]) 2 =ᶠ[ae μ] HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2
⊢ μ[HPow.hPow (β := ℕ) (c • X - μ[c • X | m]) 2 | m] =ᶠ[ae μ]
    μ[HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m]

Tactic:
refine condExp_congr_ae ?_

Premises used: MeasureTheory.condExp_congr_ae
-- Module: Mathlib.Probability.CondVar
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
h :
  ∀ (ω : Ω) (hω : μ[c • X | m] ω = (c • μ[X | m]) ω),
    HPow.hPow (β := ℕ) (c • X - μ[c • X | m]) 2 ω = (HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2) ω
⊢ HPow.hPow (β := ℕ) (c • X - μ[c • X | m]) 2 =ᶠ[ae μ] HPow.hPow (β := ℕ) c 2 • HPow.hPow (β := ℕ) (X - μ[X | m]) 2

Tactic:
filter_upwards [condExp_smul (m := m) c X] with ω hω

Premises used: MeasureTheory.condExp_smul