awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
rw : HPow.hPow (β := ℕ) c 2 * eVar[X; μ].toReal = HPow.hPow (β := ℕ) c 2 * Var[X; μ]
⊢ Var[fun (ω : Ω) ↦ c * X ω; μ] = HPow.hPow (β := ℕ) c 2 * Var[X; μ]

Tactic:
rw [variance, evariance_mul, ENNReal.toReal_mul, ENNReal.toReal_ofReal (sq_nonneg _)]

Premises used: ProbabilityTheory.variance, ENNReal.toReal_ofReal, ENNReal.toReal_mul, sq_nonneg, ProbabilityTheory.evariance_mul
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ HPow.hPow (β := ℕ) c 2 * eVar[X; μ].toReal = HPow.hPow (β := ℕ) c 2 * Var[X; μ]

Tactic:
rfl
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ Var[fun (ω : Ω) ↦ X ω * c; μ] = Var[X; μ] * HPow.hPow (β := ℕ) c 2

Tactic:
simp [mul_comm, variance_const_mul]

Premises used: mul_comm, ProbabilityTheory.variance_const_mul
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ Var[c • X; μ] = HPow.hPow (β := ℕ) c 2 * Var[X; μ]

Tactic:
variance_const_mul c X μ

Premises used: ProbabilityTheory.variance_const_mul
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst : CommSemiring A
inst_1 : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ Var[HSMul.hSMul (α := ℝ) ((algebraMap A ℝ : (a : A) → ℝ) c : ℝ) X; μ] =
    HPow.hPow (α := ℝ) (β := ℕ) ((algebraMap A ℝ : (a : A) → ℝ) c : ℝ) 2 * Var[X; μ]

Tactic:
variance_smul (algebraMap A ℝ c) X μ

Premises used: Real, Algebra.algebraMap, DFunLike.coe, ProbabilityTheory.variance_smul
-- Module: Mathlib.Probability.Moments.Variance
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; μ]
h₁ :
  HPow.hPow (β := ℕ) c 2 • Var[X; μ] = HPow.hPow (α := ℝ) (β := ℕ) ((algebraMap A ℝ : (a : A) → ℝ) c : ℝ) 2 * Var[X; μ]
⊢ Var[c • X; μ] = HPow.hPow (β := ℕ) c 2 • Var[X; μ]

Tactic:
convert! variance_smul (algebraMap A ℝ c) X μ using 1

Premises used: Real, Algebra.algebraMap, DFunLike.coe, ProbabilityTheory.variance_smul
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst : CommSemiring A
inst_1 : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ Var[c • X; μ] = Var[HSMul.hSMul (α := ℝ) ((algebraMap A ℝ : (a : A) → ℝ) c : ℝ) X; μ]

Tactic:
simp only [algebraMap_smul]

Premises used: algebraMap_smul
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
A : Type u_2
inst : CommSemiring A
inst_1 : Algebra A ℝ
c : A
X : Ω → ℝ
μ : Measure Ω
⊢ HPow.hPow (β := ℕ) c 2 • Var[X; μ] = HPow.hPow (α := ℝ) (β := ℕ) ((algebraMap A ℝ : (a : A) → ℝ) c : ℝ) 2 * Var[X; μ]

Tactic:
simp only [Algebra.smul_def, map_pow]

Premises used: map_pow, Algebra.smul_def
-- Module: Mathlib.Probability.Moments.Variance
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
rw₃ 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 ∂μ)
⊢ Var[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]

Premises used: pow_two, ProbabilityTheory.covariance_eq_sub, MeasureTheory.MemLp.aemeasurable, ProbabilityTheory.covariance_self
-- Module: Mathlib.Probability.Moments.Variance
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; μ]
neg : ∀ (hX_Lp : ¬MemLp X 2 μ), Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]
⊢ Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]

Tactic:
by_cases hX_Lp : MemLp X 2 μ

Premises used: MeasureTheory.MemLp, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : MemLp X 2 μ
⊢ Integrable X μ

Tactic:
have hX_int : Integrable X μ := hX_Lp.integrable one_le_two
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : MemLp X 2 μ
hX_int : Integrable X μ
funProp : ‖c‖ₑ ≠ ∞
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ c) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : MemLp X 2 μ
hX_int : Integrable X μ
pos :
  Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω + c - (∫ (a : Ω), X a ∂μ + μ.real Set.univ • c)) 2 ∂μ)
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ)
⊢ Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]

Tactic:
rw [variance_eq_integral (hX.add_const _).aemeasurable,
      integral_add hX_int (by fun_prop), integral_const, variance_eq_integral hX.aemeasurable]

Premises used: ProbabilityTheory.variance_eq_integral, MeasureTheory.AEStronglyMeasurable.aemeasurable, MeasureTheory.AEStronglyMeasurable.add_const, MeasureTheory.integral_const, MeasureTheory.integral_add
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : MemLp X 2 μ
hX_int : Integrable X μ
⊢ Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω + c - (∫ (a : Ω), X a ∂μ + μ.real Set.univ • c)) 2 ∂μ)
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : ¬MemLp X 2 μ
neg : ¬MemLp (ε := ℝ) (fun (x : Ω) ↦ X x + c) 2 μ
⊢ Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]

Tactic:
rw [variance_of_not_memLp (hX.add_const _), variance_of_not_memLp hX hX_Lp]

Premises used: MeasureTheory.AEStronglyMeasurable.add_const, ProbabilityTheory.variance_of_not_memLp
-- Module: Mathlib.Probability.Moments.Variance
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 μ

Tactic:
fun h_memLp ↦ hX_Lp ?_

Premises used: Not
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
hX_Lp : ¬MemLp X 2 μ
neg : ∀ (h_memLp : MemLp (ε := ℝ) (fun (x : Ω) ↦ X x + c) 2 μ), MemLp X 2 μ
⊢ ¬MemLp (ε := ℝ) (fun (x : Ω) ↦ X x + c) 2 μ

Tactic:
refine fun h_memLp ↦ hX_Lp ?_
-- Module: Mathlib.Probability.Moments.Variance
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 μ
h : ∀ (x : Ω), X x = X x + c - c
⊢ X = fun (ω : Ω) ↦ X ω + c - c

Tactic:
ext
-- Module: Mathlib.Probability.Moments.Variance
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 : Ω
⊢ X x = X x + c - c

Tactic:
ring
-- Module: Mathlib.Probability.Moments.Variance
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

Tactic:
have : X = fun ω ↦ X ω + c - c := by ext; ring
-- Module: Mathlib.Probability.Moments.Variance
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
neg : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω + c - c) 2 μ
⊢ MemLp X 2 μ

Tactic:
rw [this]
-- Module: Mathlib.Probability.Moments.Variance
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 (ε := ℝ) (fun (ω : Ω) ↦ X ω + c - c) 2 μ

Tactic:
h_memLp.sub (memLp_const c)

Premises used: MeasureTheory.MemLp.sub, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.Moments.Variance
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 (ε := ℝ) (fun (ω : Ω) ↦ X ω + c - c) 2 μ

Tactic:
exact h_memLp.sub (memLp_const c)

Premises used: MeasureTheory.MemLp.sub, MeasureTheory.memLp_const
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
simp_rw : Var[fun (ω : Ω) ↦ X ω + c; μ] = Var[X; μ]
⊢ Var[fun (ω : Ω) ↦ c + X ω; μ] = Var[X; μ]

Tactic:
simp_rw [add_comm c, variance_add_const hX c]

Premises used: ProbabilityTheory.variance_add_const, add_comm
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ Var[fun (ω : Ω) ↦ -1 * X ω; μ] = HPow.hPow (α := ℝ) (β := ℕ) (-1) 2 * Var[X; μ]

Tactic:
variance_const_mul (-1) X μ

Premises used: OfNat.ofNat, ProbabilityTheory.variance_const_mul, Neg.neg
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : ∀ (x : Ω), Neg.neg = HMul.hMul (α := ℝ) (-1)
h₁ : Var[X; μ] = HPow.hPow (α := ℝ) (β := ℕ) (-1) 2 * Var[X; μ]
⊢ Var[fun (ω : Ω) ↦ -X ω; μ] = Var[X; μ]

Tactic:
convert! variance_const_mul (-1) X μ

Premises used: OfNat.ofNat, ProbabilityTheory.variance_const_mul, Neg.neg
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : Ω
h : ∀ (x : ℝ), -x = -1 * x
⊢ Neg.neg = HMul.hMul (α := ℝ) (-1)

Tactic:
ext
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
x : Ω
x_1 : ℝ
⊢ -x_1 = -1 * x_1

Tactic:
ring
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
⊢ Var[X; μ] = HPow.hPow (α := ℝ) (β := ℕ) (-1) 2 * Var[X; μ]

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

Tactic:
variance_fun_neg

Premises used: ProbabilityTheory.variance_fun_neg
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ -X ω) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsProbabilityMeasure μ
hX : AEStronglyMeasurable X μ
c : ℝ
rw : Var[fun (ω : Ω) ↦ -X ω; μ] = Var[X; μ]
rw₁ rw₂ : Var[X; μ] = Var[X; μ]
⊢ Var[fun (ω : Ω) ↦ c + -X ω; μ] = Var[X; μ]

Tactic:
rw [variance_const_add (by fun_prop) c, variance_fun_neg]

Premises used: ProbabilityTheory.variance_fun_neg, ProbabilityTheory.variance_const_add
-- Module: Mathlib.Probability.Moments.Variance
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 μ
rw₃ : AEMeasurable (X + Y) μ
⊢ Var[X + Y; μ] = Var[X; μ] + 2 * cov[X, Y; μ] + 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]

Premises used: ProbabilityTheory.covariance_add_left, MeasureTheory.MemLp.add, ProbabilityTheory.covariance_add_right, ProbabilityTheory.covariance_comm, ProbabilityTheory.covariance_self
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[X; μ] + cov[Y, X; μ] + (cov[Y, X; μ] + Var[Y; μ]) = Var[X; μ] + 2 * cov[Y, X; μ] + Var[Y; μ]

Tactic:
ring
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable Y μ

Tactic:
hY.aemeasurable

Premises used: MeasureTheory.MemLp.aemeasurable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable Y μ

Tactic:
exact hY.aemeasurable

Premises used: MeasureTheory.MemLp.aemeasurable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable X μ

Tactic:
hX.aemeasurable

Premises used: MeasureTheory.MemLp.aemeasurable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable X μ

Tactic:
exact hX.aemeasurable

Premises used: MeasureTheory.MemLp.aemeasurable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable (X + Y) μ

Tactic:
hX.aemeasurable.add hY.aemeasurable

Premises used: AEMeasurable.add, MeasureTheory.MemLp.aemeasurable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ AEMeasurable (X + Y) μ

Tactic:
exact hX.aemeasurable.add hY.aemeasurable

Premises used: AEMeasurable.add, MeasureTheory.MemLp.aemeasurable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[fun (ω : Ω) ↦ X ω + Y ω; μ] = Var[X; μ] + 2 * cov[X, Y; μ] + Var[Y; μ]

Tactic:
variance_add hX hY

Premises used: ProbabilityTheory.variance_add
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
rw : Var[X; μ] + 2 * -cov[X, Y; μ] + Var[Y; μ] = Var[X; μ] - 2 * cov[X, Y; μ] + Var[Y; μ]
⊢ Var[X - 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]

Premises used: sub_eq_add_neg, ProbabilityTheory.covariance_neg_right, MeasureTheory.MemLp.neg, ProbabilityTheory.variance_add, ProbabilityTheory.variance_neg
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[X; μ] + 2 * -cov[X, Y; μ] + Var[Y; μ] = Var[X; μ] - 2 * cov[X, Y; μ] + Var[Y; μ]

Tactic:
ring
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
hY : MemLp Y 2 μ
⊢ Var[fun (ω : Ω) ↦ X ω - Y ω; μ] = Var[X; μ] - 2 * cov[X, Y; μ] + Var[Y; μ]

Tactic:
variance_sub hX hY

Premises used: ProbabilityTheory.variance_sub
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ ∀ i ∈ s, MemLp (X i) 2 μ

Tactic:
simpa
-- Module: Mathlib.Probability.Moments.Variance
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 μ
rw₂ : AEMeasurable (β := ℝ) (∑ i ∈ s, X i) μ
⊢ Var[∑ i ∈ s, X i; μ] = ∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]

Tactic:
rw [← covariance_self, covariance_sum_left' (by simpa)]

Premises used: ProbabilityTheory.covariance_sum_left', ProbabilityTheory.covariance_self
-- Module: Mathlib.Probability.Moments.Variance
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; μ])

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

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
refine : ∀ (i : ι) (hi : i ∈ s), cov[X i, ∑ i ∈ s, X i; μ] = ∑ j ∈ s, cov[X i, X j; μ]
⊢ Eq (α := ℝ) (∑ i ∈ s, cov[X i, ∑ i ∈ s, X i; μ]) (∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ])

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

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Probability.Moments.Variance
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
⊢ ∀ i ∈ s, MemLp (X i) 2 μ

Tactic:
simpa
-- Module: Mathlib.Probability.Moments.Variance
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
rw rw₁ : Eq (α := ℝ) (∑ i_1 ∈ s, cov[X i, X i_1; μ]) (∑ j ∈ s, cov[X i, X j; μ])
⊢ cov[X i, ∑ i ∈ s, X i; μ] = ∑ j ∈ s, cov[X i, X j; μ]

Tactic:
rw [covariance_sum_right' (by simpa) (hX i hi)]

Premises used: ProbabilityTheory.covariance_sum_right'
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ MemLp (ε := ℝ) (∑ i ∈ s, X i) 2 μ

Tactic:
exact memLp_finsetSum' _ (by simpa)

Premises used: MeasureTheory.memLp_finsetSum'
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
⊢ AEMeasurable (β := ℝ) (∑ i ∈ s, X i) μ

Tactic:
exact (memLp_finsetSum' _ (by simpa)).aemeasurable

Premises used: MeasureTheory.memLp_finsetSum', MeasureTheory.MemLp.aemeasurable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
⊢ Var[∑ i : ι, X i; μ] = ∑ i : ι, ∑ j : ι, cov[X i, X j; μ]

Tactic:
variance_sum' (fun _ _ ↦ hX _)

Premises used: ProbabilityTheory.variance_sum'
-- Module: Mathlib.Probability.Moments.Variance
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; μ]

Tactic:
variance_sum' hX

Premises used: ProbabilityTheory.variance_sum'
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
h : ∀ (x : Ω), Eq (α := ℝ) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)
⊢ Var[fun (ω : Ω) ↦ ∑ i ∈ s, X i ω; μ] = ∑ i ∈ s, ∑ j ∈ s, cov[X i, X j; μ]

Tactic:
convert! variance_sum' hX

Premises used: ProbabilityTheory.variance_sum'
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
s : Finset ι
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
hX : ∀ i ∈ s, MemLp (X i) 2 μ
x : Ω
⊢ Eq (α := ℝ) (∑ i ∈ s, X i x) ((∑ i ∈ s, X i) x)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
⊢ Var[∑ i : ι, X i; μ] = ∑ i : ι, ∑ j : ι, cov[X i, X j; μ]

Tactic:
variance_sum hX

Premises used: ProbabilityTheory.variance_sum
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
h : ∀ (x : Ω), Eq (α := ℝ) (∑ i : ι, X i x) ((∑ i : ι, X i) x)
⊢ Var[fun (ω : Ω) ↦ ∑ i : ι, X i ω; μ] = ∑ i : ι, ∑ j : ι, cov[X i, X j; μ]

Tactic:
convert! variance_sum hX

Premises used: ProbabilityTheory.variance_sum
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : (i : ι) → Ω → ℝ
inst : IsFiniteMeasure μ
inst_1 : Fintype ι
hX : ∀ (i : ι), MemLp (X i) 2 μ
x : Ω
⊢ Eq (α := ℝ) (∑ i : ι, X i x) ((∑ i : ι, X i) x)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
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
rw₁ : AEMeasurable (_m := mΩ) X (Measure.dirac x)
⊢ variance (mΩ := mΩ) X (Measure.dirac x) = 0

Tactic:
rw [variance_eq_integral]

Premises used: ProbabilityTheory.variance_eq_integral
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst : MeasurableSingletonClass Ω
x : Ω
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ mΩ (Measure.dirac x) fun (ω : Ω) ↦
      HPow.hPow (β := ℕ) (X ω - @integral _ _ _ _ mΩ (Measure.dirac x) fun (x : Ω) ↦ X x) 2)
    0

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst : MeasurableSingletonClass Ω
x : Ω
⊢ AEMeasurable (_m := mΩ) X (Measure.dirac x)

Tactic:
aemeasurable_dirac

Premises used: MeasureTheory.aemeasurable_dirac
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
inst : MeasurableSingletonClass Ω
x : Ω
⊢ AEMeasurable (_m := mΩ) X (Measure.dirac x)

Tactic:
exact aemeasurable_dirac

Premises used: MeasureTheory.aemeasurable_dirac