awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ν
rw : Var[fun (ω : Ω) ↦ f (X ω); μ] = variance (mΩ := mΩ') f (Measure.map X μ)
⊢ Var[fun (ω : Ω) ↦ f (X ω); μ] = Var[f; ν]
have rw₁ : Var[fun (ω : Ω) ↦ f (X ω); μ] = Var[f ∘ X; μ]
Tactic: rw [← hX.map_eq, variance_map (hX.map_eq ▸ hf) hX.aemeasurable, Function.comp_def]
-- 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 ν
rw : Var[fun (ω : Ω) ↦ f (X ω); μ] = variance (mΩ := mΩ') f (Measure.map X μ)
rw₁ : Var[fun (ω : Ω) ↦ f (X ω); μ] = Var[f ∘ X; μ]
⊢ Var[fun (ω : Ω) ↦ f (X ω); μ] = Var[f; ν]
have rw₂ : Var[fun (ω : Ω) ↦ f (X ω); μ] = Var[fun (x : Ω) ↦ f (X x); μ]
Tactic: rw [← hX.map_eq, variance_map (hX.map_eq ▸ hf) hX.aemeasurable, Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
X : Ω → ℝ
Y : Ω' ≃ᵐ Ω
⊢ variance (mΩ := mΩ) X (Measure.map (⇑Y : (a : Ω') → Ω) μ) = Var[X ∘ (⇑Y : (a : Ω') → Ω); μ]
have simp_rw : (evariance (mΩ := mΩ) X (Measure.map (⇑Y : (a : Ω') → Ω) μ)).toReal = eVar[X ∘ (⇑Y : (a : Ω') → Ω); μ].toReal
Tactic: simp_rw [variance, evariance, lintegral_map_equiv, integral_map_equiv, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
X : Ω → ℝ
Y : Ω' ≃ᵐ Ω
simp_rw : (evariance (mΩ := mΩ) X (Measure.map (⇑Y : (a : Ω') → Ω) μ)).toReal = eVar[X ∘ (⇑Y : (a : Ω') → Ω); μ].toReal
⊢ variance (mΩ := mΩ) X (Measure.map (⇑Y : (a : Ω') → Ω) μ) = Var[X ∘ (⇑Y : (a : Ω') → Ω); μ]
have simp_rw₁ : (∫⁻ (ω : Ω),
      HPow.hPow (β := ℕ) ‖X ω - @integral _ _ _ _ mΩ (Measure.map (⇑Y : (a : Ω') → Ω) μ) fun (x : Ω) ↦ X x‖ₑ
        2 ∂Measure.map (⇑Y : (a : Ω') → Ω) μ).toReal =
  (∫⁻ (ω : Ω'),
      HPow.hPow (β := ℕ) ‖(X ∘ (⇑Y : (a : Ω') → Ω)) ω - ∫ (x : Ω'), (X ∘ (⇑Y : (a : Ω') → Ω)) x ∂μ‖ₑ 2 ∂μ).toReal
Tactic: simp_rw [variance, evariance, lintegral_map_equiv, integral_map_equiv, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
X : Ω → ℝ
Y : Ω' ≃ᵐ Ω
simp_rw : (evariance (mΩ := mΩ) X (Measure.map (⇑Y : (a : Ω') → Ω) μ)).toReal = eVar[X ∘ (⇑Y : (a : Ω') → Ω); μ].toReal
simp_rw₁ :
  (∫⁻ (ω : Ω),
        HPow.hPow (β := ℕ) ‖X ω - @integral _ _ _ _ mΩ (Measure.map (⇑Y : (a : Ω') → Ω) μ) fun (x : Ω) ↦ X x‖ₑ
          2 ∂Measure.map (⇑Y : (a : Ω') → Ω) μ).toReal =
    (∫⁻ (ω : Ω'),
        HPow.hPow (β := ℕ) ‖(X ∘ (⇑Y : (a : Ω') → Ω)) ω - ∫ (x : Ω'), (X ∘ (⇑Y : (a : Ω') → Ω)) x ∂μ‖ₑ 2 ∂μ).toReal
⊢ variance (mΩ := mΩ) X (Measure.map (⇑Y : (a : Ω') → Ω) μ) = Var[X ∘ (⇑Y : (a : Ω') → Ω); μ]
have simp_rw₂ : (∫⁻ (a : Ω'),
      HPow.hPow (β := ℕ)
        ‖X ((Y : (a : Ω') → Ω) a) - @integral _ _ _ _ mΩ (Measure.map (⇑Y : (a : Ω') → Ω) μ) fun (x : Ω) ↦ X x‖ₑ
        2 ∂μ).toReal =
  (∫⁻ (ω : Ω'),
      HPow.hPow (β := ℕ) ‖(X ∘ (⇑Y : (a : Ω') → Ω)) ω - ∫ (x : Ω'), (X ∘ (⇑Y : (a : Ω') → Ω)) x ∂μ‖ₑ 2 ∂μ).toReal
Tactic: simp_rw [variance, evariance, lintegral_map_equiv, integral_map_equiv, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
Ω' : Type u_3
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
X : Ω → ℝ
Y : Ω' ≃ᵐ Ω
simp_rw : (evariance (mΩ := mΩ) X (Measure.map (⇑Y : (a : Ω') → Ω) μ)).toReal = eVar[X ∘ (⇑Y : (a : Ω') → Ω); μ].toReal
simp_rw₁ :
  (∫⁻ (ω : Ω),
        HPow.hPow (β := ℕ) ‖X ω - @integral _ _ _ _ mΩ (Measure.map (⇑Y : (a : Ω') → Ω) μ) fun (x : Ω) ↦ X x‖ₑ
          2 ∂Measure.map (⇑Y : (a : Ω') → Ω) μ).toReal =
    (∫⁻ (ω : Ω'),
        HPow.hPow (β := ℕ) ‖(X ∘ (⇑Y : (a : Ω') → Ω)) ω - ∫ (x : Ω'), (X ∘ (⇑Y : (a : Ω') → Ω)) x ∂μ‖ₑ 2 ∂μ).toReal
simp_rw₂ :
  (∫⁻ (a : Ω'),
        HPow.hPow (β := ℕ)
          ‖X ((Y : (a : Ω') → Ω) a) - @integral _ _ _ _ mΩ (Measure.map (⇑Y : (a : Ω') → Ω) μ) fun (x : Ω) ↦ X x‖ₑ
          2 ∂μ).toReal =
    (∫⁻ (ω : Ω'),
        HPow.hPow (β := ℕ) ‖(X ∘ (⇑Y : (a : Ω') → Ω)) ω - ∫ (x : Ω'), (X ∘ (⇑Y : (a : Ω') → Ω)) x ∂μ‖ₑ 2 ∂μ).toReal
⊢ variance (mΩ := mΩ) X (Measure.map (⇑Y : (a : Ω') → Ω) μ) = Var[X ∘ (⇑Y : (a : Ω') → Ω); μ]
have simp_rw₃ : (∫⁻ (a : Ω'), HPow.hPow (β := ℕ) ‖X ((Y : (a : Ω') → Ω) a) - ∫ (x : Ω'), X ((Y : (a : Ω') → Ω) x) ∂μ‖ₑ 2 ∂μ).toReal =
  (∫⁻ (ω : Ω'),
      HPow.hPow (β := ℕ) ‖(X ∘ (⇑Y : (a : Ω') → Ω)) ω - ∫ (x : Ω'), (X ∘ (⇑Y : (a : Ω') → Ω)) x ∂μ‖ₑ 2 ∂μ).toReal
Tactic: simp_rw [variance, evariance, lintegral_map_equiv, integral_map_equiv, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
⊢ Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ
have pos : ∀ (hX : MemLp X 2 μ), Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ
Tactic: by_cases hX : MemLp X 2 μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
pos : ∀ (hX : MemLp X 2 μ), Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ
⊢ Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ
have neg : ∀ (hX : ¬MemLp X 2 μ), Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ
Tactic: by_cases hX : MemLp X 2 μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : MemLp X 2 μ
⊢ Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ
have pos : ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 ≤
  ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ
Tactic: rw [variance_eq_sub hX]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ
have neg : LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
Tactic: rw [variance, evariance_eq_lintegral_ofReal, ← integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
neg :
  LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
⊢ Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ
have neg₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2
Tactic: rw [variance, evariance_eq_lintegral_ofReal, ← integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
neg :
  LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
neg₁ : (ae μ).EventuallyLE (β := ℝ) 0 fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2
⊢ Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ
have neg₂ : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) μ
Tactic: rw [variance, evariance_eq_lintegral_ofReal, ← integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
have pos : ∀ (hint : Integrable X μ),
  LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
Tactic: by_cases hint : Integrable X μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
pos :
  ∀ (hint : Integrable X μ),
    LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ)
      (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
⊢ LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
have neg : ∀ (hint : ¬Integrable X μ),
  LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
Tactic: by_cases hint : Integrable X μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : ¬Integrable X μ
⊢ LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
have neg : LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 ∂μ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 ∂μ)
Tactic: simp only [integral_undef hint, Pi.pow_apply, sub_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
have pos : LE.le (α := ℝ) 0 (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
Tactic: rw [integral_undef]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
pos : LE.le (α := ℝ) 0 (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
⊢ LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)
have pos₁ : ¬Integrable (ε := ℝ) (fun (a : Ω) ↦ HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2) μ
Tactic: rw [integral_undef]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
h : Integrable (ε := ℝ) (fun (a : Ω) ↦ HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2) μ
⊢ False
have A : MemLp (X - fun (ω : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ
Tactic: have A : MemLp (X - fun ω : Ω => μ[X]) 2 μ :=
        (memLp_two_iff_integrable_sq (by fun_prop)).2 h
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
h : Integrable (ε := ℝ) (fun (a : Ω) ↦ HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2) μ
A : MemLp (X - fun (ω : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ
⊢ False
have B : MemLp (ε := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ
Tactic: have B : MemLp (fun _ : Ω => μ[X]) 2 μ := memLp_const _
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
h : Integrable (ε := ℝ) (fun (a : Ω) ↦ HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2) μ
A : MemLp (X - fun (ω : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ
B : MemLp (ε := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ
⊢ False
have pos : MemLp X 2 μ
Tactic: apply hX
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
h : Integrable (ε := ℝ) (fun (a : Ω) ↦ HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2) μ
A : MemLp (X - fun (ω : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ
B : MemLp (ε := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ
⊢ MemLp X 2 μ
have h₁ : X = (X - fun (ω : Ω) ↦ ∫ (x : Ω), X x ∂μ) + fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ
Tactic: convert! A.add B
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
⊢ eVar[X; μ] =
    ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
have pos : ∀ (hℒ : MemLp X 2 μ),
  eVar[X; μ] =
    ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
Tactic: by_cases hℒ : MemLp X 2 μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
pos :
  ∀ (hℒ : MemLp X 2 μ),
    eVar[X; μ] =
      ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
⊢ eVar[X; μ] =
    ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
have neg : ∀ (hℒ : ¬MemLp X 2 μ),
  eVar[X; μ] =
    ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
Tactic: by_cases hℒ : MemLp X 2 μ
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ eVar[X; μ] =
    ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
have pos : ENNReal.ofReal (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) -
    ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
  ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
Tactic: rw [← ofReal_variance hℒ, variance_eq_sub hℒ, ENNReal.ofReal_sub _ (sq_nonneg _)]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) -
      ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
    ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
have pos : ENNReal.ofReal (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) = ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) = ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ
have pos : ENNReal.ofReal (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) = ∫⁻ (ω : Ω), (↑‖HPow.hPow (β := ℕ) (X ω) 2‖₊ : ℝ≥0∞) ∂μ
Tactic: simp_rw [← enorm_pow, enorm]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ ENNReal.ofReal (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) = ∫⁻ (ω : Ω), (↑‖HPow.hPow (β := ℕ) (X ω) 2‖₊ : ℝ≥0∞) ∂μ
have pos : ENNReal.ofReal (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) =
  ENNReal.ofReal (∫ (a : Ω), (↑‖HPow.hPow (β := ℕ) (X a) 2‖₊ : ℝ) ∂μ)
Tactic: rw [lintegral_coe_eq_integral]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
pos :
  ENNReal.ofReal (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) =
    ENNReal.ofReal (∫ (a : Ω), (↑‖HPow.hPow (β := ℕ) (X a) 2‖₊ : ℝ) ∂μ)
⊢ ENNReal.ofReal (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) = ∫⁻ (ω : Ω), (↑‖HPow.hPow (β := ℕ) (X ω) 2‖₊ : ℝ≥0∞) ∂μ
have pos₁ : Integrable (ε := ℝ) (fun (x : Ω) ↦ (↑‖HPow.hPow (β := ℕ) (X x) 2‖₊ : ℝ)) μ
Tactic: rw [lintegral_coe_eq_integral]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ eVar[X; μ] =
    ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)
have neg : ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
  eVar[X; μ]
Tactic: symm
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
    eVar[X; μ]
have neg : ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ = ∞ ∧ ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) ≠ ∞
Tactic: rw [evariance_eq_top hX hℒ, ENNReal.sub_eq_top_iff]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ = ∞ ∧
    ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) ≠ ∞
have neg : ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ = ∞
Tactic: refine ⟨?_, ENNReal.ofReal_ne_top⟩
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ = ∞
have hℒ₁ : AEStronglyMeasurable X μ → ¬eLpNorm X 2 μ < ∞
Tactic: rw [MemLp, not_and] at hℒ
Cleared hypotheses: hℒ
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : AEStronglyMeasurable X μ → ¬eLpNorm X 2 μ < ∞
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ = ∞
have hℒ₁ : ¬eLpNorm X 2 μ < ∞
Tactic: specialize hℒ hX
Cleared hypotheses: hℒ
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬eLpNorm X 2 μ < ∞
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ = ∞
have hℒ₁ : (¬¬∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x‖ₑ 2 ∂μ = 0 → LE.le (α := ℝ) 0 2) → ∫⁻ (x : Ω), HPow.hPow (β := ℝ) ‖X x‖ₑ 2 ∂μ = ∞
Tactic: simp only [eLpNorm_eq_lintegral_rpow_enorm_toReal two_ne_zero ENNReal.ofNat_ne_top, not_lt,
      top_le_iff, ENNReal.toReal_ofNat, one_div, ENNReal.rpow_eq_top_iff, inv_lt_zero, inv_pos,
      and_true, or_iff_not_imp_left, not_and_or, zero_lt_two] at hℒ
Cleared hypotheses: hℒ
-- 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
⊢ (↑c : ℝ≥0∞) ≠ 0
have rwa : ¬(↑c : ℝ≥0∞) = 0
Tactic: rwa [Ne, ENNReal.coe_eq_zero]
-- 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
rwa : ¬(↑c : ℝ≥0∞) = 0
⊢ (↑c : ℝ≥0∞) ≠ 0
have rwa₁ : ¬c = 0
Tactic: rwa [Ne, ENNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
⊢ (μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤
    eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2
have A : (↑c : ℝ≥0∞) ≠ 0
Tactic: have A : (c : ℝ≥0∞) ≠ 0 := by rwa [Ne, ENNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Moments.Variance (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
c : ℝ≥0
hc : c ≠ 0
A : (↑c : ℝ≥0∞) ≠ 0
⊢ (μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤
    eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2
have B : AEStronglyMeasurable (β := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) μ
Tactic: have B : AEStronglyMeasurable (fun _ : Ω => μ[X]) μ := aestronglyMeasurable_const
-- 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 ∂μ) μ
⊢ (μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤
    eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)
  ((μ : (a : Set Ω) → ℝ≥0∞) {x : Ω | (↑c : ℝ≥0∞) ≤ ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ} :
    ℝ≥0∞)
Tactic: convert!
      meas_ge_le_mul_pow_eLpNorm_enorm μ two_ne_zero ENNReal.ofNat_ne_top (hX.sub B) A (by simp)
    using 1
-- 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 :
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) {x : Ω | (↑c : ℝ≥0∞) ≤ ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ} :
      ℝ≥0∞)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} ≤
    eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2
have h₁ : eVar[X; μ] / HPow.hPow (β := ℕ) (↑c : ℝ≥0∞) 2 =
  (↑c : ℝ≥0∞)⁻¹ ^ ENNReal.toReal 2 * eLpNorm (X - fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ ^ ENNReal.toReal 2
Tactic: convert!
      meas_ge_le_mul_pow_eLpNorm_enorm μ two_ne_zero ENNReal.ofNat_ne_top (hX.sub B) A (by simp)
    using 1
-- 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 ∂μ) μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)
    ((μ : (a : Set Ω) → ℝ≥0∞) {x : Ω | (↑c : ℝ≥0∞) ≤ ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖ₑ} :
      ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) {ω : Ω | (↑c : ℝ) ≤ |X ω - ∫ (x : Ω), X x ∂μ|} : ℝ≥0∞)
  ((μ : (a : Set Ω) → ℝ≥0∞) {x : Ω | c ≤ ‖HSub.hSub (β := Ω → ℝ) X (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) x‖₊} : ℝ≥0∞)
Tactic: norm_cast