English
If |f(x)| ≤ c|g(x)| almost everywhere and p > 0, then the eLpNorm' of f is at most c times the eLpNorm' of g.
Русский
Если |f(x)| ≤ c|g(x)| почти повсеместно и p > 0, то eLpNorm'(f) ≤ c · eLpNorm'(g).
LaTeX
$$$\left(\forall^{\ast} x\,\partial\mu, \|f(x)\|_{ε} \le c \cdot \|g(x)\|_{ε}\right) \land p > 0 \Rightarrow eLpNorm'(f,p,\mu) \le c \cdot eLpNorm'(g,p,\mu)$$$
Lean4
theorem eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul {f : α → F} {g : α → G} {c : ℝ≥0}
(h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) {p : ℝ} (hp : 0 < p) : eLpNorm' f p μ ≤ c • eLpNorm' g p μ :=
by
simp_rw [eLpNorm'_eq_lintegral_enorm]
rw [← ENNReal.rpow_le_rpow_iff hp, ENNReal.smul_def, smul_eq_mul, ENNReal.mul_rpow_of_nonneg _ _ hp.le]
simp_rw [← ENNReal.rpow_mul, one_div, inv_mul_cancel₀ hp.ne.symm, ENNReal.rpow_one, enorm, ←
ENNReal.coe_rpow_of_nonneg _ hp.le, ← lintegral_const_mul' _ _ ENNReal.coe_ne_top, ← ENNReal.coe_mul]
apply lintegral_mono_ae
simp_rw [ENNReal.coe_le_coe, ← NNReal.mul_rpow, NNReal.rpow_le_rpow_iff hp]
exact h
