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.eLpNorm'_add_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {q : ℝ} {μ : Measure α} {f g : α → E} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (hq1 : 1 ≤ q) : eLpNorm' (f + g) q μ ≤ eLpNorm' f q μ + eLpNorm' g q μ

theorem MeasureTheory.eLpNorm'_add_le_of_le_one {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {q : ℝ} {μ : Measure α} {f g : α → E} (hf : AEStronglyMeasurable f μ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) : eLpNorm' (f + g) q μ ≤ 2 ^ (1 / q - 1) * (eLpNorm' f q μ + eLpNorm' g q μ)

theorem MeasureTheory.eLpNormEssSup_add_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {μ : Measure α} {f g : α → E} : eLpNormEssSup (f + g) μ ≤ eLpNormEssSup f μ + eLpNormEssSup g μ

theorem MeasureTheory.eLpNorm_add_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} {f g : α → E} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (hp1 : 1 ≤ p) : eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

noncomputable def MeasureTheory.LpAddConst (p : ENNReal) : 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

• MeasureTheory.LpAddConst p = if p ∈ Set.Ioo 0 1 then 2 ^ (1 / p.toReal - 1) else 1

theorem MeasureTheory.LpAddConst_of_one_le {p : ENNReal} (hp : 1 ≤ p) : LpAddConst p = 1

theorem MeasureTheory.LpAddConst_zero : LpAddConst 0 = 1

theorem MeasureTheory.LpAddConst_lt_top (p : ENNReal) : LpAddConst p < ⊤

theorem MeasureTheory.eLpNorm_add_le' {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {μ : Measure α} {f g : α → E} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (p : ENNReal) : eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)

theorem MeasureTheory.exists_Lp_half {α : Type u_1} (E : Type u_2) {m : MeasurableSpace α} [NormedAddCommGroup E] (μ : Measure α) (p : ENNReal) {δ : ENNReal} (hδ : δ ≠ 0) : ∃ (η : ENNReal), 0 < η ∧ ∀ (f g : α → E), AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → eLpNorm f p μ ≤ η → eLpNorm g p μ ≤ η → eLpNorm (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.eLpNorm_sub_le' {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {μ : Measure α} {f g : α → E} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (p : ENNReal) : eLpNorm (f - g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)

theorem MeasureTheory.eLpNorm_sub_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} {f g : α → E} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (hp : 1 ≤ p) : eLpNorm (f - g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ

theorem MeasureTheory.eLpNorm_add_lt_top {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : eLpNorm (f + g) p μ < ⊤

theorem MeasureTheory.eLpNorm'_sum_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {q : ℝ} {μ : Measure α} {ι : Type u_3} {f : ι → α → E} {s : Finset ι} (hfs : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) (hq1 : 1 ≤ q) : eLpNorm' (∑ i ∈ s, f i) q μ ≤ ∑ i ∈ s, eLpNorm' (f i) q μ

theorem MeasureTheory.eLpNorm_sum_le {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} {ι : Type u_3} {f : ι → α → E} {s : Finset ι} (hfs : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) (hp1 : 1 ≤ p) : eLpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, eLpNorm (f i) p μ

theorem MeasureTheory.MemLp.add {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : MemLp (f + g) p μ

theorem MeasureTheory.MemLp.sub {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} {f g : α → E} (hf : MemLp f p μ) (hg : MemLp g p μ) : MemLp (f - g) p μ

theorem MeasureTheory.memLp_finset_sum {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} {ι : Type u_3} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, MemLp (f i) p μ) : MemLp (fun (a : α) => ∑ i ∈ s, f i a) p μ

theorem MeasureTheory.memLp_finset_sum' {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [NormedAddCommGroup E] {p : ENNReal} {μ : Measure α} {ι : Type u_3} (s : Finset ι) {f : ι → α → E} (hf : ∀ i ∈ s, MemLp (f i) p μ) : MemLp (∑ i ∈ s, f i) p μ