English
If |f| ≤ c|g| a.e., then eLpNorm f p μ ≤ c · eLpNorm g p μ for any p > 0 (in NNReal or ENNReal sense).
Русский
Если |f| ≤ c|g| почти всюду, то eLpNorm f p μ ≤ c·eLpNorm g p μ для любого p>0.
LaTeX
$$$\forall a.e. \|f\| ≤ c \|g\| \Rightarrow eLpNorm f p μ ≤ c \, eLpNorm g p μ\quad( p>0 )$$$
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 : ℝ≥0∞) : eLpNorm f p μ ≤ c • eLpNorm g p μ :=
by
by_cases h0 : p = 0
· simp [h0]
by_cases h_top : p = ∞
· rw [h_top]
exact eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul h
simp_rw [eLpNorm_eq_eLpNorm' h0 h_top]
exact
eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul h
(ENNReal.toReal_pos h0 h_top)
-- TODO: add the whole family of lemmas?