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)
:
MeasureTheory.snorm' (f + g) q μ ≤ MeasureTheory.snorm' f q μ + MeasureTheory.snorm' g 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.snormEssSup_add_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{g : α → E}
:
MeasureTheory.snormEssSup (f + g) μ ≤ MeasureTheory.snormEssSup f μ + MeasureTheory.snormEssSup g μ
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)
:
MeasureTheory.snorm (f + g) p μ ≤ MeasureTheory.snorm f p μ + MeasureTheory.snorm g p μ
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 / ENNReal.toReal p - 1) else 1
Instances For
theorem
MeasureTheory.snorm_add_le'
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : MeasureTheory.Measure α}
{f : α → E}
{g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(p : ENNReal)
:
MeasureTheory.snorm (f + g) p μ ≤ MeasureTheory.LpAddConst p * (MeasureTheory.snorm f p μ + MeasureTheory.snorm g p μ)
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]
{μ : MeasureTheory.Measure α}
{f : α → E}
{g : α → E}
(hf : MeasureTheory.AEStronglyMeasurable f μ)
(hg : MeasureTheory.AEStronglyMeasurable g μ)
(p : ENNReal)
:
MeasureTheory.snorm (f - g) p μ ≤ MeasureTheory.LpAddConst p * (MeasureTheory.snorm f p μ + MeasureTheory.snorm g p μ)
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)
:
MeasureTheory.snorm (f - g) p μ ≤ MeasureTheory.snorm f p μ + MeasureTheory.snorm g 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)
:
MeasureTheory.snorm (f + 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 : ∀ i ∈ s, 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 : ∀ i ∈ s, 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)
:
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 : α → E}
{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 : α) => 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 : ∀ i ∈ s, MeasureTheory.Memℒp (f i) p)
:
MeasureTheory.Memℒp (Finset.sum s fun (i : ι) => f i) p