Compare Lp seminorms for different values of p #
In this file we compare MeasureTheory.eLpNorm' and MeasureTheory.eLpNorm for different
exponents.
theorem
MeasureTheory.eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ε}
[TopologicalSpace ε]
[ContinuousENorm ε]
{p q : ℝ}
(hp0_lt : 0 < p)
(hpq : p ≤ q)
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm'_le_eLpNormEssSup_mul_rpow_measure_univ
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ε}
[TopologicalSpace ε]
[ContinuousENorm ε]
{q : ℝ}
(hq_pos : 0 < q)
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_rpow_measure_univ
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ε}
[TopologicalSpace ε]
[ContinuousENorm ε]
{p q : ENNReal}
(hpq : p ≤ q)
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm'_le_eLpNorm'_of_exponent_le
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
{f : α → ε}
[TopologicalSpace ε]
[ContinuousENorm ε]
{p q : ℝ}
(hp0_lt : 0 < p)
(hpq : p ≤ q)
(μ : Measure α)
[IsProbabilityMeasure μ]
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm'_le_eLpNormEssSup
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ε}
[TopologicalSpace ε]
[ContinuousENorm ε]
{q : ℝ}
(hq_pos : 0 < q)
[IsProbabilityMeasure μ]
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_of_exponent_le
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ε}
[TopologicalSpace ε]
[ContinuousENorm ε]
{p q : ENNReal}
(hpq : p ≤ q)
[IsProbabilityMeasure μ]
(hf : AEStronglyMeasurable f μ)
:
theorem
MeasureTheory.eLpNorm'_lt_top_of_eLpNorm'_lt_top_of_exponent_le
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ε}
[TopologicalSpace ε]
[ContinuousENorm ε]
{p q : ℝ}
[IsFiniteMeasure μ]
(hf : AEStronglyMeasurable f μ)
(hfq_lt_top : eLpNorm' f q μ < ⊤)
(hp_nonneg : 0 ≤ p)
(hpq : p ≤ q)
:
theorem
MeasureTheory.MemLp.mono_exponent
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ε}
[TopologicalSpace ε]
[ContinuousENorm ε]
{p q : ENNReal}
[IsFiniteMeasure μ]
(hfq : MemLp f q μ)
(hpq : p ≤ q)
:
MemLp f p μ
theorem
MeasureTheory.MemLp.mono_exponent_of_measure_support_ne_top
{α : Type u_1}
{ε' : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[TopologicalSpace ε']
[ESeminormedAddMonoid ε']
{p q : ENNReal}
{f : α → ε'}
(hfq : MemLp f q μ)
{s : Set α}
(hf : ∀ x ∉ s, f x = 0)
(hs : μ s ≠ ⊤)
(hpq : p ≤ q)
:
MemLp f p μ
If a function is supported on a finite-measure set and belongs to ℒ^p, then it belongs to
ℒ^q for any q ≤ p.
theorem
MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : Measure α}
(p : ENNReal)
(f : α → E)
{g : α → F}
(hg : AEStronglyMeasurable g μ)
(b : E → F → G)
(c : NNReal)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_top
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : Measure α}
(p : ENNReal)
{f : α → E}
(hf : AEStronglyMeasurable f μ)
(g : α → F)
(b : E → F → G)
(c : NNReal)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
:
theorem
MeasureTheory.eLpNorm'_le_eLpNorm'_mul_eLpNorm'
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : Measure α}
{f : α → E}
{g : α → F}
{p q r : ℝ}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(b : E → F → G)
(c : NNReal)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
(hro_lt : 0 < r)
(hrp : r < p)
(hpqr : 1 / r = 1 / p + 1 / q)
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : Measure α}
{f : α → E}
{g : α → F}
{p q r : ENNReal}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(b : E → F → G)
(c : NNReal)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
[hpqr : p.HolderTriple q r]
:
Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation
fun x => b (f x) (g x).
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm'_of_norm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : Measure α}
{f : α → E}
{g : α → F}
{p q r : ENNReal}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(b : E → F → G)
(c : NNReal)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ ≤ ↑c * ‖f x‖ * ‖g x‖)
[hpqr : p.HolderTriple q r]
:
Hölder's inequality, as an inequality on the ℒp seminorm of an elementwise operation
fun x => b (f x) (g x).
theorem
MeasureTheory.MemLp.of_bilin
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{μ : Measure α}
{p q r : ENNReal}
{f : α → E}
{g : α → F}
(b : E → F → G)
(c : NNReal)
(hf : MemLp f p μ)
(hg : MemLp g q μ)
(h : AEStronglyMeasurable (fun (x : α) => b (f x) (g x)) μ)
(hb : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
[hpqr : p.HolderTriple q r]
:
MemLp (fun (x : α) => b (f x) (g x)) r μ
theorem
MeasureTheory.eLpNorm_smul_le_eLpNorm_top_mul_eLpNorm
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[IsBoundedSMul 𝕜 E]
{f : α → E}
(p : ENNReal)
(hf : AEStronglyMeasurable f μ)
(φ : α → 𝕜)
:
theorem
MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[IsBoundedSMul 𝕜 E]
(p : ENNReal)
(f : α → E)
{φ : α → 𝕜}
(hφ : AEStronglyMeasurable φ μ)
:
theorem
MeasureTheory.eLpNorm'_smul_le_mul_eLpNorm'
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[IsBoundedSMul 𝕜 E]
{p q r : ℝ}
{f : α → E}
(hf : AEStronglyMeasurable f μ)
{φ : α → 𝕜}
(hφ : AEStronglyMeasurable φ μ)
(hp0_lt : 0 < p)
(hpq : p < q)
(hpqr : 1 / p = 1 / q + 1 / r)
:
theorem
MeasureTheory.eLpNorm_smul_le_mul_eLpNorm
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[IsBoundedSMul 𝕜 E]
{p q r : ENNReal}
{f : α → E}
(hf : AEStronglyMeasurable f μ)
{φ : α → 𝕜}
(hφ : AEStronglyMeasurable φ μ)
[hpqr : p.HolderTriple q r]
:
Hölder's inequality, as an inequality on the ℒp seminorm of a scalar product φ • f.
theorem
MeasureTheory.MemLp.smul
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[IsBoundedSMul 𝕜 E]
{p q r : ENNReal}
{f : α → E}
{φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
theorem
MeasureTheory.MemLp.mul
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
theorem
MeasureTheory.MemLp.mul'
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hf : MemLp f q μ)
(hφ : MemLp φ p μ)
[hpqr : p.HolderTriple q r]
:
Variant of MemLp.mul where the function is written as fun x ↦ φ x * f x
instead of φ * f.
theorem
MeasureTheory.MemLp.prod
{ι : Type u_1}
{α : Type u_2}
{𝕜 : Type u_3}
{x✝ : MeasurableSpace α}
[NormedCommRing 𝕜]
{μ : Measure α}
{f : ι → α → 𝕜}
{p : ι → ENNReal}
{s : Finset ι}
(hf : ∀ i ∈ s, MemLp (f i) (p i) μ)
:
See MemLp.prod' for the applied version.
theorem
MeasureTheory.MemLp.prod'
{ι : Type u_1}
{α : Type u_2}
{𝕜 : Type u_3}
{x✝ : MeasurableSpace α}
[NormedCommRing 𝕜]
{μ : Measure α}
{f : ι → α → 𝕜}
{p : ι → ENNReal}
{s : Finset ι}
(hf : ∀ i ∈ s, MemLp (f i) (p i) μ)
:
See MemLp.prod for the unapplied version.