awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
⊢ evariance (mΩ := mΩ) X 0 = 0

Tactic:
simp [evariance]

Premises used: ProbabilityTheory.evariance
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
⊢ variance (mΩ := mΩ) X 0 = 0

Tactic:
simp [variance]

Premises used: ProbabilityTheory.variance
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ HPow.hPow (β := ℕ) (eLpNorm (X - fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ) 2 < ∞

Tactic:
have := ENNReal.pow_lt_top (hX.sub <| memLp_const <| μ[X]).2 (n := 2)
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : HPow.hPow (β := ℕ) (eLpNorm (X - fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ) 2 < ∞
⊢ HPow.hPow (β := ℝ)
      ((∫⁻ (x : Ω), ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^
        (1 / ENNReal.toReal 2))
      2 <
    ∞

Tactic:
rw [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top, ← ENNReal.rpow_two]
    at this

Premises used: ENNReal.ofNat_ne_top, ENNReal.rpow_two, two_ne_zero, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
this :
  HPow.hPow (β := ℝ)
      ((∫⁻ (x : Ω), ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^
        (1 / ENNReal.toReal 2))
      2 <
    ∞
⊢ HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2 < ∞

Tactic:
simp only [ENNReal.toReal_ofNat, Pi.sub_apply, one_div] at this

Premises used: one_div, ENNReal.toReal_ofNat, Pi.sub_apply
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
this :
  HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2 < ∞
⊢ ∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ < ∞

Tactic:
rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_one] at this

Premises used: ENNReal.rpow_mul, ENNReal.rpow_one, two_ne_zero, inv_mul_cancel₀
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ < ∞
⊢ ∫⁻ (x : Ω), HPow.hPow (β := ℕ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ < ∞

Tactic:
simp_rw [ENNReal.rpow_two] at this

Premises used: ENNReal.rpow_two
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ∫⁻ (x : Ω), HPow.hPow (β := ℕ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ < ∞
⊢ eVar[X; μ] < ∞

Tactic:
this

Premises used: ProbabilityTheory.evariance
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ∫⁻ (x : Ω), HPow.hPow (β := ℕ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ < ∞
⊢ eVar[X; μ] < ∞

Tactic:
exact this
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] ≠ ∞

Tactic:
(evariance_lt_top hX).ne

Premises used: ProbabilityTheory.evariance_lt_top, LT.lt.ne
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
by_contra : ∀ (h : ¬eVar[X; μ] = ∞), False
⊢ eVar[X; μ] = ∞

Tactic:
by_contra h
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : ¬eVar[X; μ] = ∞
⊢ eVar[X; μ] < ∞

Tactic:
rw [← Ne, ← lt_top_iff_ne_top] at h

Premises used: Ne, lt_top_iff_ne_top
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
refine : eLpNorm (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ < ∞
⊢ MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ

Tactic:
refine ⟨by fun_prop, ?_⟩
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
rw : (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2) < ∞
⊢ eLpNorm (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ < ∞

Tactic:
rw [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top]

Premises used: ENNReal.ofNat_ne_top, two_ne_zero, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
simp : (∫⁻ (x : Ω), HPow.hPow (β := ℕ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) ^ HDiv.hDiv (α := ℝ) 1 2 < ∞
⊢ (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2) < ∞

Tactic:
simp only [ENNReal.toReal_ofNat, ENNReal.rpow_two]

Premises used: ENNReal.rpow_two, ENNReal.toReal_ofNat
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
linarith : HDiv.hDiv (α := ℝ) 1 2 < 0 → 2 / 2 = 1
linarith₁ : HDiv.hDiv (α := ℝ) 1 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HDiv.hDiv (α := ℝ) 1 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : HDiv.hDiv (α := ℝ) 1 2 < 0 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 2

Tactic:
linarith
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ (∫⁻ (x : Ω), HPow.hPow (β := ℕ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) ^ HDiv.hDiv (α := ℝ) 1 2 < ∞

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg (by linarith) h.ne

Premises used: ENNReal.rpow_lt_top_of_nonneg, LT.lt.ne
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ

Tactic:
have : MemLp (fun ω => X ω - μ[X]) 2 μ := by
    refine ⟨by fun_prop, ?_⟩
    rw [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top]
    simp only [ENNReal.toReal_ofNat, ENNReal.rpow_two]
    exact ENNReal.rpow_lt_top_of_nonneg (by linarith) h.ne
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
⊢ False

Tactic:
hX ?_
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
refine : MemLp X 2 μ
⊢ False

Tactic:
refine hX ?_
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
⊢ MemLp (HAdd.hAdd (α := Ω → ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ

Tactic:
this.add (memLp_const μ[X])

Premises used: MeasureTheory.MemLp.add, MeasureTheory.integral, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
h₁ : X = HAdd.hAdd (α := Ω → ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ
⊢ MemLp X 2 μ

Tactic:
convert! this.add (memLp_const μ[X])

Premises used: MeasureTheory.MemLp.add, MeasureTheory.integral, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
h₁ :
  ∀ (ω : Ω),
    X ω =
      HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) ω
⊢ X = HAdd.hAdd (α := Ω → ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ

Tactic:
ext ω
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
ω : Ω
h₁ : X ω = X ω - ∫ (x : Ω), X x ∂μ + ∫ (x : Ω), X x ∂μ
h₂ h₃ : X ω = X ω
⊢ X ω = HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) ω

Tactic:
rw [Pi.add_apply, sub_add_cancel]

Premises used: Pi.add_apply, sub_add_cancel
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
contrapose! : ¬MemLp X 2 μ → ∞ ≤ eVar[X; μ]
⊢ eVar[X; μ] < ∞ → MemLp X 2 μ

Tactic:
contrapose!
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
rw : ¬MemLp X 2 μ → eVar[X; μ] = ∞
⊢ ¬MemLp X 2 μ → ∞ ≤ eVar[X; μ]

Tactic:
rw [top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬MemLp X 2 μ → eVar[X; μ] = ∞

Tactic:
evariance_eq_top hX

Premises used: ProbabilityTheory.evariance_eq_top
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬MemLp X 2 μ → eVar[X; μ] = ∞

Tactic:
exact evariance_eq_top hX

Premises used: ProbabilityTheory.evariance_eq_top
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ eVar[X; μ] = ∞ ↔ ¬MemLp X 2 μ

Tactic:
simp [← evariance_lt_top_iff_memLp hX]

Premises used: ProbabilityTheory.evariance_lt_top_iff_memLp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
hX_not : ¬MemLp X 2 μ
⊢ Var[X; μ] = 0

Tactic:
simp [variance, (evariance_eq_top_iff hX).mpr hX_not]

Premises used: Iff.mpr, ProbabilityTheory.evariance_eq_top_iff, ProbabilityTheory.variance
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
h : Var[X; μ] ≠ 0
contrapose : ∀ (h : ¬MemLp X 2 μ), Var[X; μ] = 0
⊢ MemLp X 2 μ

Tactic:
contrapose h
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
h : ¬MemLp X 2 μ
⊢ Var[X; μ] = 0

Tactic:
variance_of_not_memLp hX h

Premises used: ProbabilityTheory.variance_of_not_memLp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
h : ¬MemLp X 2 μ
⊢ Var[X; μ] = 0

Tactic:
exact variance_of_not_memLp hX h

Premises used: ProbabilityTheory.variance_of_not_memLp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
rw : eVar[X; μ] ≠ ∞
⊢ ENNReal.ofReal Var[X; μ] = eVar[X; μ]

Tactic:
rw [variance, ENNReal.ofReal_toReal]

Premises used: ENNReal.ofReal_toReal, ProbabilityTheory.variance
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] ≠ ∞

Tactic:
evariance_ne_top hX

Premises used: ProbabilityTheory.evariance_ne_top
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] ≠ ∞

Tactic:
exact evariance_ne_top hX

Premises used: ProbabilityTheory.evariance_ne_top
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ eVar[X; μ] = ∫⁻ (ω : Ω), ENNReal.ofReal (HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) ∂μ

Tactic:
simp [evariance, ← enorm_pow, Real.enorm_of_nonneg (sq_nonneg _)]

Premises used: Real.enorm_of_nonneg, sq_nonneg, enorm_pow, ProbabilityTheory.evariance
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
⊢ Var[X; μ] = ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ

Tactic:
simp [variance, evariance, toReal_enorm, ← integral_toReal ((hX.sub_const _).enorm.pow_const _) <|
    .of_forall fun _ ↦ ENNReal.pow_lt_top enorm_lt_top]

Premises used: AEMeasurable.pow_const, AEMeasurable.enorm, toReal_enorm, ProbabilityTheory.variance, AEMeasurable.sub_const, ProbabilityTheory.evariance, MeasureTheory.integral_toReal
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : Var[X; μ] = 0
rw :
  ∀ (h : (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) 0),
    ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ
hf :
  ∀ (h : Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ) 0),
    LE.le.{u_1} (α := Ω → ℝ) 0 fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2
hfi :
  ∀ (h : Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ) 0),
    Integrable (ε := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) μ
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ

Tactic:
rw [variance_eq_integral hX.aemeasurable, integral_eq_zero_iff_of_nonneg] at h

Premises used: ProbabilityTheory.variance_eq_integral, MeasureTheory.integral_eq_zero_iff_of_nonneg, MeasureTheory.MemLp.aemeasurable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) 0
h₁ : ∀ (ω : Ω) (hω : HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 = 0 ω), X ω = ∫ (x : Ω), X x ∂μ
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ

Tactic:
filter_upwards [h] with ω hω
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) 0
ω : Ω
hω : HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 = 0 ω
⊢ X ω - ∫ (x : Ω), X x ∂μ = 0

Tactic:
simp at hω
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) 0
ω : Ω
hω : X ω - ∫ (x : Ω), X x ∂μ = 0
⊢ X ω = ∫ (x : Ω), X x ∂μ

Tactic:
grind
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ) 0
x : Ω
⊢ 0 x ≤ HPow.hPow (β := ℕ) (X x - ∫ (x : Ω), X x ∂μ) 2

Tactic:
positivity
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ) 0
⊢ LE.le.{u_1} (α := Ω → ℝ) 0 fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2

Tactic:
exact fun _ ↦ by positivity
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ) 0
hfi :
  Integrable (ε := ℝ)
    (fun (ω : Ω) ↦
      HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * ∫ (x : Ω), X x ∂μ + HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
    μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) μ

Tactic:
simp_rw [sub_sq]

Premises used: sub_sq
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ) 0
⊢ LE.le (α := ℝ≥0∞) 1 2

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ) 0
⊢ Integrable (ε := ℝ)
    (fun (ω : Ω) ↦
      HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * ∫ (x : Ω), X x ∂μ + HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
    μ

Tactic:
exact (hX.integrable_sq.sub (((hX.integrable (by simp)).const_mul _).mul_const _)).add
      (integrable_const _)

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.MemLp.integrable, MeasureTheory.Integrable.sub, MeasureTheory.MemLp.integrable_sq, MeasureTheory.Integrable.add, MeasureTheory.Integrable.mul_const, MeasureTheory.integrable_const
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
hXint : Eq (α := ℝ) (∫ (x : Ω), X x ∂μ) 0
⊢ Var[X; μ] = ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 ∂μ

Tactic:
simp [variance_eq_integral hX, hXint]

Premises used: ProbabilityTheory.variance_eq_integral
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ eVar[0; μ] = 0

Tactic:
simp [evariance]

Premises used: ProbabilityTheory.evariance
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hX : AEMeasurable X μ
⊢ eVar[X; μ] = 0 ↔ X =ᶠ[ae μ] fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ

Tactic:
simp [evariance, lintegral_eq_zero_iff' ((hX.sub_const _).enorm.pow_const _), EventuallyEq,
    sub_eq_zero]

Premises used: AEMeasurable.pow_const, AEMeasurable.enorm, sub_eq_zero, MeasureTheory.lintegral_eq_zero_iff', Filter.EventuallyEq, AEMeasurable.sub_const, ProbabilityTheory.evariance
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
rw :
  ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ 2 ∂μ =
    ∫⁻ (a : Ω), ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X a - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ
⊢ eVar[fun (ω : Ω) ↦ c * X ω; μ] = ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * eVar[X; μ]

Tactic:
rw [evariance, evariance, ← lintegral_const_mul' _ _ ENNReal.ofReal_lt_top.ne]

Premises used: MeasureTheory.lintegral_const_mul', ENNReal.ofReal_lt_top, ProbabilityTheory.evariance, LT.lt.ne
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
e_f :
  ∀ (ω : Ω),
    HPow.hPow (β := ℕ) ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ 2 =
      ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ 2
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ 2 ∂μ =
    ∫⁻ (a : Ω), ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X a - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ

Tactic:
congr with ω
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
e_f :
  HPow.hPow (β := ℕ) ‖c * X ω - c * ∫ (a : Ω), X a ∂μ‖ₑ 2 =
    ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ 2
e_f₁ :
  HPow.hPow (β := ℕ) ‖c * (X ω - ∫ (a : Ω), X a ∂μ)‖ₑ 2 =
    ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ 2
e_f₂ :
  HPow.hPow (β := ℕ) (‖c‖ₑ * ‖X ω - ∫ (a : Ω), X a ∂μ‖ₑ) 2 =
    ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ 2
e_f₃ :
  HPow.hPow (β := ℕ) ‖c‖ₑ 2 * HPow.hPow (β := ℕ) ‖X ω - ∫ (a : Ω), X a ∂μ‖ₑ 2 =
    ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ 2
e_f₄ :
  ‖HPow.hPow (β := ℕ) c 2‖ₑ * HPow.hPow (β := ℕ) ‖X ω - ∫ (a : Ω), X a ∂μ‖ₑ 2 =
    ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ 2
e_f₅ e_f₆ :
  ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X ω - ∫ (a : Ω), X a ∂μ‖ₑ 2 =
    ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ 2
⊢ HPow.hPow (β := ℕ) ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ 2 =
    ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ 2

Tactic:
rw [integral_const_mul, ← mul_sub, enorm_mul, mul_pow, ← enorm_pow,
    Real.enorm_of_nonneg (sq_nonneg _)]

Premises used: enorm_mul, MeasureTheory.integral_const_mul, mul_sub, Real.enorm_of_nonneg, sq_nonneg, enorm_pow, mul_pow
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ Var[0; μ] = 0

Tactic:
simp only [variance, evariance_zero, ENNReal.toReal_zero]

Premises used: ProbabilityTheory.variance, ProbabilityTheory.evariance_zero, ENNReal.toReal_zero
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEMeasurable X μ
rw :
  Eq (α := ℝ) (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (X ω - ∫ (x : Ω), X x ∂μ) ∂μ)
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ)
⊢ cov[X, X; μ] = Var[X; μ]

Tactic:
rw [covariance, variance_eq_integral hX]

Premises used: ProbabilityTheory.variance_eq_integral, ProbabilityTheory.covariance
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEMeasurable X μ
e_f : ∀ (x : Ω), (X x - ∫ (x : Ω), X x ∂μ) * (X x - ∫ (x : Ω), X x ∂μ) = HPow.hPow (β := ℕ) (X x - ∫ (x : Ω), X x ∂μ) 2
⊢ Eq (α := ℝ) (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (X ω - ∫ (x : Ω), X x ∂μ) ∂μ)
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ)

Tactic:
congr with x
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEMeasurable X μ
x : Ω
⊢ (X x - ∫ (x : Ω), X x ∂μ) * (X x - ∫ (x : Ω), X x ∂μ) = HPow.hPow (β := ℕ) (X x - ∫ (x : Ω), X x ∂μ) 2

Tactic:
ring
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ 0 ≤ Var[X; μ]

Tactic:
ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg, ProbabilityTheory.variance