Norm inequalities in Lᵖ spaces #
This file contains norm estimates for Lᵖ functions derived from almost-everywhere pointwise
bounds.
Main declarations #
TauCeti.Lp.norm_le_add_of_ae_norm_le: anLᵖnorm bound from pointwise domination by a two-term linear combination.MeasureTheory.Lp.integral_norm_sq_eq_norm_sq: the integral of the squared pointwise norm of anL²function is its squaredL²norm.
theorem
TauCeti.Lp.norm_le_add_of_ae_norm_le
{alpha : Type u_1}
{F : Type u_2}
{G : Type u_3}
{H : Type u_4}
[MeasurableSpace alpha]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
[NormedAddCommGroup H]
{m : MeasureTheory.Measure alpha}
{q : ENNReal}
[Fact (1 ≤ q)]
{f : ↥(MeasureTheory.Lp F q m)}
{g : ↥(MeasureTheory.Lp G q m)}
{h : ↥(MeasureTheory.Lp H q m)}
{a b : ℝ}
(ha : 0 ≤ a)
(hb : 0 ≤ b)
(hle : ∀ᵐ (z : alpha) ∂m, ‖↑↑f z‖ ≤ a * ‖↑↑g z‖ + b * ‖↑↑h z‖)
:
The norm of an Lᵖ function dominated pointwise by a two-term combination of two other
Lᵖ functions obeys the same bound in norm.
theorem
MeasureTheory.Lp.integral_norm_sq_eq_norm_sq
{alpha : Type u_1}
{F : Type u_2}
[MeasurableSpace alpha]
{m : Measure alpha}
[NormedAddCommGroup F]
(f : ↥(Lp F 2 m))
:
The integral of the squared pointwise norm of an L² function is its squared L² norm.