memLp_top_of_bound — Mathlib

English

Same as above for general E-valued functions with essential bound.

Русский

То же самое для функций с значениями в пространстве E, обладающих существенным верхним пределом.

LaTeX

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

Lean4

theorem memLp_top_of_bound {f : α → E} (hf : AEStronglyMeasurable f μ) (C : ℝ) (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) :
    MemLp f ∞ μ :=
  ⟨hf, by
    rw [eLpNorm_exponent_top]
    exact eLpNormEssSup_lt_top_of_ae_bound hfC⟩

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