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} {ε : 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 μ

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 μ)

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 μ

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 μ

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 μ ≤ p.LpAddConst * (eLpNorm f p μ + eLpNorm g p μ)

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.

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 μ ≤ p.LpAddConst * (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} {ε : Type u_3} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p : ENNReal} {μ : Measure α} {f g : α → ε} (hf : MemLp f p μ) (hg : MemLp g p μ) : eLpNorm (f + g) p μ < ⊤

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 μ

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 μ

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 μ

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_finsetSum {α : 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 μ

@[deprecated MeasureTheory.memLp_finsetSum (since := "2026-04-08")]

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 μ

Alias of MeasureTheory.memLp_finsetSum.

theorem MeasureTheory.memLp_finsetSum' {α : 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 μ

@[deprecated MeasureTheory.memLp_finsetSum' (since := "2026-04-08")]

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 μ

Alias of MeasureTheory.memLp_finsetSum'.