awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ (∫⁻ (a : Ω), ENNReal.ofReal (|X a| ^ (↑p : ℝ)) ∂μ.tilted fun (x : Ω) ↦ t * X x) < ∞
have neg : Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a| ^ (↑p : ℝ)) (μ.tilted fun (x : Ω) ↦ t * X x)
Tactic: refine Integrable.lintegral_lt_top ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
p : ℝ≥0
hX : AEMeasurable X μ
hp : ¬p = 0
⊢ Integrable (ε := ℝ) (fun (a : Ω) ↦ |X a| ^ (↑p : ℝ)) (μ.tilted fun (x : Ω) ↦ t * X x)
have neg : Integrable (ε := ℝ) (fun (x : Ω) ↦ |X x| ^ (↑p : ℝ) * rexp (t * X x)) μ
Tactic: simp_rw [integrable_tilted_iff (interior_subset (s := integrableExpSet X μ) ht),
    smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ Var[X; μ.tilted fun (x : Ω) ↦ t * X x] = iteratedDeriv 2 (cgf X μ) t
have rw : (∫ (ω : Ω),
    HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ.tilted fun (x : Ω) ↦ t * X x) 2 ∂μ.tilted fun (x : Ω) ↦ t * X x) =
  iteratedDeriv 2 (cgf X μ) t
Tactic: rw [variance_eq_integral]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
rw :
  (∫ (ω : Ω),
      HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ.tilted fun (x : Ω) ↦ t * X x) 2 ∂μ.tilted fun (x : Ω) ↦ t * X x) =
    iteratedDeriv 2 (cgf X μ) t
⊢ Var[X; μ.tilted fun (x : Ω) ↦ t * X x] = iteratedDeriv 2 (cgf X μ) t
have rw₁ : AEMeasurable X (μ.tilted fun (x : Ω) ↦ t * X x)
Tactic: rw [variance_eq_integral]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω),
      HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ.tilted fun (x : Ω) ↦ t * X x) 2 ∂μ.tilted fun (x : Ω) ↦ t * X x) =
    iteratedDeriv 2 (cgf X μ) t
have rw : Eq (α := ℝ) (∫ (ω : Ω), (rexp (t * X ω) / mgf X μ t) • HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) t) 2 ∂μ)
  (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - deriv (cgf X μ) t) 2 * rexp (t * X a) / mgf X μ t ∂μ)
Tactic: rw [integral_tilted_mul_self ht, iteratedDeriv_two_cgf_eq_integral ht, integral_tilted_mul_eq_mgf,
    ← integral_div]
-- Lean 4 proof step from Mathlib.Probability.Moments.Tilted (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ Eq (α := ℝ) (∫ (ω : Ω), rexp (t * X ω) / mgf X μ t * HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) t) 2 ∂μ)
    (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - deriv (cgf X μ) t) 2 * rexp (t * X a) / mgf X μ t ∂μ)
have e_f : ∀ (ω : Ω),
  rexp (t * X ω) / mgf X μ t * HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) t) 2 =
    HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) t) 2 * rexp (t * X ω) / mgf X μ t
Tactic: congr with ω
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
⊢ eVar[X; μ] = eVar[Y; μ]
have simp_rw : ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω - ∫ (a : Ω), Y a ∂μ‖ₑ 2 ∂μ =
  ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖Y ω - ∫ (a : Ω), Y a ∂μ‖ₑ 2 ∂μ
Tactic: simp_rw [evariance, integral_congr_ae h]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω - ∫ (a : Ω), Y a ∂μ‖ₑ 2 ∂μ =
    ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖Y ω - ∫ (a : Ω), Y a ∂μ‖ₑ 2 ∂μ
have h₁ : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : Ω) ↦ HPow.hPow (β := ℕ) ‖X a - ∫ (a : Ω), Y a ∂μ‖ₑ 2) fun (a : Ω) ↦
  HPow.hPow (β := ℕ) ‖Y a - ∫ (a : Ω), Y a ∂μ‖ₑ 2
Tactic: apply lintegral_congr_ae
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : Ω) ↦ HPow.hPow (β := ℕ) ‖X a - ∫ (a : Ω), Y a ∂μ‖ₑ 2) fun (a : Ω) ↦
    HPow.hPow (β := ℕ) ‖Y a - ∫ (a : Ω), Y a ∂μ‖ₑ 2
have h₁ : ∀ (a : Ω),
  Membership.mem (γ := Set Ω)
    {x : Ω |
      Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = Y x) x} x →
        Membership.mem (γ := Set Ω)
          {x : Ω |
            (fun (x : Ω) ↦
                Eq (α := ℝ≥0∞) ((fun (a : Ω) ↦ HPow.hPow (β := ℕ) ‖X a - ∫ (a : Ω), Y a ∂μ‖ₑ 2) x)
                  ((fun (a : Ω) ↦ HPow.hPow (β := ℕ) ‖Y a - ∫ (a : Ω), Y a ∂μ‖ₑ 2) x))
              x}
          x}
    a
Tactic: filter_upwards [h] with ω hω using by simp [hω]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
h₁ :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ X x = Y x) x} x →
          Membership.mem (γ := Set Ω)
            {x : Ω |
              (fun (x : Ω) ↦
                  Eq (α := ℝ≥0∞) ((fun (a : Ω) ↦ HPow.hPow (β := ℕ) ‖X a - ∫ (a : Ω), Y a ∂μ‖ₑ 2) x)
                    ((fun (a : Ω) ↦ HPow.hPow (β := ℕ) ‖Y a - ∫ (a : Ω), Y a ∂μ‖ₑ 2) x))
                x}
            x}
      a
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : Ω) ↦ HPow.hPow (β := ℕ) ‖X a - ∫ (a : Ω), Y a ∂μ‖ₑ 2) fun (a : Ω) ↦
    HPow.hPow (β := ℕ) ‖Y a - ∫ (a : Ω), Y a ∂μ‖ₑ 2
have h₂ : ∀ (a : Ω), X a = Y a → HPow.hPow (β := ℕ) ‖X a - ∫ (a : Ω), Y a ∂μ‖ₑ 2 = HPow.hPow (β := ℕ) ‖Y a - ∫ (a : Ω), Y a ∂μ‖ₑ 2
Tactic: filter_upwards [h] with ω hω using by simp [hω]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ eVar[X; μ] < ∞
have this : HPow.hPow (β := ℕ) (eLpNorm (X - fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ) 2 < ∞
Tactic: have := ENNReal.pow_lt_top (hX.sub <| memLp_const <| μ[X]).2 (n := 2)
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : HPow.hPow (β := ℕ) (eLpNorm (X - fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ) 2 < ∞
⊢ eVar[X; μ] < ∞
have this₁ : HPow.hPow (β := ℝ)
    ((∫⁻ (x : Ω), ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^
      (1 / ENNReal.toReal 2))
    2 <
  ∞
Tactic: rw [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top, ← ENNReal.rpow_two]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
this :
  HPow.hPow (β := ℝ)
      ((∫⁻ (x : Ω), ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ ^ ENNReal.toReal 2 ∂μ) ^
        (1 / ENNReal.toReal 2))
      2 <
    ∞
⊢ eVar[X; μ] < ∞
have this₁ : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2 < ∞
Tactic: simp only [ENNReal.toReal_ofNat, Pi.sub_apply, one_div] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
this :
  HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) (∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) 2⁻¹) 2 < ∞
⊢ eVar[X; μ] < ∞
have this₁ : ∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ < ∞
Tactic: rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
this : ∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ < ∞
⊢ eVar[X; μ] < ∞
have this₁ : ∫⁻ (x : Ω), HPow.hPow (β := ℕ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ < ∞
Tactic: simp_rw [ENNReal.rpow_two] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ eVar[X; μ] = ∞
have by_contra : ∀ (h : ¬eVar[X; μ] = ∞), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : ¬eVar[X; μ] = ∞
⊢ False
have h₁ : eVar[X; μ] < ∞
Tactic: rw [← Ne, ← lt_top_iff_ne_top] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
have refine : eLpNorm (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ < ∞
Tactic: refine ⟨by fun_prop, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ eLpNorm (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ < ∞
have rw : (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / 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 Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ (∫⁻ (x : Ω), ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ ^ ENNReal.toReal 2 ∂μ) ^ (1 / ENNReal.toReal 2) < ∞
have simp : (∫⁻ (x : Ω), HPow.hPow (β := ℕ) ‖X x - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ) ^ HDiv.hDiv (α := ℝ) 1 2 < ∞
Tactic: simp only [ENNReal.toReal_ofNat, ENNReal.rpow_two]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 2
have linarith : HDiv.hDiv (α := ℝ) 1 2 < 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
linarith : HDiv.hDiv (α := ℝ) 1 2 < 0 → 2 / 2 = 1
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 2
have linarith₁ : HDiv.hDiv (α := ℝ) 1 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
linarith : HDiv.hDiv (α := ℝ) 1 2 < 0 → 2 / 2 = 1
linarith₁ : HDiv.hDiv (α := ℝ) 1 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 2
have linarith₂ : HDiv.hDiv (α := ℝ) 1 2 < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
linarith : HDiv.hDiv (α := ℝ) 1 2 < 0 → 2 / 2 = 1
linarith₁ : HDiv.hDiv (α := ℝ) 1 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : HDiv.hDiv (α := ℝ) 1 2 < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ HDiv.hDiv (α := ℝ) 1 2
have linarith₃ : HDiv.hDiv (α := ℝ) 1 2 < 0 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
⊢ False
have this : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
Tactic: have : MemLp (fun ω => X ω - μ[X]) 2 μ := by
    refine ⟨by fun_prop, ?_⟩
    rw [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top]
    simp only [ENNReal.toReal_ofNat, ENNReal.rpow_two]
    exact ENNReal.rpow_lt_top_of_nonneg (by linarith) h.ne
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
⊢ False
have refine : MemLp X 2 μ
Tactic: refine hX ?_
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
⊢ MemLp X 2 μ
have h₁ : X = HAdd.hAdd (α := Ω → ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ
Tactic: convert! this.add (memLp_const μ[X])
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
⊢ X = HAdd.hAdd (α := Ω → ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ
have h₁ : ∀ (ω : Ω),
  X ω = HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) ω
Tactic: ext ω
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
ω : Ω
⊢ X ω = HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) ω
have h₁ : X ω = X ω - ∫ (x : Ω), X x ∂μ + ∫ (x : Ω), X x ∂μ
Tactic: rw [Pi.add_apply, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hXm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
h : eVar[X; μ] < ∞
this : MemLp (ε := ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) 2 μ
ω : Ω
h₁ : X ω = X ω - ∫ (x : Ω), X x ∂μ + ∫ (x : Ω), X x ∂μ
⊢ X ω = HAdd.hAdd (α := Ω → ℝ) (β := Ω → ℝ) (fun (ω : Ω) ↦ X ω - ∫ (x : Ω), X x ∂μ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) ω
have h₂ : X ω = X ω
Tactic: rw [Pi.add_apply, sub_add_cancel]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ eVar[X; μ] < ∞ → MemLp X 2 μ
have contrapose! : ¬MemLp X 2 μ → ∞ ≤ eVar[X; μ]
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬MemLp X 2 μ → ∞ ≤ eVar[X; μ]
have rw : ¬MemLp X 2 μ → eVar[X; μ] = ∞
Tactic: rw [top_le_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
h : Var[X; μ] ≠ 0
⊢ MemLp X 2 μ
have contrapose : ∀ (h : ¬MemLp X 2 μ), Var[X; μ] = 0
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ ENNReal.ofReal Var[X; μ] = eVar[X; μ]
have rw : eVar[X; μ] ≠ ∞
Tactic: rw [variance, ENNReal.ofReal_toReal]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : Var[X; μ] = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ
have rw : ∀ (h : (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) 0),
  ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ
Tactic: rw [variance_eq_integral hX.aemeasurable, integral_eq_zero_iff_of_nonneg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : Var[X; μ] = 0
rw :
  ∀ (h : (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) 0),
    ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ
have hf : ∀ (h : Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ) 0),
  LE.le.{u_1} (α := Ω → ℝ) 0 fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2
Tactic: rw [variance_eq_integral hX.aemeasurable, integral_eq_zero_iff_of_nonneg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : Var[X; μ] = 0
rw :
  ∀ (h : (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) 0),
    ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ
hf :
  ∀ (h : Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ) 0),
    LE.le.{u_1} (α := Ω → ℝ) 0 fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ
have hfi : ∀ (h : Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ) 0),
  Integrable (ε := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) μ
Tactic: rw [variance_eq_integral hX.aemeasurable, integral_eq_zero_iff_of_nonneg] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) 0
⊢ ∀ᵐ (ω : Ω) ∂μ, X ω = ∫ (x : Ω), X x ∂μ
have h₁ : ∀ (ω : Ω) (hω : HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 = 0 ω), X ω = ∫ (x : Ω), X x ∂μ
Tactic: filter_upwards [h] with ω hω
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : (ae μ).EventuallyEq (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) 0
ω : Ω
hω : HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 = 0 ω
⊢ X ω = ∫ (x : Ω), X x ∂μ
have hω₁ : X ω - ∫ (x : Ω), X x ∂μ = 0
Tactic: simp at hω
Cleared hypotheses: hω
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
h : Eq (α := ℝ) (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2 ∂μ) 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) μ
have hfi : Integrable (ε := ℝ)
  (fun (ω : Ω) ↦
    HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * ∫ (x : Ω), X x ∂μ + HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
  μ
Tactic: simp_rw [sub_sq]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ eVar[fun (ω : Ω) ↦ c * X ω; μ] = ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * eVar[X; μ]
have rw : ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ 2 ∂μ =
  ∫⁻ (a : Ω), ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X a - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ
Tactic: rw [evariance, evariance, ← lintegral_const_mul' _ _ ENNReal.ofReal_lt_top.ne]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ 2 ∂μ =
    ∫⁻ (a : Ω), ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X a - ∫ (x : Ω), X x ∂μ‖ₑ 2 ∂μ
have e_f : ∀ (ω : Ω),
  HPow.hPow (β := ℕ) ‖c * X ω - ∫ (x : Ω), c * X x ∂μ‖ₑ 2 =
    ENNReal.ofReal (HPow.hPow (β := ℕ) c 2) * HPow.hPow (β := ℕ) ‖X ω - ∫ (x : Ω), X x ∂μ‖ₑ 2
Tactic: congr with ω
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ
X : Ω → ℝ
μ : Measure Ω
ω : Ω
⊢ 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 * X ω - c * ∫ (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
⊢ 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 * (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
⊢ 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‖ₑ * ‖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
⊢ 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 _)]