eLpNorm_le_of_ae_nnnorm_bound — Mathlib

English

If f is essentially bounded by a NNReal bound C almost everywhere, then the eLp norm of f is bounded by C times the universe measure to the 1/p power.

Русский

Если f почти всюду ограничена NNReal границей C, то eLpNorm f ≤ C · μ(univ)^{1/p}.

LaTeX

$$$\text{If } hfC:\forall^{\mathrm{a}} x\partial\mu,\; \|f(x)\|_{nn} ≤ C, \text{ then } eLpNorm\; f\; p\; μ ≤ C \cdot μ(\mathrm{Set.univ})^{\frac{1}{p}}.$$$

Lean4

theorem eLpNorm_le_of_ae_nnnorm_bound {f : α → F} {C : ℝ≥0} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) :
    eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹ :=
  by
  rcases eq_zero_or_neZero μ with rfl | hμ
  · simp
  by_cases hp : p = 0
  · simp [hp]
  have : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖(C : ℝ)‖₊ := hfC.mono fun x hx => hx.trans_eq C.nnnorm_eq.symm
  refine (eLpNorm_mono_ae this).trans_eq ?_
  rw [eLpNorm_const _ hp (NeZero.ne μ), C.enorm_eq, one_div, ENNReal.smul_def, smul_eq_mul]

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