# 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.

source
theorem MeasureTheory.eLpNorm'_add_le {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {q : ℝ} {μ : Measure α} {f g : α → ε} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (hq1 : 1 ≤ q) :
eLpNorm' (f + g) q μ ≤ eLpNorm' f q μ + eLpNorm' g q μ
source
theorem MeasureTheory.eLpNorm'_add_le_of_le_one {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {q : ℝ} {μ : Measure α} {f g : α → ε} (hf : AEStronglyMeasurable f μ) (hq0 : 0 ≤ q) (hq1 : q ≤ 1) :
eLpNorm' (f + g) q μ ≤ 2 ^ (1 / q - 1) * (eLpNorm' f q μ + eLpNorm' g q μ)
source
theorem MeasureTheory.eLpNormEssSup_add_le {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {μ : Measure α} {f g : α → ε} :
eLpNormEssSup (f + g) μ ≤ eLpNormEssSup f μ + eLpNormEssSup g μ
source
theorem MeasureTheory.eLpNorm_add_le {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p : ENNReal} {μ : Measure α} {f g : α → ε} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (hp1 : 1 ≤ p) :
eLpNorm (f + g) p μ ≤ eLpNorm f p μ + eLpNorm g p μ
source
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

Instances For

source
theorem MeasureTheory.LpAddConst_of_one_le {p : ENNReal} (hp : 1 ≤ p) :
LpAddConst p = 1
source
theorem MeasureTheory.LpAddConst_zero :
LpAddConst 0 = 1
source
theorem MeasureTheory.LpAddConst_lt_top (p : ENNReal) :
LpAddConst p < ⊤
source
theorem MeasureTheory.eLpNorm_add_le' {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {μ : Measure α} {f g : α → ε} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (p : ENNReal) :
eLpNorm (f + g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)
source
theorem MeasureTheory.exists_Lp_half {α : Type u_1} (ε : Type u_3) {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (μ : Measure α) (p : ENNReal) {δ : ENNReal} (hδ : δ ≠ 0) :
∃ (η : ENNReal), 0 < η ∧ ∀ (f g : α → ε), 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`.

source
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 μ)
source
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 μ
source
theorem MeasureTheory.eLpNorm_add_lt_top {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p : ENNReal} {μ : Measure α} {f g : α → ε} (hf : MemLp f p μ) (hg : MemLp g p μ) :
eLpNorm (f + g) p μ < ⊤
source
theorem MeasureTheory.eLpNorm'_sum_le {α : Type u_1} {ε' : Type u_4} {m : MeasurableSpace α} [TopologicalSpace ε'] [ESeminormedAddCommMonoid ε'] {q : ℝ} {μ : Measure α} [ContinuousAdd ε'] {ι : Type u_5} {f : ι → α → ε'} {s : Finset ι} (hfs : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) (hq1 : 1 ≤ q) :
eLpNorm' (∑ i ∈ s, f i) q μ ≤ ∑ i ∈ s, eLpNorm' (f i) q μ
source
theorem MeasureTheory.eLpNorm_sum_le {α : Type u_1} {ε' : Type u_4} {m : MeasurableSpace α} [TopologicalSpace ε'] [ESeminormedAddCommMonoid ε'] {p : ENNReal} {μ : Measure α} [ContinuousAdd ε'] {ι : Type u_5} {f : ι → α → ε'} {s : Finset ι} (hfs : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) (hp1 : 1 ≤ p) :
eLpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, eLpNorm (f i) p μ
source
theorem MeasureTheory.MemLp.add {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p : ENNReal} {μ : Measure α} {f g : α → ε} [ContinuousAdd ε] (hf : MemLp f p μ) (hg : MemLp g p μ) :
MemLp (f + g) p μ
source
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 μ
source
theorem MeasureTheory.memLp_finset_sum {α : Type u_1} {ε' : Type u_4} {m : MeasurableSpace α} [TopologicalSpace ε'] [ESeminormedAddCommMonoid ε'] {p : ENNReal} {μ : Measure α} [ContinuousAdd ε'] {ι : Type u_5} (s : Finset ι) {f : ι → α → ε'} (hf : ∀ i ∈ s, MemLp (f i) p μ) :
MemLp (fun (a : α) => ∑ i ∈ s, f i a) p μ
source
theorem MeasureTheory.memLp_finset_sum' {α : Type u_1} {ε' : Type u_4} {m : MeasurableSpace α} [TopologicalSpace ε'] [ESeminormedAddCommMonoid ε'] {p : ENNReal} {μ : Measure α} [ContinuousAdd ε'] {ι : Type u_5} (s : Finset ι) {f : ι → α → ε'} (hf : ∀ i ∈ s, MemLp (f i) p μ) :
MemLp (∑ i ∈ s, f i) p μ