Transport of an Lp norm estimate to its actual functions #
Finite Lp representatives retain their literal extended-valued seminorms. Consequently a real norm estimate between the representatives gives the same numerical estimate on the original functions, for any exponent.
theorem
CKN.Core.Endgame.eLpNorm_le_of_toLp_norm_le
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
[MeasurableSpace α]
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure α}
{p : ENNReal}
{f : α → E}
{g : α → F}
(hf : MeasureTheory.MemLp f p μ)
(hg : MeasureTheory.MemLp g p μ)
{C : ℝ}
(hC : 0 ≤ C)
(hbound : ‖MeasureTheory.MemLp.toLp g hg‖ ≤ C * ‖MeasureTheory.MemLp.toLp f hf‖)
:
A norm estimate for two actual MemLp representatives gives the same
extended-valued seminorm estimate for the original functions.