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)
:
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)
:
theorem
MeasureTheory.eLpNormEssSup_add_le
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{μ : Measure α}
{f g : α → E}
:
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)
:
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]
{μ : Measure α}
{f g : α → E}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(p : ENNReal)
:
theorem
MeasureTheory.exists_Lp_half
{α : Type u_1}
(E : Type u_2)
{m : MeasurableSpace α}
[NormedAddCommGroup E]
(μ : Measure α)
(p : ENNReal)
{δ : ENNReal}
(hδ : δ ≠ 0)
:
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)
:
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)
:
theorem
MeasureTheory.eLpNorm_add_lt_top
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : Measure α}
{f g : α → E}
(hf : Memℒp f p μ)
(hg : Memℒp 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)
:
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)
:
theorem
MeasureTheory.Memℒp.add
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : Measure α}
{f g : α → E}
(hf : Memℒp f p μ)
(hg : Memℒp g p μ)
:
theorem
MeasureTheory.Memℒp.sub
{α : Type u_1}
{E : Type u_2}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
{p : ENNReal}
{μ : Measure α}
{f g : α → E}
(hf : Memℒp f p μ)
(hg : Memℒp g p μ)
:
theorem
MeasureTheory.memℒp_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, Memℒp (f i) p μ)
:
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}
{μ : Measure α}
{ι : Type u_3}
(s : Finset ι)
{f : ι → α → E}
(hf : ∀ i ∈ s, Memℒp (f i) p μ)
:
Memℒp (∑ i ∈ s, f i) p μ