evariance_lt_top_iff_memLp — Mathlib

English

Under IsFinite μ and AEStronglyMeasurable X, evariance X μ < ∞ iff MemLp X 2 μ.

Русский

При IsFinite μ и AEStronglyMeasurable X, evariance конечна тогда и только тогда, когда X ∈ L^2(μ).

LaTeX

$$evariance X μ < ∞ ↔ MemLp X 2 μ$$

Lean4

theorem evariance_lt_top_iff_memLp [IsFiniteMeasure μ] (hX : AEStronglyMeasurable X μ) : evariance X μ < ∞ ↔ MemLp X 2 μ
    where
  mp := by contrapose!; rw [top_le_iff]; exact evariance_eq_top hX
  mpr := evariance_lt_top

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