English
If |f(x)| ≤ c|g(x)| almost everywhere, then the essential supremum-based Lp norm of f is bounded by c times that of g.
Русский
Если |f(x)| ≤ c|g(x)| почти везде, то ess sup-основанная Lp-норма f ограничена c-умноженным на ess sup-норму g.
LaTeX
$$$\\text{essSup}(\\|f\\|) \\le c \\; \\text{essSup}(\\|g\\|) \\quad\\Rightarrow\\quad eLpNormEssSup(f,μ) \\le c \\cdot eLpNormEssSup(g,μ)$$$
Lean4
/-- If `‖f x‖ₑ ≤ c * ‖g x‖ₑ` a.e., `eLpNorm' f p μ ≤ c * eLpNorm' g p μ` for all `p ∈ (0, ∞)`. -/
theorem eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul {f : α → ε} {c : ℝ≥0∞} {g : α → ε'} {p : ℝ}
(hg : AEStronglyMeasurable g μ) (h : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ) (hp : 0 < p) :
eLpNorm' f p μ ≤ c * eLpNorm' g p μ :=
by
have hp' : ¬(p < 0) := by linarith
by_cases hc : c = ⊤
· by_cases hg' : eLpNorm' g p μ = 0
· have : ∀ᵐ (x : α) ∂μ, ‖g x‖ₑ = 0 :=
by
simp [eLpNorm'_eq_lintegral_enorm, hp', hp] at hg'
rw [MeasureTheory.lintegral_eq_zero_iff' (by fun_prop)] at hg'
exact hg'.mono fun x hx ↦ by simpa [hp, hp'] using hx
have : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0 := (this.and h).mono fun x ⟨h, h'⟩ ↦ by simp_all
simpa only [hg', mul_zero, nonpos_iff_eq_zero] using eLpNorm'_eq_zero_of_ae_eq_zero hp this
· simp_all
have : c ^ p ≠ ⊤ := by simp [hp.le, hc]
simp_rw [eLpNorm'_eq_lintegral_enorm]
rw [← ENNReal.rpow_le_rpow_iff hp, ENNReal.mul_rpow_of_nonneg _ _ hp.le]
simp_rw [← ENNReal.rpow_mul, one_div, inv_mul_cancel₀ hp.ne', ENNReal.rpow_one, ← lintegral_const_mul' _ _ this]
apply lintegral_mono_ae
have aux (x) : (↑c) ^ p * ‖g x‖ₑ ^ p = (↑c * ‖g x‖ₑ) ^ p := by simp [ENNReal.mul_rpow_eq_ite, hp']
simpa [ENNReal.coe_rpow_of_nonneg _ hp.le, aux, ENNReal.rpow_le_rpow_iff hp]
