awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬eLpNorm X 2 μ < ∞
⊢ (¬¬∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x‖ₑ 2 ∂μ = 0 → LE.le (α := ℝ) 0 2) →
    ∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x‖ₑ 2 ∂μ = ∞

Tactic:
simp only [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top, not_lt,
      top_le_iff, ENNReal.toReal_ofNat, one_div, ENNReal.rpow_eq_top_iff, inv_lt_zero, inv_pos,
      and_true, or_iff_not_imp_left, not_and_or, zero_lt_two] at hℒ

Premises used: ENNReal.ofNat_ne_top, and_true, inv_pos, ENNReal.rpow_eq_top_iff, two_ne_zero, not_lt, Classical.or_iff_not_imp_left, not_and_or, one_div, inv_lt_zero, top_le_iff, ENNReal.toReal_ofNat, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal, zero_lt_two
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ :
  (¬¬∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x‖ₑ 2 ∂μ = 0 → LE.le (α := ℝ) 0 2) →
    ∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x‖ₑ 2 ∂μ = ∞
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ = ∞

Tactic:
mod_cast hℒ fun _ => zero_le_two

Premises used: congrArg, ENNReal.rpow_natCast, cast, funext, ENorm.enorm, zero_le_two, congrFun', Top.top, OfNat.ofNat, Eq, MeasureTheory.lintegral
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ :
  (¬¬∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x‖ₑ 2 ∂μ = 0 → LE.le (α := ℝ) 0 2) →
    ∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x‖ₑ 2 ∂μ = ∞
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ = ∞

Tactic:
exact mod_cast hℒ fun _ => zero_le_two

Premises used: zero_le_two
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
rwa : ¬(↑c : ℝ≥0∞) = 0
rwa₁ rwa₂ rwa₃ rwa₄ : ¬c = 0
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
rwa [Ne, ENNReal.coe_eq_zero]

Premises used: Ne, ENNReal.coe_eq_zero
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
⊢ (↑c : ℝ≥0∞) ≠ 0

Tactic:
have A : (c : ℝ≥0∞) ≠ 0 := by rwa [Ne, ENNReal.coe_eq_zero]
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : (↑c : ℝ≥0∞) ≠ 0
⊢ AEStronglyMeasurable (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) μ

Tactic:
have B : AEStronglyMeasurable (fun _ : Ω => μ[X]) μ := aestronglyMeasurable_const
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : (↑c : ℝ≥0∞) ≠ 0
B : AEStronglyMeasurable (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) μ
⊢ (↑c : ℝ≥0∞) = ∞ →
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set Ω) → ℝ≥0∞) {x : Ω | ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ = ∞} : ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : (↑c : ℝ≥0∞) ≠ 0
B : AEStronglyMeasurable (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) μ
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) {x : Ω | (↑c : ℝ≥0∞) ≤ ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ} :
      ℝ≥0∞)
h₁ :
  eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2 =
    (↑c : ℝ≥0∞)⁻¹ ^ ENNReal.toReal 2 * eLpNorm (X - fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ ^ ENNReal.toReal 2
⊢ (μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤
    eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2

Tactic:
convert!
      meas_ge_le_mul_pow_eLpNorm_enorm μ two_ne_zero ENNReal.ofNat_ne_top (hX.sub B) A (by simp)
    using 1

Premises used: ENNReal.ofNat_ne_top, MeasureTheory.AEStronglyMeasurable.sub, two_ne_zero, MeasureTheory.meas_ge_le_mul_pow_eLpNorm_enorm
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : (↑c : ℝ≥0∞) ≠ 0
B : AEStronglyMeasurable (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) μ
h h₁ h₂ h₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) {x : Ω | c ≤ ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖₊} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) {x : Ω | (↑c : ℝ≥0∞) ≤ ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ} :
      ℝ≥0∞)

Tactic:
norm_cast
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : (↑c : ℝ≥0∞) ≠ 0
B : AEStronglyMeasurable (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) μ
h :
  eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2 =
    (↑c : ℝ≥0∞)⁻¹ ^ ENNReal.toReal 2 *
      ((∫⁻ (x : Ω), ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^
          (1 / ENNReal.toReal 2)) ^
        ENNReal.toReal 2
⊢ eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2 =
    (↑c : ℝ≥0∞)⁻¹ ^ ENNReal.toReal 2 * eLpNorm (X - fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ ^ ENNReal.toReal 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 Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : (↑c : ℝ≥0∞) ≠ 0
B : AEStronglyMeasurable (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) μ
h :
  eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2 =
    HPow.hPow (β := ℝ) (↑c : ℝ≥0∞)⁻¹ 2 *
      HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2
⊢ eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2 =
    (↑c : ℝ≥0∞)⁻¹ ^ ENNReal.toReal 2 *
      ((∫⁻ (x : Ω), ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^
          (1 / ENNReal.toReal 2)) ^
        ENNReal.toReal 2

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

Premises used: one_div, ENNReal.toReal_ofNat, Pi.sub_apply
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : (↑c : ℝ≥0∞) ≠ 0
B : AEStronglyMeasurable (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) μ
h :
  HPow.hPow (β := ℕ) (↑c : ℝ≥0∞)⁻¹ 2 * eVar[X; μ] =
    HPow.hPow (β := ℕ) (↑c : ℝ≥0∞)⁻¹ 2 *
      HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2
⊢ eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2 =
    HPow.hPow (β := ℝ) (↑c : ℝ≥0∞)⁻¹ 2 *
      HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2

Tactic:
rw [div_eq_mul_inv, ENNReal.inv_pow, mul_comm, ENNReal.rpow_two]

Premises used: ENNReal.rpow_two, div_eq_mul_inv, mul_comm, ENNReal.inv_pow
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : (↑c : ℝ≥0∞) ≠ 0
B : AEStronglyMeasurable (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) μ
h :
  eVar[X; μ] =
    HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2
⊢ HPow.hPow (β := ℕ) (↑c : ℝ≥0∞)⁻¹ 2 * eVar[X; μ] =
    HPow.hPow (β := ℕ) (↑c : ℝ≥0∞)⁻¹ 2 *
      HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2

Tactic:
congr
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : (↑c : ℝ≥0∞) ≠ 0
B : AEStronglyMeasurable (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) μ
h : eVar[X; μ] = (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) ^ HMul.hMul (α := ℝ) 2⁻¹ 2
h₁ : eVar[X; μ] = HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 1
h₂ : eVar[X; μ] = HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℕ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 1
h₃ : eVar[X; μ] = ∫⁻ (x : Ω), HPow.hPow (β := ℕ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ
⊢ eVar[X; μ] =
    HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2

Tactic:
simp_rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_two,
    ENNReal.rpow_one, evariance]

Premises used: ENNReal.rpow_mul, ENNReal.rpow_one, ENNReal.rpow_two, two_ne_zero, inv_mul_cancel₀, ProbabilityTheory.evariance
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
rw :
  (μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤
    eVar[X; μ] / ENNReal.ofReal (HPow.hPow (β := ℕ) c 2)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ ENNReal.ofReal (Var[X; μ] / HPow.hPow (β := ℕ) c 2)

Tactic:
rw [ENNReal.ofReal_div_of_pos (sq_pos_of_ne_zero hc.ne.symm), hX.ofReal_variance_eq]

Premises used: ENNReal.ofReal_div_of_pos, Ne.symm, MeasureTheory.MemLp.ofReal_variance_eq, sq_pos_of_ne_zero, LT.lt.ne
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ c.toNNReal ≠ 0

Tactic:
simp [hc]
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
h :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c.toNNReal : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)
h₁ : eVar[X; μ] / ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) = eVar[X; μ] / HPow.hPow (β := ℕ) (↑c.toNNReal : ℝ≥0∞) 2
⊢ (μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤
    eVar[X; μ] / ENNReal.ofReal (HPow.hPow (β := ℕ) c 2)

Tactic:
convert! @meas_ge_le_evariance_div_sq _ _ _ _ hX.1 c.toNNReal (by simp [hc]) using 1

Premises used: And.left, ProbabilityTheory.meas_ge_le_evariance_div_sq
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c.toNNReal : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
h : eVar[X; μ] / HPow.hPow (β := ℕ) (ENNReal.ofReal c) 2 = eVar[X; μ] / HPow.hPow (β := ℕ) (↑c.toNNReal : ℝ≥0∞) 2
⊢ eVar[X; μ] / ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) = eVar[X; μ] / HPow.hPow (β := ℕ) (↑c.toNNReal : ℝ≥0∞) 2

Tactic:
rw [ENNReal.ofReal_pow hc.le]

Premises used: LT.lt.le, ENNReal.ofReal_pow
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ eVar[X; μ] / HPow.hPow (β := ℕ) (ENNReal.ofReal c) 2 = eVar[X; μ] / HPow.hPow (β := ℕ) (↑c.toNNReal : ℝ≥0∞) 2

Tactic:
rfl
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
pos : ∀ (h' : X =ᶠ[ae μ] 0), Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]
neg : ∀ (h' : ¬X =ᶠ[ae μ] 0), Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]

Tactic:
by_cases h' : X =ᵐ[μ] 0
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : X =ᶠ[ae μ] 0
pos : Var[0 + Y; μ] = Var[0; μ] + Var[Y; μ]
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]

Tactic:
rw [variance_congr h', variance_congr h'.add_right]

Premises used: ProbabilityTheory.variance_congr, Filter.EventuallyEq.add_right
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : X =ᶠ[ae μ] 0
⊢ Var[0 + Y; μ] = Var[0; μ] + Var[Y; μ]

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᶠ[ae μ] 0
⊢ Ne (α := ℝ≥0∞) 2 0

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᶠ[ae μ] 0
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᶠ[ae μ] 0
⊢ IsProbabilityMeasure μ

Tactic:
have := hX.isProbabilityMeasure_of_indepFun X Y (by simp) (by simp) h' h
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᶠ[ae μ] 0
this : IsProbabilityMeasure μ
neg : Var[X; μ] + HMul.hMul (α := ℝ) 2 0 + Var[Y; μ] = Var[X; μ] + Var[Y; μ]
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]

Tactic:
rw [variance_add hX hY, h.covariance_eq_zero hX hY]

Premises used: ProbabilityTheory.IndepFun.covariance_eq_zero, ProbabilityTheory.IndepFun.variance_add
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
h' : ¬X =ᶠ[ae μ] 0
this : IsProbabilityMeasure μ
⊢ Var[X; μ] + HMul.hMul (α := ℝ) 2 0 + Var[Y; μ] = Var[X; μ] + Var[Y; μ]

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
⊢ Var[fun (ω : Ω) ↦ X ω + Y ω; μ] = Var[X; μ] + Var[Y; μ]

Tactic:
h.variance_add hX hY

Premises used: ProbabilityTheory.IndepFun.variance_add
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
pos : ∀ (h'' : ∀ i ∈ s, X i =ᶠ[ae μ] 0), Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
neg : ∀ (h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0), Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]

Tactic:
by_cases h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᶠ[ae μ] 0
pos : Eq (α := ℝ) 0 (∑ i ∈ s, Var[X i; μ])
pos₁ : (ae μ).EventuallyEq (β := ℝ) (∑ i ∈ s, X i) 0
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]

Tactic:
rw [variance_congr (Y := 0), variance_zero]

Premises used: ProbabilityTheory.variance_zero, ProbabilityTheory.variance_congr
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᶠ[ae μ] 0
pos : Eq (α := ℝ) (∑ i ∈ s, Var[X i; μ]) 0
⊢ Eq (α := ℝ) 0 (∑ i ∈ s, Var[X i; μ])

Tactic:
symm
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᶠ[ae μ] 0
⊢ Eq (α := ℝ) (∑ i ∈ s, Var[X i; μ]) 0

Tactic:
Finset.sum_eq_zero fun i hi ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᶠ[ae μ] 0
pos : ∀ (i : ι) (hi : i ∈ s), Var[X i; μ] = 0
⊢ Eq (α := ℝ) (∑ i ∈ s, Var[X i; μ]) 0

Tactic:
refine Finset.sum_eq_zero fun i hi ↦ ?_

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᶠ[ae μ] 0
i : ι
hi : i ∈ s
⊢ Var[X i; μ] = 0

Tactic:
simp [variance_congr (h'' i hi)]

Premises used: ProbabilityTheory.variance_congr
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᶠ[ae μ] 0
⊢ ∀ (i : ↥s), X (↑i : ι) =ᶠ[ae μ] 0

Tactic:
have := fun (i : s) ↦ h'' i.1 i.2
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᶠ[ae μ] 0
this : ∀ (i : ↥s), X (↑i : ι) =ᶠ[ae μ] 0
h₁ : ∀ (ω : Ω) (hω : ∀ (i : ↥s), X (↑i : ι) ω = 0 ω), Eq (α := ℝ) ((∑ i ∈ s, X i) ω) (0 ω)
⊢ (ae μ).EventuallyEq (β := ℝ) (∑ i ∈ s, X i) 0

Tactic:
filter_upwards [ae_all_iff.2 this] with ω hω

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᶠ[ae μ] 0
this : ∀ (i : ↥s), X (↑i : ι) =ᶠ[ae μ] 0
ω : Ω
hω : ∀ (i : ↥s), X (↑i : ι) ω = 0 ω
h₁ : Eq (α := ℝ) (∑ c ∈ s, X c ω) 0
⊢ Eq (α := ℝ) ((∑ i ∈ s, X i) ω) (0 ω)

Tactic:
simp only [sum_apply, Pi.zero_apply]

Premises used: Finset.sum_apply, Pi.zero_apply
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᶠ[ae μ] 0
this : ∀ (i : ↥s), X (↑i : ι) =ᶠ[ae μ] 0
ω : Ω
hω : ∀ (i : ↥s), X (↑i : ι) ω = 0 ω
⊢ Eq (α := ℝ) (∑ c ∈ s, X c ω) 0

Tactic:
Finset.sum_eq_zero fun i hi ↦ hω ⟨i, hi⟩

Premises used: Finset.sum_eq_zero, Subtype.mk
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ∀ i ∈ s, X i =ᶠ[ae μ] 0
this : ∀ (i : ↥s), X (↑i : ι) =ᶠ[ae μ] 0
ω : Ω
hω : ∀ (i : ↥s), X (↑i : ι) ω = 0 ω
⊢ Eq (α := ℝ) (∑ c ∈ s, X c ω) 0

Tactic:
exact Finset.sum_eq_zero fun i hi ↦ hω ⟨i, hi⟩

Premises used: Finset.sum_eq_zero
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
neg : ∀ (j : ι) (hj1 : j ∈ s) (hj2 : ¬X j =ᶠ[ae μ] 0), Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]

Tactic:
obtain ⟨j, hj1, hj2⟩ := not_forall₂.1 h''

Premises used: Iff.mp, not_forall₂
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᶠ[ae μ] 0
neg :
  ∀ (hs : ∀ (i : ι), Membership.mem (γ := Finset ι) {j} i → MemLp (X i) 2 μ)
    (h : (↑{j} : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j)
    (h'' : ¬∀ (i : ι), Membership.mem (γ := Finset ι) {j} i → X i =ᶠ[ae μ] 0)
    (hj1 : Membership.mem (γ := Finset ι) {j} j), Var[∑ i ∈ {j}, X i; μ] = ∑ i ∈ {j}, Var[X i; μ]
neg₁ : ∀ (h' : s.Nontrivial), Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]

Tactic:
obtain rfl | h' := s.eq_singleton_or_nontrivial hj1

Premises used: Finset.eq_singleton_or_nontrivial, rfl
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
j : ι
hj2 : ¬X j =ᶠ[ae μ] 0
hs : ∀ (i : ι), Membership.mem (γ := Finset ι) {j} i → MemLp (X i) 2 μ
h : (↑{j} : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ (i : ι), Membership.mem (γ := Finset ι) {j} i → X i =ᶠ[ae μ] 0
hj1 : Membership.mem (γ := Finset ι) {j} j
⊢ Var[∑ i ∈ {j}, X i; μ] = ∑ i ∈ {j}, Var[X i; μ]

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᶠ[ae μ] 0
h' : s.Nontrivial
neg : ∀ (k : ι) (hk1 : k ∈ s) (hk2 : k ≠ j), Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]

Tactic:
obtain ⟨k, hk1, hk2⟩ := h'.exists_ne j

Premises used: Finset.Nontrivial.exists_ne
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᶠ[ae μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
⊢ Ne (α := ℝ≥0∞) 2 0

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᶠ[ae μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᶠ[ae μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
⊢ IsProbabilityMeasure μ

Tactic:
have := (hs j hj1).isProbabilityMeasure_of_indepFun (X j) (X k) (by simp) (by simp) hj2
    (h hj1 hk1 hk2.symm)
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᶠ[ae μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
this : IsProbabilityMeasure μ
neg : Eq (α := ℝ) (∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]) (∑ i ∈ s, Var[X i; μ])
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]

Tactic:
rw [variance_sum' hs]

Premises used: ProbabilityTheory.variance_sum'
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_3
X : ι → Ω → ℝ
s : Finset ι
hs : ∀ i ∈ s, MemLp (X i) 2 μ
h : (↑s : Set ι).Pairwise fun (i j : ι) ↦ X i ⟂ᵢ[μ] X j
h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0
j : ι
hj1 : j ∈ s
hj2 : ¬X j =ᶠ[ae μ] 0
h' : s.Nontrivial
k : ι
hk1 : k ∈ s
hk2 : k ≠ j
this : IsProbabilityMeasure μ
⊢ Eq (α := ℝ) (∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]) (∑ i ∈ s, Var[X i; μ])

Tactic:
Finset.sum_congr rfl (fun i hi ↦ ?_)

Premises used: Finset.sum_congr, rfl