English
If g is in L^p(μ) and f is AEStronglyMeasurable with |f| ≤ c|g| almost everywhere, then f is in L^p(μ) and its L^p-norm satisfies ||f||_p ≤ c ||g||_p.
Русский
Пусть g ∈ L^p(μ) и f является AES-измеримой, причем существует c ≥ 0 такое, что |f(x)| ≤ c|g(x)| почти наверняка по μ. Тогда f ∈ L^p(μ) и ||f||_p ≤ c ||g||_p.
LaTeX
$$$g \\in L^{p}(\\mu) \\land f \\text{ AES-measurable} \\land \\exists c \\ge 0 \\; (|f(x)| \\le c \\cdot |g(x)|) \\text{ for μ-almost every } x \\Rightarrow f \\in L^{p}(\\mu) \\land \\|f\\|_{Lp(\\mu)} \\le c \\|g\\|_{Lp(\\mu)}.$$$
Lean4
theorem of_enorm_le_mul {f : α → ε} {g : α → ε'} {c : ℝ≥0} (hg : MemLp g p μ) (hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ) : MemLp f p μ :=
⟨hf,
(eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul' hfg p).trans_lt <|
ENNReal.mul_lt_top ENNReal.coe_lt_top hg.eLpNorm_lt_top⟩
