eLpNormEssSup_lt_top_iff_isBoundedUnder

English

eLpNormEssSup f μ < ∞ if and only if the family {‖f x‖} is bounded almost everywhere

Русский

eLpNormEssSup f μ < ∞ тогда и только тогда, когда family ‖f x‖ ограничено почти повсеместно.

LaTeX

$$eLpNormEssSup f μ < ⊤ ↔ IsBoundedUnder (· ≤ ·) (ae μ) (fun x => ‖f x‖₊)$$

Lean4

theorem eLpNormEssSup_lt_top_iff_isBoundedUnder : eLpNormEssSup f μ < ⊤ ↔ IsBoundedUnder (· ≤ ·) (ae μ) fun x ↦ ‖f x‖₊
    where
  mp
    h :=
    ⟨(eLpNormEssSup f μ).toNNReal, by simp_rw [← ENNReal.coe_le_coe, ENNReal.coe_toNNReal h.ne];
      exact ae_le_eLpNormEssSup⟩
  mpr := by rintro ⟨C, hC⟩; exact eLpNormEssSup_lt_top_of_ae_nnnorm_bound (C := C) hC

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