Pointwise bounds for the real-valued Lᵖ norm #
A pointwise bound ‖f x‖ ≤ c ‖g x‖ almost everywhere bounds the real-valued Lᵖ norm:
lpNorm f p μ ≤ c * lpNorm g p μ (MeasureTheory.lpNorm_le_mul_lpNorm_of_ae_le_mul). This is
the lpNorm form of Mathlib's MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul. Since
lpNorm is 0 off Lᵖ, the hypothesis g ∈ Lᵖ(μ) is needed. It is the estimate for
multiplication by a bounded measurable coefficient, as for the lower-order terms of a
differential operator.
theorem
MeasureTheory.lpNorm_le_mul_lpNorm_of_ae_le_mul
{α : Type u_1}
{F : Type u_2}
{G : Type u_3}
{m : MeasurableSpace α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{p : ENNReal}
{μ : Measure α}
{f : α → F}
{g : α → G}
{c : ℝ}
(hf : AEStronglyMeasurable f μ)
(hg : MemLp g p μ)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
:
A pointwise bound bounds lpNorm. If g ∈ Lᵖ(μ) and ‖f x‖ ≤ c ‖g x‖ for almost every
x, then lpNorm f p μ ≤ c * lpNorm g p μ.