awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.Variance
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 μ)
rw₂ :
  AEStronglyMeasurable (β := ℝ) (m₀ := mΩ)
    (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - @integral _ _ _ _ mΩ (Measure.map Y μ) fun (x : Ω) ↦ X x) 2)
    (Measure.map Y μ)
⊢ variance (mΩ := mΩ) X (Measure.map Y μ) = Var[X ∘ Y; μ]

Tactic:
rw [variance_eq_integral hX, integral_map hY, variance_eq_integral (hX.comp_aemeasurable hY),
    integral_map hY]

Premises used: ProbabilityTheory.variance_eq_integral, MeasureTheory.integral_map, AEMeasurable.comp_aemeasurable
-- Module: Mathlib.Probability.Moments.Variance
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 μ
⊢ Eq (α := ℝ) (∫ (x : Ω'), HPow.hPow (β := ℕ) (X (Y x) - ∫ (x : Ω'), X (Y x) ∂μ) 2 ∂μ)
    (∫ (ω : Ω'), HPow.hPow (β := ℕ) ((X ∘ Y) ω - ∫ (x : Ω'), (X ∘ Y) x ∂μ) 2 ∂μ)

Tactic:
congr
-- Module: Mathlib.Probability.Moments.Variance
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Ω) X (Measure.map Y μ)

Tactic:
hX.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.Variance
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Ω) X (Measure.map Y μ)

Tactic:
exact hX.aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.Variance
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 μ)

Tactic:
AEStronglyMeasurable.pow ?_ _

Premises used: MeasureTheory.AEStronglyMeasurable.pow
-- Module: Mathlib.Probability.Moments.Variance
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 μ
refine :
  AEStronglyMeasurable (β := ℝ) (m₀ := mΩ)
    (fun (ω : Ω) ↦ X ω - @integral _ _ _ _ mΩ (Measure.map Y μ) fun (x : Ω) ↦ X x) (Measure.map Y μ)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := mΩ)
    (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - @integral _ _ _ _ mΩ (Measure.map Y μ) fun (x : Ω) ↦ X x) 2)
    (Measure.map Y μ)

Tactic:
refine AEStronglyMeasurable.pow ?_ _

Premises used: MeasureTheory.AEStronglyMeasurable.pow
-- Module: Mathlib.Probability.Moments.Variance
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 μ
⊢ AEMeasurable (β := ℝ) (_m := mΩ) (fun (ω : Ω) ↦ X ω - @integral _ _ _ _ mΩ (Measure.map Y μ) fun (x : Ω) ↦ X x)
    (Measure.map Y μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Variance
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 (ω : Ω) ↦ X ω - @integral _ _ _ _ mΩ (Measure.map Y μ) fun (x : Ω) ↦ X x) (Measure.map Y μ)

Tactic:
exact AEMeasurable.aestronglyMeasurable (by fun_prop)

Premises used: AEMeasurable.aestronglyMeasurable
-- Module: Mathlib.Probability.Moments.Variance
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; μ]
rw₂ rw₃ : Var[fun (ω : Ω) ↦ f (X ω); μ] = Var[fun (x : Ω) ↦ f (X x); μ]
⊢ Var[fun (ω : Ω) ↦ f (X ω); μ] = Var[f; ν]

Tactic:
rw [← hX.map_eq, variance_map (hX.map_eq ▸ hf) hX.aemeasurable, Function.comp_def]

Premises used: MeasureTheory.MeasurePreserving.aemeasurable, MeasureTheory.MeasurePreserving.map_eq, Function.comp_def, ProbabilityTheory.variance_map
-- Module: Mathlib.Probability.Moments.Variance
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
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
⊢ variance (mΩ := mΩ) X (Measure.map (⇑Y : (a : Ω') → Ω) μ) = Var[X ∘ (⇑Y : (a : Ω') → Ω); μ]

Tactic:
simp_rw [variance, evariance, lintegral_map_equiv, integral_map_equiv, Function.comp_apply]

Premises used: MeasureTheory.integral_map_equiv, ProbabilityTheory.variance, Function.comp_apply, MeasureTheory.lintegral_map_equiv, ProbabilityTheory.evariance
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
hX : AEMeasurable X μ
⊢ variance (mΩ := Real.measurableSpace) id (Measure.map X μ) = Var[X; μ]

Tactic:
simp [variance_map measurable_id.aemeasurable hX]

Premises used: Measurable.aemeasurable, measurable_id, ProbabilityTheory.variance_map
-- Module: Mathlib.Probability.Moments.Variance
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 ∂μ
neg : ∀ (hX : ¬MemLp X 2 μ), Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ
⊢ Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ

Tactic:
by_cases hX : MemLp X 2 μ

Premises used: MeasureTheory.MemLp, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : MemLp X 2 μ
pos :
  ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 ≤
    ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ
⊢ Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ

Tactic:
rw [variance_eq_sub hX]

Premises used: ProbabilityTheory.variance_eq_sub
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ - HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2 ≤
    ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ

Tactic:
simp only [sq_nonneg, sub_le_self_iff]

Premises used: sq_nonneg, sub_le_self_iff
-- Module: Mathlib.Probability.Moments.Variance
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
neg₂ : AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) μ
⊢ Var[X; μ] ≤ ∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ

Tactic:
rw [variance, evariance_eq_lintegral_ofReal, ← integral_eq_lintegral_of_nonneg_ae]

Premises used: ProbabilityTheory.evariance_eq_lintegral_ofReal, ProbabilityTheory.variance, MeasureTheory.integral_eq_lintegral_of_nonneg_ae
-- Module: Mathlib.Probability.Moments.Variance
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 ∂μ)
neg :
  ∀ (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 ∂μ)

Tactic:
by_cases hint : Integrable X μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : ¬Integrable X μ
neg : LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 ∂μ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 ∂μ)
⊢ LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)

Tactic:
simp only [integral_undef hint, Pi.pow_apply, sub_zero]

Premises used: sub_zero, MeasureTheory.integral_undef, Pi.pow_apply
-- Module: Mathlib.Probability.Moments.Variance
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) 2 ∂μ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 ∂μ)

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Moments.Variance
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) 2 ∂μ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 ∂μ)

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Moments.Variance
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 ∂μ)
pos₁ : ¬Integrable (ε := ℝ) (fun (a : Ω) ↦ HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2) μ
⊢ LE.le (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a - ∫ (x : Ω), X x ∂μ) 2 ∂μ) (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)

Tactic:
rw [integral_undef]

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)

Tactic:
integral_nonneg fun a => sq_nonneg _

Premises used: MeasureTheory.integral_nonneg, sq_nonneg
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
hint : Integrable X μ
⊢ LE.le (α := ℝ) 0 (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ)

Tactic:
exact integral_nonneg fun a => sq_nonneg _

Premises used: MeasureTheory.integral_nonneg
-- Module: Mathlib.Probability.Moments.Variance
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) μ
⊢ AEStronglyMeasurable (X - fun (ω : Ω) ↦ ∫ (x : Ω), X x ∂μ) μ

Tactic:
fun_prop
-- Module: Mathlib.Probability.Moments.Variance
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) μ
⊢ 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
-- Module: Mathlib.Probability.Moments.Variance
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 μ
⊢ MemLp (ε := ℝ) (fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ

Tactic:
have B : MemLp (fun _ : Ω => μ[X]) 2 μ := memLp_const _
-- Module: Mathlib.Probability.Moments.Variance
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 μ
pos : MemLp X 2 μ
⊢ False

Tactic:
apply hX
-- Module: Mathlib.Probability.Moments.Variance
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 - fun (ω : Ω) ↦ ∫ (x : Ω), X x ∂μ) + fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ) 2 μ

Tactic:
A.add B

Premises used: MeasureTheory.MemLp.add
-- Module: Mathlib.Probability.Moments.Variance
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 μ
h₁ : X = (X - fun (ω : Ω) ↦ ∫ (x : Ω), X x ∂μ) + fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ
⊢ MemLp X 2 μ

Tactic:
convert! A.add B

Premises used: MeasureTheory.MemLp.add
-- Module: Mathlib.Probability.Moments.Variance
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 μ
⊢ X = (X - fun (ω : Ω) ↦ ∫ (x : Ω), X x ∂μ) + fun (x : Ω) ↦ ∫ (x : Ω), X x ∂μ

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2

Tactic:
Eventually.of_forall fun x => sq_nonneg _

Premises used: HSub.hSub, Filter.Eventually.of_forall, MeasureTheory.integral, sq_nonneg, Filter.EventuallyLE
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ (ae μ).EventuallyLE (β := ℝ) 0 fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2

Tactic:
exact Eventually.of_forall fun x => sq_nonneg _

Premises used: Filter.Eventually.of_forall, sq_nonneg
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) μ

Tactic:
(AEMeasurable.pow_const (hm.aemeasurable.sub_const _) _).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.sub_const
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hm : AEStronglyMeasurable X μ
hX : ¬MemLp X 2 μ
⊢ AEStronglyMeasurable (β := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - ∫ (x : Ω), X x ∂μ) 2) μ

Tactic:
exact (AEMeasurable.pow_const (hm.aemeasurable.sub_const _) _).aestronglyMeasurable

Premises used: AEMeasurable.aestronglyMeasurable, AEMeasurable.pow_const, MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.sub_const
-- Module: Mathlib.Probability.Moments.Variance
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)
neg :
  ∀ (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)

Tactic:
by_cases hℒ : MemLp X 2 μ

Premises used: MeasureTheory.MemLp, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.Variance
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 (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
    ∫⁻ (ω : Ω), 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)

Tactic:
rw [← ofReal_variance hℒ, variance_eq_sub hℒ, ENNReal.ofReal_sub _ (sq_nonneg _)]

Premises used: ProbabilityTheory.variance_eq_sub, sq_nonneg, ENNReal.ofReal_sub, ProbabilityTheory.ofReal_variance
-- Module: Mathlib.Probability.Moments.Variance
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 ∂μ) = ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖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)

Tactic:
congr
-- Module: Mathlib.Probability.Moments.Variance
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 ∂μ) = ∫⁻ (ω : Ω), (↑‖HPow.hPow (β := ℕ) (X ω) 2‖₊ : ℝ≥0∞) ∂μ
⊢ ENNReal.ofReal (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) = ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ

Tactic:
simp_rw [← enorm_pow, enorm]

Premises used: ENorm.enorm, enorm_pow
-- Module: Mathlib.Probability.Moments.Variance
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‖₊ : ℝ) ∂μ)
pos₁ : Integrable (ε := ℝ) (fun (x : Ω) ↦ (↑‖HPow.hPow (β := ℕ) (X x) 2‖₊ : ℝ)) μ
⊢ ENNReal.ofReal (∫ (x : Ω), HPow.hPow (β := ℕ) X 2 x ∂μ) = ∫⁻ (ω : Ω), (↑‖HPow.hPow (β := ℕ) (X ω) 2‖₊ : ℝ≥0∞) ∂μ

Tactic:
rw [lintegral_coe_eq_integral]

Premises used: MeasureTheory.lintegral_coe_eq_integral
-- Module: Mathlib.Probability.Moments.Variance
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 (∫ (a : Ω), (↑‖HPow.hPow (β := ℕ) (X a) 2‖₊ : ℝ) ∂μ)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : MemLp X 2 μ
⊢ Integrable (ε := ℝ) (fun (x : Ω) ↦ (↑‖HPow.hPow (β := ℕ) (X x) 2‖₊ : ℝ)) μ

Tactic:
simpa using hℒ.abs.integrable_sq

Premises used: MeasureTheory.MemLp.integrable_sq, MeasureTheory.MemLp.abs
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
neg :
  ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
    eVar[X; μ]
⊢ eVar[X; μ] =
    ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2)

Tactic:
symm
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
neg :
  ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ = ∞ ∧
    ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) ≠ ∞
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ - ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) =
    eVar[X; μ]

Tactic:
rw [evariance_eq_top hX hℒ, ENNReal.sub_eq_top_iff]

Premises used: ENNReal.sub_eq_top_iff, ProbabilityTheory.evariance_eq_top
-- Module: Mathlib.Probability.Moments.Variance
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) ≠ ∞

Tactic:
⟨?_, ENNReal.ofReal_ne_top⟩

Premises used: And.intro, ENNReal.ofReal_ne_top
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
neg : ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ = ∞
⊢ ∫⁻ (ω : Ω), HPow.hPow (β := ℕ) ‖X ω‖ₑ 2 ∂μ = ∞ ∧
    ENNReal.ofReal (HPow.hPow (α := ℝ) (β := ℕ) (∫ (x : Ω), X x ∂μ) 2) ≠ ∞

Tactic:
refine ⟨?_, ENNReal.ofReal_ne_top⟩
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : ¬MemLp X 2 μ
⊢ AEStronglyMeasurable X μ → ¬eLpNorm X 2 μ < ∞

Tactic:
rw [MemLp, not_and] at hℒ

Premises used: MeasureTheory.MemLp, not_and
-- Module: Mathlib.Probability.Moments.Variance
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
X : Ω → ℝ
hX : AEStronglyMeasurable X μ
hℒ : AEStronglyMeasurable X μ → ¬eLpNorm X 2 μ < ∞
⊢ ¬eLpNorm X 2 μ < ∞

Tactic:
specialize hℒ hX