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 : ℝ}
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(hq1 : 1 ≤ q)
:
MeasureTheory.eLpNorm' (f + g) q μ ≤ MeasureTheory.eLpNorm' f q μ + MeasureTheory.eLpNorm' g q μ
@[deprecated MeasureTheory.eLpNorm'_add_le (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_add_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{q : ℝ}
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(hq1 : 1 ≤ q)
:
MeasureTheory.eLpNorm' (f + g) q μ ≤ MeasureTheory.eLpNorm' f q μ + MeasureTheory.eLpNorm' g q μ
Alias of MeasureTheory.eLpNorm'_add_le.
theorem
MeasureTheory.eLpNorm'_add_le_of_le_one
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{q : ℝ}
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hq0 : 0 ≤ q)
(hq1 : q ≤ 1)
:
MeasureTheory.eLpNorm' (f + g) q μ ≤ 2 ^ (1 / q - 1) * (MeasureTheory.eLpNorm' f q μ + MeasureTheory.eLpNorm' g q μ)
@[deprecated MeasureTheory.eLpNorm'_add_le_of_le_one (since := "2024-07-27")]
theorem
MeasureTheory.snorm'_add_le_of_le_one
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{q : ℝ}
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hq0 : 0 ≤ q)
(hq1 : q ≤ 1)
:
MeasureTheory.eLpNorm' (f + g) q μ ≤ 2 ^ (1 / q - 1) * (MeasureTheory.eLpNorm' f q μ + MeasureTheory.eLpNorm' g q μ)
Alias of MeasureTheory.eLpNorm'_add_le_of_le_one.
theorem
MeasureTheory.eLpNormEssSup_add_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f g : α → E}
:
MeasureTheory.eLpNormEssSup (f + g) μ ≤ MeasureTheory.eLpNormEssSup f μ + MeasureTheory.eLpNormEssSup g μ
@[deprecated MeasureTheory.eLpNormEssSup_add_le (since := "2024-07-27")]
theorem
MeasureTheory.snormEssSup_add_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f g : α → E}
:
MeasureTheory.eLpNormEssSup (f + g) μ ≤ MeasureTheory.eLpNormEssSup f μ + MeasureTheory.eLpNormEssSup g μ
Alias of MeasureTheory.eLpNormEssSup_add_le.
theorem
MeasureTheory.eLpNorm_add_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(hp1 : 1 ≤ p)
:
MeasureTheory.eLpNorm (f + g) p μ ≤ MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_add_le (since := "2024-07-27")]
theorem
MeasureTheory.snorm_add_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(hp1 : 1 ≤ p)
:
MeasureTheory.eLpNorm (f + g) p μ ≤ MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ
Alias of MeasureTheory.eLpNorm_add_le.
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).
Instances For
theorem
MeasureTheory.eLpNorm_add_le'
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(p : ENNReal)
:
MeasureTheory.eLpNorm (f + g) p μ ≤ MeasureTheory.LpAddConst p * (MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ)
@[deprecated MeasureTheory.eLpNorm_add_le' (since := "2024-07-27")]
theorem
MeasureTheory.snorm_add_le'
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(p : ENNReal)
:
MeasureTheory.eLpNorm (f + g) p μ ≤ MeasureTheory.LpAddConst p * (MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ)
Alias of MeasureTheory.eLpNorm_add_le'.
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.eLpNorm f p μ ≤ η → MeasureTheory.eLpNorm g p μ ≤ η → MeasureTheory.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]
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(p : ENNReal)
:
MeasureTheory.eLpNorm (f - g) p μ ≤ MeasureTheory.LpAddConst p * (MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ)
@[deprecated MeasureTheory.eLpNorm_sub_le' (since := "2024-07-27")]
theorem
MeasureTheory.snorm_sub_le'
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(p : ENNReal)
:
MeasureTheory.eLpNorm (f - g) p μ ≤ MeasureTheory.LpAddConst p * (MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ)
Alias of MeasureTheory.eLpNorm_sub_le'.
theorem
MeasureTheory.eLpNorm_sub_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(hp : 1 ≤ p)
:
MeasureTheory.eLpNorm (f - g) p μ ≤ MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ
@[deprecated MeasureTheory.eLpNorm_sub_le (since := "2024-07-27")]
theorem
MeasureTheory.snorm_sub_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(hp : 1 ≤ p)
:
MeasureTheory.eLpNorm (f - g) p μ ≤ MeasureTheory.eLpNorm f p μ + MeasureTheory.eLpNorm g p μ
Alias of MeasureTheory.eLpNorm_sub_le.
theorem
MeasureTheory.eLpNorm_add_lt_top
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.eLpNorm (f + g) p μ < ⊤
@[deprecated MeasureTheory.eLpNorm_add_lt_top (since := "2024-07-27")]
theorem
MeasureTheory.snorm_add_lt_top
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.eLpNorm (f + g) p μ < ⊤
Alias of MeasureTheory.eLpNorm_add_lt_top.
theorem
MeasureTheory.eLpNorm'_sum_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{q : ℝ}
{μ : MeasureTheory.Measure α}
{ι : Type u_3}
{f : ι → α → E}
{s : Finset ι}
(hfs : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ)
(hq1 : 1 ≤ q)
:
MeasureTheory.eLpNorm' (∑ i ∈ s, f i) q μ ≤ ∑ i ∈ s, MeasureTheory.eLpNorm' (f i) q μ
@[deprecated MeasureTheory.eLpNorm'_sum_le (since := "2024-07-27")]
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 : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ)
(hq1 : 1 ≤ q)
:
MeasureTheory.eLpNorm' (∑ i ∈ s, f i) q μ ≤ ∑ i ∈ s, MeasureTheory.eLpNorm' (f i) q μ
Alias of MeasureTheory.eLpNorm'_sum_le.
theorem
MeasureTheory.eLpNorm_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 : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ)
(hp1 : 1 ≤ p)
:
MeasureTheory.eLpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, MeasureTheory.eLpNorm (f i) p μ
@[deprecated MeasureTheory.eLpNorm_sum_le (since := "2024-07-27")]
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 : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ)
(hp1 : 1 ≤ p)
:
MeasureTheory.eLpNorm (∑ i ∈ s, f i) p μ ≤ ∑ i ∈ s, MeasureTheory.eLpNorm (f i) p μ
Alias of MeasureTheory.eLpNorm_sum_le.
theorem
MeasureTheory.Memℒp.add
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.Memℒp (f + g) p μ
theorem
MeasureTheory.Memℒp.sub
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : MeasureTheory.Measure α}
{f g : α → E}
(hf : MeasureTheory.Memℒp f p μ)
(hg : MeasureTheory.Memℒp g p μ)
:
MeasureTheory.Memℒp (f - 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 : ∀ i ∈ s, MeasureTheory.Memℒp (f i) p μ)
:
MeasureTheory.Memℒp (fun (a : α) => ∑ i ∈ s, 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 : ∀ i ∈ s, MeasureTheory.Memℒp (f i) p μ)
:
MeasureTheory.Memℒp (∑ i ∈ s, f i) p μ