Monotonicity and ℒp seminorms #
theorem
MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
{p : ℝ}
(hp : 0 < p)
:
theorem
MeasureTheory.eLpNorm'_le_nnreal_smul_eLpNorm'_of_ae_le_mul'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_5}
{ε' : Type u_6}
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ)
{p : ℝ}
(hp : 0 < p)
:
theorem
MeasureTheory.eLpNorm'_le_mul_eLpNorm'_of_ae_le_mul
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε' : Type u_6}
[TopologicalSpace ε']
[ContinuousENorm ε']
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
{c : ENNReal}
{g : α → ε'}
{p : ℝ}
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ)
(hp : 0 < p)
:
If ‖f x‖ₑ ≤ c * ‖g x‖ₑ a.e., eLpNorm' f p μ ≤ c * eLpNorm' g p μ for all p ∈ (0, ∞).
theorem
MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_5}
{ε' : Type u_6}
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
{c : ENNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ)
:
theorem
MeasureTheory.eLpNormEssSup_le_nnreal_smul_eLpNormEssSup_of_ae_le_mul
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
:
theorem
MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_5}
{ε' : Type u_6}
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ)
(p : ENNReal)
:
theorem
MeasureTheory.eLpNorm_le_nnreal_smul_eLpNorm_of_ae_le_mul
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
(p : ENNReal)
:
theorem
MeasureTheory.eLpNorm_eq_zero_and_zero_of_ae_le_mul_neg
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
(hc : c < 0)
(p : ENNReal)
:
When c is negative, ‖f x‖ ≤ c * ‖g x‖ is nonsense and forces both f and g to have an
eLpNorm of 0.
theorem
MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul
{α : Type u_1}
{F : Type u_3}
{G : Type u_4}
{m : MeasurableSpace α}
{μ : Measure α}
[NormedAddCommGroup F]
[NormedAddCommGroup G]
{f : α → F}
{g : α → G}
{c : ℝ}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
(p : ENNReal)
:
theorem
MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul'
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε : Type u_5}
{ε' : Type u_6}
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
{c : NNReal}
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ)
(p : ENNReal)
:
If ‖f x‖ₑ ≤ c * ‖g x‖ₑ, then eLpNorm f p μ ≤ c * eLpNorm g p μ.
This version assumes c is finite, but requires no measurability hypothesis on g.
theorem
MeasureTheory.eLpNorm_le_mul_eLpNorm_of_ae_le_mul''
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{ε' : Type u_6}
[TopologicalSpace ε']
[ContinuousENorm ε']
{ε : Type u_7}
[TopologicalSpace ε]
[ESeminormedAddMonoid ε]
{f : α → ε}
{c : ENNReal}
{g : α → ε'}
(p : ENNReal)
(hg : AEStronglyMeasurable g μ)
(h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ)
:
If ‖f x‖ₑ ≤ c * ‖g x‖ₑ, then eLpNorm f p μ ≤ c * eLpNorm g p μ.
This version allows c = ∞, but requires g to be a.e. strongly measurable.
theorem
MeasureTheory.MemLp.of_nnnorm_le_mul
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
{c : NNReal}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊)
:
MemLp f p μ
theorem
MeasureTheory.MemLp.of_enorm_le_mul
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_5}
{ε' : Type u_6}
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
{c : NNReal}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ)
:
MemLp f p μ
theorem
MeasureTheory.MemLp.of_le_mul
{α : Type u_1}
{E : Type u_2}
{F : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup E]
[NormedAddCommGroup F]
{f : α → E}
{g : α → F}
{c : ℝ}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖)
:
MemLp f p μ
theorem
MeasureTheory.MemLp.of_le_mul'
{α : Type u_1}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
{ε : Type u_5}
{ε' : Type u_6}
[TopologicalSpace ε]
[ContinuousENorm ε]
[TopologicalSpace ε']
[ContinuousENorm ε']
{f : α → ε}
{g : α → ε'}
{c : NNReal}
(hg : MemLp g p μ)
(hf : AEStronglyMeasurable f μ)
(hfg : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ)
:
MemLp f p μ
theorem
MeasureTheory.le_eLpNorm_of_bddBelow
{α : Type u_1}
{F : Type u_3}
{m : MeasurableSpace α}
{p : ENNReal}
{μ : Measure α}
[NormedAddCommGroup F]
(hp : p ≠ 0)
(hp' : p ≠ ⊤)
{f : α → F}
(C : NNReal)
{s : Set α}
(hs : MeasurableSet s)
(hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊)
:
@[simp]
theorem
MeasureTheory.eLpNorm_star
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{R : Type u_5}
[NormedAddCommGroup R]
[StarAddMonoid R]
[NormedStarGroup R]
{p : ENNReal}
{f : α → R}
:
@[simp]
theorem
MeasureTheory.AEEqFun.eLpNorm_star
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{R : Type u_5}
[NormedAddCommGroup R]
[StarAddMonoid R]
[NormedStarGroup R]
{p : ENNReal}
{f : α →ₘ[μ] R}
:
theorem
MeasureTheory.MemLp.star
{α : Type u_1}
{m : MeasurableSpace α}
{μ : Measure α}
{R : Type u_5}
[NormedAddCommGroup R]
[StarAddMonoid R]
[NormedStarGroup R]
{p : ENNReal}
{f : α → R}
(hf : MemLp f p μ)
:
@[simp]
theorem
MeasureTheory.eLpNorm_conj
{α : Type u_1}
{m : MeasurableSpace α}
{𝕜 : Type u_5}
[RCLike 𝕜]
(f : α → 𝕜)
(p : ENNReal)
(μ : Measure α)
: