Documentation

Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality

Triangle inequality for Lp-seminorm #

In this file we prove several versions of the triangle inequality for the Lp seminorm, as well as simple corollaries.

theorem MeasureTheory.snorm'_add_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {q : } {μ : MeasureTheory.Measure α} {f : αE} {g : αE} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (hq1 : 1 q) :
theorem MeasureTheory.snorm'_add_le_of_le_one {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {q : } {μ : MeasureTheory.Measure α} {f : αE} {g : αE} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hq0 : 0 q) (hq1 : q 1) :
MeasureTheory.snorm' (f + g) q μ 2 ^ (1 / q - 1) * (MeasureTheory.snorm' f q μ + MeasureTheory.snorm' g q μ)
theorem MeasureTheory.snorm_add_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} {f : αE} {g : αE} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (hp1 : 1 p) :
noncomputable def MeasureTheory.LpAddConst (p : ENNReal) :

A constant for the inequality ‖f + g‖_{L^p} ≤ C * (‖f‖_{L^p} + ‖g‖_{L^p}). It is equal to 1 for p ≥ 1 or p = 0, and 2^(1/p-1) in the more tricky interval (0, 1).

Equations
Instances For
    theorem MeasureTheory.exists_Lp_half {α : Type u_1} (E : Type u_2) {m : MeasurableSpace α} [NormedAddCommGroup E] (μ : MeasureTheory.Measure α) (p : ENNReal) {δ : ENNReal} (hδ : δ 0) :
    ∃ (η : ENNReal), 0 < η ∀ (f g : αE), MeasureTheory.AEStronglyMeasurable f μMeasureTheory.AEStronglyMeasurable g μMeasureTheory.snorm f p μ ηMeasureTheory.snorm g p μ ηMeasureTheory.snorm (f + g) p μ < δ

    Technical lemma to control the addition of functions in L^p even for p < 1: Given δ > 0, there exists η such that two functions bounded by η in L^p have a sum bounded by δ. One could take η = δ / 2 for p ≥ 1, but the point of the lemma is that it works also for p < 1.

    theorem MeasureTheory.snorm_sub_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} {f : αE} {g : αE} (hf : MeasureTheory.AEStronglyMeasurable f μ) (hg : MeasureTheory.AEStronglyMeasurable g μ) (hp : 1 p) :
    theorem MeasureTheory.snorm_add_lt_top {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} {f : αE} {g : αE} (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ) :
    theorem MeasureTheory.snorm'_sum_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {q : } {μ : MeasureTheory.Measure α} {ι : Type u_3} {f : ιαE} {s : Finset ι} (hfs : is, MeasureTheory.AEStronglyMeasurable (f i) μ) (hq1 : 1 q) :
    MeasureTheory.snorm' (Finset.sum s fun (i : ι) => f i) q μ Finset.sum s fun (i : ι) => MeasureTheory.snorm' (f i) q μ
    theorem MeasureTheory.snorm_sum_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} {ι : Type u_3} {f : ιαE} {s : Finset ι} (hfs : is, MeasureTheory.AEStronglyMeasurable (f i) μ) (hp1 : 1 p) :
    MeasureTheory.snorm (Finset.sum s fun (i : ι) => f i) p μ Finset.sum s fun (i : ι) => MeasureTheory.snorm (f i) p μ
    theorem MeasureTheory.Memℒp.add {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} {f : αE} {g : αE} (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ) :
    theorem MeasureTheory.Memℒp.sub {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} {f : αE} {g : αE} (hf : MeasureTheory.Memℒp f p μ) (hg : MeasureTheory.Memℒp g p μ) :
    theorem MeasureTheory.memℒp_finset_sum {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} {ι : Type u_3} (s : Finset ι) {f : ιαE} (hf : is, MeasureTheory.Memℒp (f i) p μ) :
    MeasureTheory.Memℒp (fun (a : α) => Finset.sum s fun (i : ι) => f i a) p μ
    theorem MeasureTheory.memℒp_finset_sum' {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : MeasureTheory.Measure α} {ι : Type u_3} (s : Finset ι) {f : ιαE} (hf : is, MeasureTheory.Memℒp (f i) p μ) :
    MeasureTheory.Memℒp (Finset.sum s fun (i : ι) => f i) p μ