English
If |f| ≤ c|g| almost everywhere, then eLpNorm' of f is bounded by c times eLpNorm' of g for any p > 0, including variants with real-valued or NNReal constants.
Русский
Если |f| ≤ c|g| почти всюду, то eLpNorm'(f) ограничена сверху на c·eLpNorm'(g) для любого p > 0, включая варианты с коэффициентами NNReal.
LaTeX
$$$\text{If } \forall^{\ast} x, \|f(x)\|_{ε} \le c \cdot \|g(x)\|_{ε} \text{, then } eLpNorm'(f,p,\mu) \le c \cdot eLpNorm'(g,p,\mu)\text{ for } p>0.$$$
Lean4
theorem eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul' {f : α → ε} {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', ENNReal.rpow_one, ← ENNReal.coe_rpow_of_nonneg _ hp.le,
← lintegral_const_mul' _ _ ENNReal.coe_ne_top]
apply lintegral_mono_ae
have aux (x) : (↑c) ^ p * ‖g x‖ₑ ^ p = (↑c * ‖g x‖ₑ) ^ p :=
by
have : ¬(p < 0) := by linarith
simp [ENNReal.mul_rpow_eq_ite, this]
simpa [ENNReal.coe_rpow_of_nonneg _ hp.le, aux, ENNReal.rpow_le_rpow_iff hp]
