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 α}
[TopologicalSpace E]
[ENormedAddCommMonoid E]
[TopologicalSpace F]
[ENormedAddCommMonoid F]
[TopologicalSpace G]
[ENormedAddCommMonoid 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 α}
[TopologicalSpace E]
[ENormedAddCommMonoid E]
[TopologicalSpace F]
[ENormedAddCommMonoid F]
[TopologicalSpace G]
[ENormedAddCommMonoid 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 α}
[TopologicalSpace E]
[ENormedAddCommMonoid E]
[TopologicalSpace F]
[ENormedAddCommMonoid F]
[TopologicalSpace G]
[ENormedAddCommMonoid 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_enorm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[TopologicalSpace E]
[ENormedAddCommMonoid E]
[TopologicalSpace F]
[ENormedAddCommMonoid F]
[TopologicalSpace G]
[ENormedAddCommMonoid 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_enorm'
{α : Type u_1}
{m : 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'_of_enorm
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
[TopologicalSpace E]
[ENormedAddCommMonoid E]
[TopologicalSpace F]
[ENormedAddCommMonoid F]
[TopologicalSpace G]
[ENormedAddCommMonoid 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 α}
[TopologicalSpace E]
[ENormedAddCommMonoid E]
[TopologicalSpace F]
[ENormedAddCommMonoid F]
[TopologicalSpace G]
[ENormedAddCommMonoid 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 μ