The deviation of an Lᵖ function from a constant #
On a finite measure space the Lᵖ seminorm of fun x => f x - a, for a constant a, is the
Lᵖ distance from f to the constant class MeasureTheory.Lp.const. The identity is the
bridge between the seminorm form of an estimate on the deviation from a constant and its norm
form, in which both sides are continuous functions of the Lᵖ class and so pass to limits.
Main declaration #
TauCeti.eLpNorm_sub_const_eq_enorm: the deviation from a constant as a distance inLᵖ.
theorem
TauCeti.eLpNorm_sub_const_eq_enorm
{α : Type u_1}
{F : Type u_2}
[MeasurableSpace α]
[NormedAddCommGroup F]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsFiniteMeasure μ]
{p : ENNReal}
[Fact (1 ≤ p)]
(a : F)
(f : ↥(MeasureTheory.Lp F p μ))
:
The deviation from a constant, as a distance in Lᵖ. The Lᵖ seminorm of
fun x => f x - a is the distance from f to the constant class a.