evariance_lt_top — Mathlib

English

If μ is finite and X ∈ L^2(μ), then evariance X μ < ∞.

Русский

Если μ конечна и X ∈ L^2(μ), то evariance X μ < ∞.

LaTeX

$$evariance X μ < ∞$$

Lean4

theorem evariance_lt_top [IsFiniteMeasure μ] (hX : MemLp X 2 μ) : evariance X μ < ∞ :=
  by
  have := ENNReal.pow_lt_top (hX.sub <| memLp_const <| μ[X]).2 (n := 2)
  rw [eLpNorm_eq_lintegral_rpow_enorm two_ne_zero ENNReal.ofNat_ne_top, ← ENNReal.rpow_two] at this
  simp only [ENNReal.toReal_ofNat, Pi.sub_apply, one_div] at this
  rw [← ENNReal.rpow_mul, inv_mul_cancel₀ (two_ne_zero : (2 : ℝ) ≠ 0), ENNReal.rpow_one] at this
  simp_rw [ENNReal.rpow_two] at this
  exact this

Похожие утверждения