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 measure of the whole space to the power 1/p.
Русский
Если функционал f почти всюду ограничен на NNReal границей C, тогда eLpNorm f ≤ C · μ(α)^{1/p}.
LaTeX
$$$\text{If } hfC:\forall^{\mathrm{a}} x\partial\mu,\; \|f(x)\|_{e}\le C, \text{ then } eLpNorm\; f\; p\; μ \le C \cdot μ(\mathrm{Set.univ})^{\frac{1}{p}}.$$$
Lean4
theorem eLpNorm_le_of_ae_enorm_bound {ε} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {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 (Preorder.le_refl C)
refine (eLpNorm_mono_enorm_ae this).trans_eq ?_
rw [eLpNorm_const _ hp (NeZero.ne μ), one_div, enorm_eq_self, smul_eq_mul]
