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) : eLpNorm' f p μ ≤ c • eLpNorm' g 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) : eLpNorm' f p μ ≤ c • eLpNorm' g 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) : eLpNorm' f p μ ≤ c * eLpNorm' g p μ

If ‖f x‖ₑ ≤ c * ‖g x‖ₑ a.e., eLpNorm' f p μ ≤ c * eLpNorm' g p μ for all p ∈ (0, ∞).

theorem MeasureTheory.le_eLpNorm_of_bddBelow' {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_7} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (hp : p ≠ 0) (hp' : p ≠ ⊤) {f : α → ε} (C : ENNReal) {s : Set α} (hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖ₑ) : C * μ s ^ (1 / p.toReal) ≤ eLpNorm f p μ

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‖ₑ) : eLpNormEssSup f μ ≤ c • eLpNormEssSup g μ

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‖₊) : eLpNormEssSup f μ ≤ c • eLpNormEssSup g μ

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} (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ) (p : ENNReal) : eLpNorm f p μ ≤ c • eLpNorm g p μ

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} (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ c * ‖g x‖₊) (p : ENNReal) : eLpNorm f p μ ≤ c • eLpNorm g p μ

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) : eLpNorm f p μ = 0 ∧ eLpNorm g p μ = 0

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 : ℝ} (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c * ‖g x‖) (p : ENNReal) : eLpNorm f p μ ≤ ENNReal.ofReal c * eLpNorm g p μ

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} (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑c * ‖g x‖ₑ) (p : ENNReal) : eLpNorm f p μ ≤ ↑c * eLpNorm g p μ

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) (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ c * ‖g x‖ₑ) : eLpNorm f p μ ≤ c * eLpNorm g p μ

If ‖f x‖ₑ ≤ c * ‖g x‖ₑ, then eLpNorm f p μ ≤ c * eLpNorm g p μ.

This version allows c = ∞, but requires f 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 α} (hf : ∀ᵐ (x : α) ∂μ, x ∈ s → C ≤ ‖f x‖₊) : C • μ s ^ (1 / p.toReal) ≤ eLpNorm f p μ

@[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} : eLpNorm (star f) p μ = eLpNorm f p μ

@[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} : eLpNorm (↑(star f)) p μ = eLpNorm (↑f) p μ

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 μ) : MemLp (star f) p μ

@[simp]

theorem MeasureTheory.eLpNorm_conj {α : Type u_1} {m : MeasurableSpace α} {𝕜 : Type u_5} [RCLike 𝕜] (f : α → 𝕜) (p : ENNReal) (μ : Measure α) : eLpNorm ((starRingEnd (α → 𝕜)) f) p μ = eLpNorm f p μ

theorem MeasureTheory.MemLp.re {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {𝕜 : Type u_5} [RCLike 𝕜] {f : α → 𝕜} (hf : MemLp f p μ) : MemLp (fun (x : α) => RCLike.re (f x)) p μ

theorem MeasureTheory.MemLp.im {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {𝕜 : Type u_5} [RCLike 𝕜] {f : α → 𝕜} (hf : MemLp f p μ) : MemLp (fun (x : α) => RCLike.im (f x)) p μ