of_enorm_bound — Mathlib

English

If μ is finite and ‖f‖ ≤ C a.e. with C possibly finite, then f ∈ L^p for any p.

Русский

При конечной мере μ и почти всюду ограниченности ‖f‖ ≤ C, функция f принадлежит L^p для любого p.

LaTeX

$$$\text{IsFiniteMeasure}(\mu) \wedge \text{AEStronglyMeasurable}(f,\mu) \wedge (\forall^{\mathrm{a}} x, \|f(x)\| ≤ C) \rightarrow \text{MemLp}(f,p,\mu)$$$

Lean4

theorem of_enorm_bound [IsFiniteMeasure μ] {f : α → ε} (hf : AEStronglyMeasurable f μ) {C : ℝ≥0∞} (hC : C ≠ ∞)
    (hfC : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ C) : MemLp f p μ :=
  by
  apply (memLp_const_enorm hC).of_le_enorm (ε' := ℝ≥0∞) hf <| hfC.mono fun _x hx ↦ ?_
  rw [enorm_eq_self]; exact hx

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