English
Assume μ is finite. If ∥f x∥₊ ≤ C a.e., then ∥f∥₊ ≤ μ(univ)^{1/p} · C.
Русский
Пусть μ конечна. Если ∥f x∥₊ ≤ C почти всюду, то ∥f∥₊ ≤ μ(univ)^{1/p} · C.
LaTeX
$$$[IsFiniteMeasure μ] \Rightarrow (f: Lp E p μ) (C: NNReal) (hfC: ∀^{\mathrm{ae}} x, \|f(x)\|_+ ≤ C) \Rightarrow \|f\|_+ ≤ (measureUnivNNReal μ)^{p.toReal^{-1}} · C$$$
Lean4
theorem nnnorm_le_of_ae_bound [IsFiniteMeasure μ] {f : Lp E p μ} {C : ℝ≥0} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) :
‖f‖₊ ≤ measureUnivNNReal μ ^ p.toReal⁻¹ * C :=
by
by_cases hμ : μ = 0
· by_cases hp : p.toReal⁻¹ = 0
· simp [hp, hμ, nnnorm_def]
· simp [hμ, nnnorm_def]
rw [← ENNReal.coe_le_coe, nnnorm_def, ENNReal.coe_toNNReal (eLpNorm_ne_top _)]
refine (eLpNorm_le_of_ae_nnnorm_bound hfC).trans_eq ?_
rw [← coe_measureUnivNNReal μ, ← ENNReal.coe_rpow_of_ne_zero (measureUnivNNReal_pos hμ).ne', ENNReal.coe_mul,
mul_comm, ENNReal.smul_def, smul_eq_mul]
