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_mul_rpow_measure_univ_of_pos
{α : Type u_1}
{ε : Type u_2}
{m : MeasurableSpace α}
{μ : Measure α}
{f : α → ε}
[TopologicalSpace ε]
[ContinuousENorm ε]
{p q : ENNReal}
(hpq : p ≤ q)
(hp : 0 < p)
:
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 μ]
:
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.
In this section, we show that ‖fg‖_{L^r} ≤ ‖f‖_{L^p} ‖g‖_{L^q} when 1/r = 1/p + 1/q, in a more
general version involving a general bilinear form.
There is one edge case where this formula does not hold with our conventions: if r = p = 0, f
is measurable but fg is not, then ‖fg‖_{L^r} = ∞ while ‖f‖_{L^p} ‖g‖_{L^q} = 0 * ∞ = 0.
So, we should either assume that r is nonzero, or the functions are measurable. Most lemmas
are given in the two versions, with the main one assuming measurability, and the other version
(suffixed with of_pos) assume 0 < r.
The lemmas are given for a general function b of two variables, with an assumption that
‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊. We also formulate versions giving the assumption
in terms of enorms (including of_enorm in the name), or with norms (with of_norm in the name).
Versions with nnnorms have no modifier in the name.
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_enorm_of_not_aestronglyMeasurable
{α : Type u_1}
{ε : Type u_5}
{ε' : Type u_6}
{ε'' : Type u_7}
{m : MeasurableSpace α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
[TopologicalSpace ε']
[ENormedAddMonoid ε']
[TopologicalSpace ε'']
[ENormedAddMonoid ε'']
{μ : Measure α}
(p q r : ENNReal)
(b : ε → ε' → ε'')
(c : ENNReal)
{f : α → ε}
{g : α → ε'}
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ₑ ≤ c * ‖f x‖ₑ * ‖g x‖ₑ)
(hfg : ¬(AEStronglyMeasurable f μ ∧ AEStronglyMeasurable g μ))
(hp : p ≠ 0)
(hq : q ≠ 0)
:
@[deprecated MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_enorm_of_not_aestronglyMeasurable (since := "2026-09-16")]
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_not_aestronglyMeasurable_ennreal
{α : Type u_1}
{ε : Type u_5}
{ε' : Type u_6}
{ε'' : Type u_7}
{m : MeasurableSpace α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
[TopologicalSpace ε']
[ENormedAddMonoid ε']
[TopologicalSpace ε'']
[ENormedAddMonoid ε'']
{μ : Measure α}
(p q r : ENNReal)
(b : ε → ε' → ε'')
(c : ENNReal)
{f : α → ε}
{g : α → ε'}
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ₑ ≤ c * ‖f x‖ₑ * ‖g x‖ₑ)
(hfg : ¬(AEStronglyMeasurable f μ ∧ AEStronglyMeasurable g μ))
(hp : p ≠ 0)
(hq : q ≠ 0)
:
Alias of MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_enorm_of_not_aestronglyMeasurable.
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_not_aestronglyMeasurable
{α : 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)
(b : E → F → G)
(c : NNReal)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
(hfg : ¬(AEStronglyMeasurable f μ ∧ AEStronglyMeasurable g μ))
(hp : p ≠ 0)
(hq : q ≠ 0)
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm_of_enorm_of_pos
{α : Type u_1}
{ε : Type u_5}
{ε' : Type u_6}
{ε'' : Type u_7}
{m : MeasurableSpace α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
[TopologicalSpace ε']
[ENormedAddMonoid ε']
[TopologicalSpace ε'']
[ENormedAddMonoid ε'']
{μ : Measure α}
(p : ENNReal)
(b : ε → ε' → ε'')
(c : ENNReal)
{f : α → ε}
{g : α → ε'}
(hb : AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → AEStronglyMeasurable (fun (x : α) => b (f x) (g x)) μ)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ₑ ≤ c * ‖f x‖ₑ * ‖g x‖ₑ)
(hp : 0 < p)
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm_of_pos
{α : 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 : ENNReal)
(b : E → F → G)
(c : NNReal)
(hb : Continuous (Function.uncurry b))
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
(hp : 0 < p)
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_top_mul_eLpNorm_of_enorm
{α : Type u_1}
{ε : Type u_5}
{ε' : Type u_6}
{ε'' : Type u_7}
{m : MeasurableSpace α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
[TopologicalSpace ε']
[ENormedAddMonoid ε']
[TopologicalSpace ε'']
[ENormedAddMonoid ε'']
{μ : Measure α}
(p : ENNReal)
(b : ε → ε' → ε'')
(c : ENNReal)
{f : α → ε}
{g : α → ε'}
(hb : AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → AEStronglyMeasurable (fun (x : α) => b (f x) (g x)) μ)
(hf : AEStronglyMeasurable f μ)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ₑ ≤ c * ‖f x‖ₑ * ‖g x‖ₑ)
:
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 α}
{f : α → E}
{g : α → F}
(p : ENNReal)
(b : E → F → G)
(c : NNReal)
(hb : Continuous (Function.uncurry b))
(hf : AEStronglyMeasurable f μ)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_top_of_enorm_of_pos
{α : Type u_1}
{ε : Type u_5}
{ε' : Type u_6}
{ε'' : Type u_7}
{m : MeasurableSpace α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
[TopologicalSpace ε']
[ENormedAddMonoid ε']
[TopologicalSpace ε'']
[ENormedAddMonoid ε'']
{μ : Measure α}
(p : ENNReal)
(b : ε → ε' → ε'')
(c : ENNReal)
{f : α → ε}
{g : α → ε'}
(hb : AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → AEStronglyMeasurable (fun (x : α) => b (f x) (g x)) μ)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ₑ ≤ c * ‖f x‖ₑ * ‖g x‖ₑ)
(hp : 0 < p)
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_top_of_pos
{α : 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 : ENNReal)
(b : E → F → G)
(c : NNReal)
(hb : Continuous (Function.uncurry b))
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
(hp : 0 < p)
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_top_of_enorm
{α : Type u_1}
{ε : Type u_5}
{ε' : Type u_6}
{ε'' : Type u_7}
{m : MeasurableSpace α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
[TopologicalSpace ε']
[ENormedAddMonoid ε']
[TopologicalSpace ε'']
[ENormedAddMonoid ε'']
{μ : Measure α}
(p : ENNReal)
(b : ε → ε' → ε'')
(c : ENNReal)
{f : α → ε}
{g : α → ε'}
(hb : AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → AEStronglyMeasurable (fun (x : α) => b (f x) (g x)) μ)
(hg : AEStronglyMeasurable g μ)
(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 α}
{f : α → E}
{g : α → F}
(p : ENNReal)
(b : E → F → G)
(c : NNReal)
(hb : Continuous (Function.uncurry b))
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
:
theorem
MeasureTheory.eLpNorm'_le_eLpNorm'_mul_eLpNorm'_of_enorm
{α : Type u_1}
{ε : Type u_5}
{ε' : Type u_6}
{ε'' : Type u_7}
{m : MeasurableSpace α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
[TopologicalSpace ε']
[ENormedAddMonoid ε']
[TopologicalSpace ε'']
[ENormedAddMonoid ε'']
{μ : Measure α}
{p q r : ℝ}
(b : ε → ε' → ε'')
(c : ENNReal)
{f : α → ε}
{g : α → ε'}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ₑ ≤ c * ‖f x‖ₑ * ‖g x‖ₑ)
(hpqr : p.HolderTriple q r)
:
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 : ℝ}
(b : E → F → G)
(c : NNReal)
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
(hpqr : p.HolderTriple q r)
:
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_enorm
{α : Type u_1}
{ε : Type u_5}
{ε' : Type u_6}
{ε'' : Type u_7}
{m : MeasurableSpace α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
[TopologicalSpace ε']
[ENormedAddMonoid ε']
[TopologicalSpace ε'']
[ENormedAddMonoid ε'']
{μ : Measure α}
{p q r : ENNReal}
(b : ε → ε' → ε'')
(c : ENNReal)
{f : α → ε}
{g : α → ε'}
(hb : AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → AEStronglyMeasurable (fun (x : α) => b (f x) (g x)) μ)
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(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
{α : 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}
(b : E → F → G)
(c : NNReal)
(hb : Continuous (Function.uncurry b))
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
[hpqr : p.HolderTriple q r]
:
@[deprecated MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm (since := "2026-09-16")]
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}
(b : E → F → G)
(c : NNReal)
(hb : Continuous (Function.uncurry b))
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
[hpqr : p.HolderTriple q r]
:
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}
(b : E → F → G)
(c : NNReal)
(hb : Continuous (Function.uncurry b))
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(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).
@[deprecated MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_norm (since := "2026-09-11")]
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}
(b : E → F → G)
(c : NNReal)
(hb : Continuous (Function.uncurry b))
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ ≤ ↑c * ‖f x‖ * ‖g x‖)
[hpqr : p.HolderTriple q r]
:
Alias of MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_norm.
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_enorm_of_pos
{α : Type u_1}
{ε : Type u_5}
{ε' : Type u_6}
{ε'' : Type u_7}
{m : MeasurableSpace α}
[TopologicalSpace ε]
[ENormedAddMonoid ε]
[TopologicalSpace ε']
[ENormedAddMonoid ε']
[TopologicalSpace ε'']
[ENormedAddMonoid ε'']
{μ : Measure α}
{p q r : ENNReal}
(b : ε → ε' → ε'')
(c : ENNReal)
{f : α → ε}
{g : α → ε'}
(hb : AEStronglyMeasurable f μ → AEStronglyMeasurable g μ → AEStronglyMeasurable (fun (x : α) => b (f x) (g x)) μ)
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ₑ ≤ c * ‖f x‖ₑ * ‖g x‖ₑ)
(hr : 0 < r)
[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_pos
{α : 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}
(b : E → F → G)
(c : NNReal)
(hb : Continuous (Function.uncurry b))
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
(hr : 0 < r)
[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).
@[deprecated MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_pos (since := "2026-09-16")]
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm_of_pos
{α : 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}
(b : E → F → G)
(c : NNReal)
(hb : Continuous (Function.uncurry b))
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊)
(hr : 0 < r)
[hpqr : p.HolderTriple q r]
:
Alias of MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_pos.
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_of_pos
{α : 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}
(b : E → F → G)
(c : NNReal)
(hb : Continuous (Function.uncurry b))
(h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖ ≤ ↑c * ‖f x‖ * ‖g x‖)
(hr : 0 < r)
[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 μ)
(hb : Continuous (Function.uncurry b))
(h : ∀ᵐ (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_of_pos
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[IsBoundedSMul 𝕜 E]
{f : α → E}
{φ : α → 𝕜}
(p : ENNReal)
(hp : 0 < p)
:
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)
(hφ : AEStronglyMeasurable φ μ)
:
theorem
MeasureTheory.eLpNorm_smul_le_eLpNorm_mul_eLpNorm_top_of_pos
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[IsBoundedSMul 𝕜 E]
{f : α → E}
{φ : α → 𝕜}
(p : ENNReal)
(hp : 0 < p)
:
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]
{f : α → E}
{φ : α → 𝕜}
(p : ENNReal)
(hf : AEStronglyMeasurable f μ)
:
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]
{f : α → E}
{p q r : ℝ}
(hf : AEStronglyMeasurable f μ)
{φ : α → 𝕜}
(hφ : AEStronglyMeasurable φ μ)
(hpqr : q.HolderTriple r p)
:
theorem
MeasureTheory.eLpNorm_smul_le_mul_eLpNorm_of_pos
{𝕜 : Type u_1}
{α : Type u_2}
{E : Type u_3}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedRing 𝕜]
[NormedAddCommGroup E]
[MulActionWithZero 𝕜 E]
[IsBoundedSMul 𝕜 E]
{f : α → E}
{φ : α → 𝕜}
{p q r : ENNReal}
(hr : 0 < r)
[hpqr : p.HolderTriple q r]
:
Hölder's inequality, as an inequality on the ℒp seminorm of a scalar product φ • f.
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]
{f : α → E}
{φ : α → 𝕜}
{p q r : ENNReal}
(hφ : AEStronglyMeasurable φ μ)
(hf : AEStronglyMeasurable f μ)
[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}
{φ : α → 𝕜}
(hφ : MemLp φ p μ)
(hf : MemLp f q μ)
[hpqr : p.HolderTriple q r]
:
theorem
MeasureTheory.MemLp.mul
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hφ : MemLp φ p μ)
(hf : MemLp f q μ)
[hpqr : p.HolderTriple q r]
:
theorem
MeasureTheory.MemLp.fun_mul
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hφ : MemLp φ p μ)
(hf : MemLp f q μ)
[hpqr : p.HolderTriple q r]
:
Eta-expanded form of MeasureTheory.MemLp.mul
@[deprecated MeasureTheory.MemLp.fun_mul (since := "2026-09-06")]
theorem
MeasureTheory.MemLp.mul'
{α : Type u_1}
{x✝ : MeasurableSpace α}
{𝕜 : Type u_2}
[NormedRing 𝕜]
{μ : Measure α}
{p q r : ENNReal}
{f φ : α → 𝕜}
(hφ : MemLp φ p μ)
(hf : MemLp f q μ)
[hpqr : p.HolderTriple q r]
:
Alias of MeasureTheory.MemLp.fun_mul.
Eta-expanded form of MeasureTheory.MemLp.mul
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_ennreal
{α : Type u_1}
{x✝ : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
{f g : α → ENNReal}
(hf : AEStronglyMeasurable f μ)
(hg : AEStronglyMeasurable g μ)
[hpqr : p.HolderTriple q r]
:
Hölder's inequality, as an inequality on the ℒp seminorm for functions to ℝ≥0∞.
theorem
MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_ennreal_of_pos
{α : Type u_1}
{x✝ : MeasurableSpace α}
{μ : Measure α}
{p q r : ENNReal}
{f g : α → ENNReal}
(hr : 0 < r)
[hpqr : p.HolderTriple q r]
:
Hölder's inequality, as an inequality on the ℒp seminorm for functions to ℝ≥0∞.
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.fun_prod for the applied version.
theorem
MeasureTheory.MemLp.fun_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.
@[deprecated MeasureTheory.MemLp.fun_prod (since := "2026-09-06")]
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) μ)
:
Alias of MeasureTheory.MemLp.fun_prod.
See MemLp.prod for the unapplied version.