awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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
⊢ HPow.hPow (β := ℕ) ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ 2 =
    ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ 2
have 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
Tactic: rw [integral_const_mul, ← mul_sub, enorm_mul, mul_pow, ← enorm_pow,
    Real.enorm_of_nonneg (sq_nonneg _)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
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
⊢ HPow.hPow (β := ℕ) ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ 2 =
    ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ 2
have 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
Tactic: rw [integral_const_mul, ← mul_sub, enorm_mul, mul_pow, ← enorm_pow,
    Real.enorm_of_nonneg (sq_nonneg _)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEMeasurable X μ
⊢ cov[X, X; μ] = Var[X; μ]
have rw : Eq (α := ℝ) (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (X ω - ∫ (x : Ω), X x ∂μ) ∂μ)
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ)
Tactic: rw [covariance, variance_eq_integral hX]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEMeasurable X μ
⊢ Eq (α := ℝ) (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ) * (X ω - ∫ (x : Ω), X x ∂μ) ∂μ)
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ)
have e_f : ∀ (x : Ω), (X x - ∫ (x : Ω), X x ∂μ) * (X x - ∫ (x : Ω), X x ∂μ) = HPow.hPow (β := ℕ) (X x - ∫ (x : Ω), X x ∂μ) 2
Tactic: congr with x
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ Var[fun (ω : Ω) ↦ c * X ω; μ] = HPow.hPow (β := ℕ) c 2 * Var[X; μ]
have rw : HPow.hPow (β := ℕ) c 2 * eVar[X; μ].toReal = HPow.hPow (β := ℕ) c 2 * Var[X; μ]
Tactic: rw [variance, evariance_mul, ENNReal.toReal_mul, ENNReal.toReal_ofReal (sq_nonneg _)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst : CommSemiring A
inst_1 : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ Var[c • X; μ] = HPow.hPow (β := ℕ) c 2 • Var[X; μ]
have h : Var[c • X; μ] = Var[HSMul.hSMul (α := ℝ) ((algebraMap A ℝ : (a : A) → ℝ) c : ℝ) X; μ]
Tactic: convert! variance_smul (algebraMap A ℝ c) X μ using 1
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst : CommSemiring A
inst_1 : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
h : Var[c • X; μ] = Var[HSMul.hSMul (α := ℝ) ((algebraMap A ℝ : (a : A) → ℝ) c : ℝ) X; μ]
⊢ Var[c • X; μ] = HPow.hPow (β := ℕ) c 2 • Var[X; μ]
have h₁ : HPow.hPow (β := ℕ) c 2 • Var[X; μ] = HPow.hPow (α := ℝ) (β := ℕ) ((algebraMap A ℝ : (a : A) → ℝ) c : ℝ) 2 * Var[X; μ]
Tactic: convert! variance_smul (algebraMap A ℝ c) X μ using 1
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
⊢ Var[X; μ] = ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
have rw : cov[X, X; μ] = ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
Tactic: rw [← covariance_self hX.aemeasurable, covariance_eq_sub hX hX, pow_two, pow_two]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
rw : cov[X, X; μ] = ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
⊢ Var[X; μ] = ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
have rw₁ : ∫ (x : Ω), (X * X) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), X x ∂μ) =
  ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
Tactic: rw [← covariance_self hX.aemeasurable, covariance_eq_sub hX hX, pow_two, pow_two]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
rw : cov[X, X; μ] = ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
rw₁ :
  ∫ (x : Ω), (X * X) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), X x ∂μ) =
    ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
⊢ Var[X; μ] = ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
have rw₂ : ∫ (x : Ω), (X * X) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), X x ∂μ) =
  ∫ (x : Ω), (X * X) x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
Tactic: rw [← covariance_self hX.aemeasurable, covariance_eq_sub hX hX, pow_two, pow_two]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : MemLp X 2 μ
rw : cov[X, X; μ] = ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
rw₁ :
  ∫ (x : Ω), (X * X) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), X x ∂μ) =
    ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
rw₂ :
  ∫ (x : Ω), (X * X) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), X x ∂μ) =
    ∫ (x : Ω), (X * X) x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
⊢ Var[X; μ] = ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2
have rw₃ : ∫ (x : Ω), (X * X) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), X x ∂μ) =
  ∫ (x : Ω), (X * X) x ∂μ - HMul.hMul (α := ℝ) (∫ (x : Ω), X x ∂μ) (∫ (x : Ω), X x ∂μ)
Tactic: rw [← covariance_self hX.aemeasurable, covariance_eq_sub hX hX, pow_two, pow_two]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
⊢ Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]
have pos : ∀ (hX_Lp : MemLp X 2 μ), Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]
Tactic: by_cases hX_Lp : MemLp X 2 μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
pos : ∀ (hX_Lp : MemLp X 2 μ), Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]
⊢ Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]
have neg : ∀ (hX_Lp : ¬MemLp X 2 μ), Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]
Tactic: by_cases hX_Lp : MemLp X 2 μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : MemLp X 2 μ
⊢ Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]
have hX_int : Integrable X μ
Tactic: have hX_int : Integrable X μ := hX_Lp.integrable one_le_two
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : MemLp X 2 μ
hX_int : Integrable X μ
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ c) μ
have funProp : ‖c‖ₑ ≠ ∞
Tactic: fun_prop
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : MemLp X 2 μ
hX_int : Integrable X μ
⊢ Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]
have pos : Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω + c - (∫ (a : Ω), X a ∂μ + μ.real Set.univ • c)) 2 ∂μ)
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ)
Tactic: rw [variance_eq_integral (hX.add_const _).aemeasurable,
      integral_add hX_int (by fun_prop), integral_const, variance_eq_integral hX.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : ¬MemLp X 2 μ
⊢ Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]
have neg : ¬MemLp (ε := ℝ) (fun (x : Ω) ↦ X x + c) 2 μ
Tactic: rw [variance_of_not_memLp (hX.add_const _), variance_of_not_memLp hX hX_Lp]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : ¬MemLp X 2 μ
⊢ ¬MemLp (ε := ℝ) (fun (x : Ω) ↦ X x + c) 2 μ
have neg : ∀ (h_memLp : MemLp (ε := ℝ) (fun (x : Ω) ↦ X x + c) 2 μ), MemLp X 2 μ
Tactic: refine fun h_memLp ↦ hX_Lp ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : ¬MemLp X 2 μ
h_memLp : MemLp (ε := ℝ) (fun (x : Ω) ↦ X x + c) 2 μ
⊢ X = fun (ω : Ω) ↦ X ω + c - c
have h : ∀ (x : Ω), X x = X x + c - c
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : ¬MemLp X 2 μ
h_memLp : MemLp (ε := ℝ) (fun (x : Ω) ↦ X x + c) 2 μ
⊢ MemLp X 2 μ
have this : X = fun (ω : Ω) ↦ X ω + c - c
Tactic: have : X = fun ω ↦ X ω + c - c := by ext; ring
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : ¬MemLp X 2 μ
h_memLp : MemLp (ε := ℝ) (fun (x : Ω) ↦ X x + c) 2 μ
this : X = fun (ω : Ω) ↦ X ω + c - c
⊢ MemLp X 2 μ
have neg : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω + c - c) 2 μ
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
⊢ Var[fun (ω : Ω) ↦ c + X ω; μ] = Var[X; μ]
have simp_rw : Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]
Tactic: simp_rw [add_comm c, variance_add_const hX c]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ Var[fun (ω : Ω) ↦ -X ω; μ] = Var[X; μ]
have h : ∀ (x : Ω), Neg.neg = HMul.hMul (α := ℝ) (-1)
Tactic: convert! variance_const_mul (-1) X μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (x : Ω), Neg.neg = HMul.hMul (α := ℝ) (-1)
⊢ Var[fun (ω : Ω) ↦ -X ω; μ] = Var[X; μ]
have h₁ : Var[X; μ] = HPow.hPow (α := ℝ) (β := ℕ) (-1) 2 * Var[X; μ]
Tactic: convert! variance_const_mul (-1) X μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : Ω
⊢ Neg.neg = HMul.hMul (α := ℝ) (-1)
have h : ∀ (x : ℝ), -x = -1 * x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
⊢ Var[fun (ω : Ω) ↦ c + -X ω; μ] = Var[X; μ]
have rw : Var[fun (ω : Ω) ↦ -X ω; μ] = Var[X; μ]
Tactic: rw [variance_const_add (by fun_prop) c, variance_fun_neg]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
rw : Var[fun (ω : Ω) ↦ -X ω; μ] = Var[X; μ]
⊢ Var[fun (ω : Ω) ↦ c + -X ω; μ] = Var[X; μ]
have rw₁ : Var[X; μ] = Var[X; μ]
Tactic: rw [variance_const_add (by fun_prop) c, variance_fun_neg]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[X + Y; μ] = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ]
have rw : Var[X; μ] + cov[Y, X; μ] + (cov[Y, X; μ] + Var[Y; μ]) = Var[X; μ] + 2 * cov[Y, X; μ] + Var[Y; μ]
Tactic: rw [← covariance_self, covariance_add_left hX hY (hX.add hY), covariance_add_right hX hX hY,
    covariance_add_right hY hX hY, covariance_self, covariance_self, covariance_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw : Var[X; μ] + cov[Y, X; μ] + (cov[Y, X; μ] + Var[Y; μ]) = Var[X; μ] + 2 * cov[Y, X; μ] + Var[Y; μ]
⊢ Var[X + Y; μ] = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ]
have rw₁ : AEMeasurable Y μ
Tactic: rw [← covariance_self, covariance_add_left hX hY (hX.add hY), covariance_add_right hX hX hY,
    covariance_add_right hY hX hY, covariance_self, covariance_self, covariance_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw : Var[X; μ] + cov[Y, X; μ] + (cov[Y, X; μ] + Var[Y; μ]) = Var[X; μ] + 2 * cov[Y, X; μ] + Var[Y; μ]
rw₁ : AEMeasurable Y μ
⊢ Var[X + Y; μ] = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ]
have rw₂ : AEMeasurable X μ
Tactic: rw [← covariance_self, covariance_add_left hX hY (hX.add hY), covariance_add_right hX hX hY,
    covariance_add_right hY hX hY, covariance_self, covariance_self, covariance_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw : Var[X; μ] + cov[Y, X; μ] + (cov[Y, X; μ] + Var[Y; μ]) = Var[X; μ] + 2 * cov[Y, X; μ] + Var[Y; μ]
rw₁ : AEMeasurable Y μ
rw₂ : AEMeasurable X μ
⊢ Var[X + Y; μ] = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ]
have rw₃ : AEMeasurable (X + Y) μ
Tactic: rw [← covariance_self, covariance_add_left hX hY (hX.add hY), covariance_add_right hX hX hY,
    covariance_add_right hY hX hY, covariance_self, covariance_self, covariance_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[X - Y; μ] = Var[X; μ] - 2 * cov[X, Y; μ] + Var[Y; μ]
have rw : Var[X; μ] + 2 * -cov[X, Y; μ] + Var[Y; μ] = Var[X; μ] - 2 * cov[X, Y; μ] + Var[Y; μ]
Tactic: rw [sub_eq_add_neg, variance_add hX hY.neg, variance_neg, covariance_neg_right]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]
have rw : Eq (α := ℝ) (∑ i ∈ s, cov[X i, ∑ i ∈ s, X i; μ]) (∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ])
Tactic: rw [← covariance_self, covariance_sum_left' (by simpa)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
rw : Eq (α := ℝ) (∑ i ∈ s, cov[X i, ∑ i ∈ s, X i; μ]) (∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ])
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]
have rw₁ : MemLp (ε := ℝ) (∑ i ∈ s, X i) 2 μ
Tactic: rw [← covariance_self, covariance_sum_left' (by simpa)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
rw : Eq (α := ℝ) (∑ i ∈ s, cov[X i, ∑ i ∈ s, X i; μ]) (∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ])
rw₁ : MemLp (ε := ℝ) (∑ i ∈ s, X i) 2 μ
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]
have rw₂ : AEMeasurable (β := ℝ) (∑ i ∈ s, X i) μ
Tactic: rw [← covariance_self, covariance_sum_left' (by simpa)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ Eq (α := ℝ) (∑ i ∈ s, cov[X i, ∑ i ∈ s, X i; μ]) (∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ])
have refine : ∀ (i : ι) (hi : i ∈ s), cov[X i, ∑ i ∈ s, X i; μ] = ∑ j ∈ s, cov[X i, X j; μ]
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_2
s : Finset ι
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
i : ι
hi : i ∈ s
⊢ cov[X i, ∑ i ∈ s, X i; μ] = ∑ j ∈ s, cov[X i, X j; μ]
have rw : Eq (α := ℝ) (∑ i_1 ∈ s, cov[X i, X i_1; μ]) (∑ j ∈ s, cov[X i, X j; μ])
Tactic: rw [covariance_sum_right' (by simpa) (hX i hi)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ Var[fun (ω : Ω) ↦ ∑ i ∈ s, X i ω; μ] = ∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]
have h : ∀ (x : Ω), Eq (α := ℝ) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)
Tactic: convert! variance_sum' hX
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
⊢ Var[fun (ω : Ω) ↦ ∑ i : ι, X i ω; μ] = ∑ i : ι, ∑ j : ι, cov[X i, X j; μ]
have h : ∀ (x : Ω), Eq (α := ℝ) (∑ i : ι, X i x) ((∑ i : ι, X i) x)
Tactic: convert! variance_sum hX
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst : MeasurableSingletonClass Ω
x : Ω
⊢ variance (mΩ := mΩ) X (Measure.dirac x) = 0
have rw : Eq (α := ℝ)
  (@integral _ _ _ _ mΩ (Measure.dirac x) fun (ω : Ω) ↦
    HPow.hPow (β := ℕ) (X ω - @integral _ _ _ _ mΩ (Measure.dirac x) fun (x : Ω) ↦ X x) 2)
  0
Tactic: rw [variance_eq_integral]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst : MeasurableSingletonClass Ω
x : Ω
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ mΩ (Measure.dirac x) fun (ω : Ω) ↦
      HPow.hPow (β := ℕ) (X ω - @integral _ _ _ _ mΩ (Measure.dirac x) fun (x : Ω) ↦ X x) 2)
    0
⊢ variance (mΩ := mΩ) X (Measure.dirac x) = 0
have rw₁ : AEMeasurable (_m := mΩ) X (Measure.dirac x)
Tactic: rw [variance_eq_integral]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
hX : AEMeasurable (_m := mΩ) X (Measure.map Y μ)
hY : AEMeasurable Y μ
⊢ variance (mΩ := mΩ) X (Measure.map Y μ) = Var[X ∘ Y; μ]
have rw : Eq (α := ℝ) (∫ (x : Ω'), HPow.hPow (β := ℕ) (X (Y x) - ∫ (x : Ω'), X (Y x) ∂μ) 2 ∂μ)
  (∫ (ω : Ω'), HPow.hPow (β := ℕ) ((X ∘ Y) ω - ∫ (x : Ω'), (X ∘ Y) x ∂μ) 2 ∂μ)
Tactic: rw [variance_eq_integral hX, integral_map hY, variance_eq_integral (hX.comp_aemeasurable hY),
    integral_map hY]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
hX : AEMeasurable (_m := mΩ) X (Measure.map Y μ)
hY : AEMeasurable Y μ
rw :
  Eq (α := ℝ) (∫ (x : Ω'), HPow.hPow (β := ℕ) (X (Y x) - ∫ (x : Ω'), X (Y x) ∂μ) 2 ∂μ)
    (∫ (ω : Ω'), HPow.hPow (β := ℕ) ((X ∘ Y) ω - ∫ (x : Ω'), (X ∘ Y) x ∂μ) 2 ∂μ)
⊢ variance (mΩ := mΩ) X (Measure.map Y μ) = Var[X ∘ Y; μ]
have rw₁ : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Y μ)
Tactic: rw [variance_eq_integral hX, integral_map hY, variance_eq_integral (hX.comp_aemeasurable hY),
    integral_map hY]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
hX : AEMeasurable (_m := mΩ) X (Measure.map Y μ)
hY : AEMeasurable Y μ
rw :
  Eq (α := ℝ) (∫ (x : Ω'), HPow.hPow (β := ℕ) (X (Y x) - ∫ (x : Ω'), X (Y x) ∂μ) 2 ∂μ)
    (∫ (ω : Ω'), HPow.hPow (β := ℕ) ((X ∘ Y) ω - ∫ (x : Ω'), (X ∘ Y) x ∂μ) 2 ∂μ)
rw₁ : AEStronglyMeasurable (m₀ := mΩ) X (Measure.map Y μ)
⊢ variance (mΩ := mΩ) X (Measure.map Y μ) = Var[X ∘ Y; μ]
have rw₂ : AEStronglyMeasurable (β := ℝ) (m₀ := mΩ)
  (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - @integral _ _ _ _ mΩ (Measure.map Y μ) fun (x : Ω) ↦ X x) 2)
  (Measure.map Y μ)
Tactic: rw [variance_eq_integral hX, integral_map hY, variance_eq_integral (hX.comp_aemeasurable hY),
    integral_map hY]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
hX : AEMeasurable (_m := mΩ) X (Measure.map Y μ)
hY : AEMeasurable Y μ
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mΩ)
    (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - @integral _ _ _ _ mΩ (Measure.map Y μ) fun (x : Ω) ↦ X x) 2)
    (Measure.map Y μ)
have refine : AEStronglyMeasurable (β := ℝ) (m₀ := mΩ) (fun (ω : Ω) ↦ X ω - @integral _ _ _ _ mΩ (Measure.map Y μ) fun (x : Ω) ↦ X x)
  (Measure.map Y μ)
Tactic: refine AEStronglyMeasurable.pow ?_ _
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
X : Ω → Ω'
hX : MeasurePreserving X μ ν
f : Ω' → ℝ
hf : AEMeasurable f ν
⊢ Var[fun (ω : Ω) ↦ f (X ω); μ] = Var[f; ν]
have rw : Var[fun (ω : Ω) ↦ f (X ω); μ] = variance (mΩ := mΩ') f (Measure.map X μ)
Tactic: rw [← hX.map_eq, variance_map (hX.map_eq ▸ hf) hX.aemeasurable, Function.comp_def]