English
If g is AEStronglyMeasurable and |f| ≤ c|g| a.e., then MemLp f p μ with bound c is implied by MemLp g p μ.
Русский
Если g измеримо по силе AEStronglyMeasurable и почти везде выполняется |f| ≤ c|g|, то MemLp f p μ следует из MemLp g p μ.
LaTeX
$$$\text{If } \text{AEStronglyMeasurable}(g,\mu) \land (\forall^{\ast} x, \|f(x)\| ≤ c\|g(x)\|), \Rightarrow \operatorname{MemLp}(f,p,\mu)$.$$
Lean4
/-- If `‖f x‖ₑ ≤ c * ‖g x‖ₑ`, then `eLpNorm f p μ ≤ c * eLpNorm g p μ`.
This version allows `c = ∞`, but requires `g` to be a.e. strongly measurable. -/
theorem eLpNorm_le_mul_eLpNorm_of_ae_le_mul'' {f : α → ε} {c : ℝ≥0∞} {g : α → ε'} (p : ℝ≥0∞)
(hg : AEStronglyMeasurable g μ) (h : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ) : eLpNorm f p μ ≤ c * eLpNorm g p μ :=
by
by_cases h₀ : p = 0
· simp [h₀]
simp only [eLpNorm, h₀, ↓reduceIte, mul_ite]
by_cases hp' : p = ⊤
· simpa [hp'] using eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul' h
· simpa [hp'] using eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul hg h (ENNReal.toReal_pos h₀ hp')
