awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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 ∂μ) μ
⊢ eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2 =
    (↑c : ℝ≥0∞)⁻¹ ^ ENNReal.toReal 2 * eLpNorm (X - fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ ^ ENNReal.toReal 2
have 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
Tactic: rw [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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 ∂μ) μ
⊢ 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
have 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
Tactic: simp only [ENNReal.toReal_ofNat, one_div, Pi.sub_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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 ∂μ) μ
⊢ 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
have 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
Tactic: rw [div_eq_mul_inv, ENNReal.inv_pow, mul_comm, ENNReal.rpow_two]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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 ∂μ) μ
⊢ 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
have h : eVar[X; μ] =
  HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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 ∂μ) μ
⊢ eVar[X; μ] =
    HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2
have h : eVar[X; μ] = (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) ^ HMul.hMul (α := ℝ) 2⁻¹ 2
Tactic: simp_rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_two,
    ENNReal.rpow_one, evariance]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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
⊢ eVar[X; μ] =
    HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2
have h₁ : eVar[X; μ] = HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 1
Tactic: simp_rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_two,
    ENNReal.rpow_one, evariance]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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
⊢ eVar[X; μ] =
    HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2
have h₂ : eVar[X; μ] = HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℕ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 1
Tactic: simp_rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_two,
    ENNReal.rpow_one, evariance]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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
⊢ eVar[X; μ] =
    HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2
have h₃ : eVar[X; μ] = ∫⁻ (x : Ω), HPow.hPow (β := ℕ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ
Tactic: simp_rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_two,
    ENNReal.rpow_one, evariance]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ (μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ ENNReal.ofReal (Var[X; μ] / HPow.hPow (β := ℕ) c 2)
have rw : (μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤ eVar[X; μ] / ENNReal.ofReal (HPow.hPow (β := ℕ) c 2)
Tactic: rw [ENNReal.ofReal_div_of_pos (sq_pos_of_ne_zero hc.ne.symm), hX.ofReal_variance_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ (μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤
    eVar[X; μ] / ENNReal.ofReal (HPow.hPow (β := ℕ) c 2)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)
  ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c.toNNReal : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)
Tactic: convert! @meas_ge_le_evariance_div_sq _ _ _ _ hX.1 c.toNNReal (by simp [hc]) using 1
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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∞)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | c ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤
    eVar[X; μ] / ENNReal.ofReal (HPow.hPow (β := ℕ) c 2)
have h₁ : eVar[X; μ] / ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) = eVar[X; μ] / HPow.hPow (β := ℕ) (↑c.toNNReal : ℝ≥0∞) 2
Tactic: convert! @meas_ge_le_evariance_div_sq _ _ _ _ hX.1 c.toNNReal (by simp [hc]) using 1
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
c : ℝ
hc : 0 < c
⊢ eVar[X; μ] / ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) = eVar[X; μ] / HPow.hPow (β := ℕ) (↑c.toNNReal : ℝ≥0∞) 2
have h : eVar[X; μ] / HPow.hPow (β := ℕ) (ENNReal.ofReal c) 2 = eVar[X; μ] / HPow.hPow (β := ℕ) (↑c.toNNReal : ℝ≥0∞) 2
Tactic: rw [ENNReal.ofReal_pow hc.le]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
h : X ⟂ᵢ[μ] Y
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]
have pos : ∀ (h' : X =ᶠ[ae μ] 0), Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]
Tactic: by_cases h' : X =ᵐ[μ] 0
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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; μ]
⊢ Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]
have neg : ∀ (h' : ¬X =ᶠ[ae μ] 0), Var[X + Y; μ] = Var[X; μ] + Var[Y; μ]
Tactic: by_cases h' : X =ᵐ[μ] 0
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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[X + Y; μ] = Var[X; μ] + Var[Y; μ]
have pos : Var[0 + Y; μ] = Var[0; μ] + Var[Y; μ]
Tactic: rw [variance_congr h', variance_congr h'.add_right]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
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[X + Y; μ] = Var[X; μ] + Var[Y; μ]
have this : IsProbabilityMeasure μ
Tactic: have := hX.isProbabilityMeasure_of_indepFun X Y (by simp) (by simp) h' h
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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 + Y; μ] = Var[X; μ] + Var[Y; μ]
have neg : Var[X; μ] + HMul.hMul (α := ℝ) 2 0 + Var[Y; μ] = Var[X; μ] + Var[Y; μ]
Tactic: rw [variance_add hX hY, h.covariance_eq_zero hX hY]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
have pos : ∀ (h'' : ∀ i ∈ s, X i =ᶠ[ae μ] 0), Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
Tactic: by_cases h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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; μ]
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
have neg : ∀ (h'' : ¬∀ i ∈ s, X i =ᶠ[ae μ] 0), Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
Tactic: by_cases h'' : ∀ i ∈ s, X i =ᵐ[μ] 0
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
have pos : Eq (α := ℝ) 0 (∑ i ∈ s, Var[X i; μ])
Tactic: rw [variance_congr (Y := 0), variance_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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; μ])
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
have pos₁ : (ae μ).EventuallyEq (β := ℝ) (∑ i ∈ s, X i) 0
Tactic: rw [variance_congr (Y := 0), variance_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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 (α := ℝ) 0 (∑ i ∈ s, Var[X i; μ])
have pos : Eq (α := ℝ) (∑ i ∈ s, Var[X i; μ]) 0
Tactic: symm
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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
have pos : ∀ (i : ι) (hi : i ∈ s), Var[X i; μ] = 0
Tactic: refine Finset.sum_eq_zero fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
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
⊢ (ae μ).EventuallyEq (β := ℝ) (∑ i ∈ s, X i) 0
have this : ∀ (i : ↥s), X (↑i : ι) =ᶠ[ae μ] 0
Tactic: have := fun (i : s) ↦ h'' i.1 i.2
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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
⊢ (ae μ).EventuallyEq (β := ℝ) (∑ i ∈ s, X i) 0
have h₁ : ∀ (ω : Ω) (hω : ∀ (i : ↥s), X (↑i : ι) ω = 0 ω), Eq (α := ℝ) ((∑ i ∈ s, X i) ω) (0 ω)
Tactic: filter_upwards [ae_all_iff.2 this] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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 (α := ℝ) ((∑ i ∈ s, X i) ω) (0 ω)
have h₁ : Eq (α := ℝ) (∑ c ∈ s, X c ω) 0
Tactic: simp only [sum_apply, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
have neg : ∀ (j : ι) (hj1 : j ∈ s) (hj2 : ¬X j =ᶠ[ae μ] 0), Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
Tactic: obtain ⟨j, hj1, hj2⟩ := not_forall₂.1 h''
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
have 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; μ]
Tactic: obtain rfl | h' := s.eq_singleton_or_nontrivial hj1
Cleared hypotheses: s, hs, h, h'', hj1
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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; μ]
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
have neg₁ : ∀ (h' : s.Nontrivial), Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
Tactic: obtain rfl | h' := s.eq_singleton_or_nontrivial hj1
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
have neg : ∀ (k : ι) (hk1 : k ∈ s) (hk2 : k ≠ j), Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
Tactic: obtain ⟨k, hk1, hk2⟩ := h'.exists_ne j
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
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
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
have this : IsProbabilityMeasure μ
Tactic: have := (hs j hj1).isProbabilityMeasure_of_indepFun (X j) (X k) (by simp) (by simp) hj2
    (h hj1 hk1 hk2.symm)
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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 μ
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, Var[X i; μ]
have neg : Eq (α := ℝ) (∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]) (∑ i ∈ s, Var[X i; μ])
Tactic: rw [variance_sum' hs]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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; μ])
have neg : ∀ (i : ι) (hi : i ∈ s), ∑ j ∈ s, cov[X i, X j; μ] = Var[X i; μ]
Tactic: refine Finset.sum_congr rfl (fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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 μ
i : ι
hi : i ∈ s
⊢ ∑ j ∈ s, cov[X i, X j; μ] = Var[X i; μ]
have neg : ∑ j ∈ s, cov[X i, X j; μ] = cov[X i, X i; μ]
Tactic: rw [← covariance_self (hs i hi).aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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 μ
i : ι
hi : i ∈ s
⊢ ∑ j ∈ s, cov[X i, X j; μ] = cov[X i, X i; μ]
have neg : ∀ (j : ι) (hj1 : j ∈ s) (hj2 : j ≠ i), cov[X i, X j; μ] = 0
Tactic: refine Finset.sum_eq_single_of_mem i hi fun j hj1 hj2 ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ Var[∑ i : ι, fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ] = ∑ i : ι, Var[X i; μ i]
have rw : Eq (α := ℝ) (∑ i : ι, Var[fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ]) (∑ i : ι, Var[X i; μ i])
Tactic: rw [IndepFun.variance_sum]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
rw : Eq (α := ℝ) (∑ i : ι, Var[fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ]) (∑ i : ι, Var[X i; μ i])
⊢ Var[∑ i : ι, fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ] = ∑ i : ι, Var[X i; μ i]
have hs : ∀ (i : ι),
  Membership.mem (γ := Finset ι) univ i → MemLp (ε := ℝ) (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) 2 (Measure.pi (α := Ω) μ)
Tactic: rw [IndepFun.variance_sum]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
rw : Eq (α := ℝ) (∑ i : ι, Var[fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ]) (∑ i : ι, Var[X i; μ i])
hs :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) univ i →
      MemLp (ε := ℝ) (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) 2 (Measure.pi (α := Ω) μ)
⊢ Var[∑ i : ι, fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ] = ∑ i : ι, Var[X i; μ i]
have h₁ : (↑univ : Set ι).Pairwise fun (i j : ι) ↦
  (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) ⟂ᵢ[Measure.pi (α := Ω) μ] fun (ω : (i : ι) → Ω i) ↦ X j (ω j)
Tactic: rw [IndepFun.variance_sum]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
⊢ Eq (α := ℝ) (∑ i : ι, Var[fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ]) (∑ i : ι, Var[X i; μ i])
have e_f : ∀ (i : ι), Var[fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ] = Var[X i; μ i]
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ Var[fun (ω : (i : ι) → Ω i) ↦ X i (ω i); Measure.pi (α := Ω) μ] = Var[X i; μ i]
have e_f : Var[X i ∘ fun (ω : (i : ι) → Ω i) ↦ ω i; Measure.pi (α := Ω) μ] = Var[X i; μ i]
Tactic: change Var[(X i) ∘ (fun ω ↦ ω i); Measure.pi μ] = _
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
⊢ Var[X i ∘ fun (ω : (i : ι) → Ω i) ↦ ω i; Measure.pi (α := Ω) μ] = Var[X i; μ i]
have e_f : AEMeasurable (_m := mΩ i) (X i) (Measure.map (fun (ω : (i : ι) → Ω i) ↦ ω i) (Measure.pi (α := Ω) μ))
Tactic: rw [← variance_map, (measurePreserving_eval _ i).map_eq]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
ι : Type u_2
inst : Fintype ι
Ω : ι → Type u_3
mΩ : (i : ι) → MeasurableSpace (Ω i)
μ : (i : ι) → Measure (Ω i)
inst_1 : ∀ (i : ι), IsProbabilityMeasure (μ i)
X : (i : ι) → Ω i → ℝ
h : ∀ (i : ι), MemLp (X i) 2 (μ i)
i : ι
e_f : AEMeasurable (_m := mΩ i) (X i) (Measure.map (fun (ω : (i : ι) → Ω i) ↦ ω i) (Measure.pi (α := Ω) μ))
⊢ Var[X i ∘ fun (ω : (i : ι) → Ω i) ↦ ω i; Measure.pi (α := Ω) μ] = Var[X i; μ i]
have e_f₁ : AEMeasurable (β := Ω i) (fun (ω : (i : ι) → Ω i) ↦ ω i) (Measure.pi (α := Ω) μ)
Tactic: rw [← variance_map, (measurePreserving_eval _ i).map_eq]