Triangle inequality for Lorentz-seminorm

In this file we prove several versions of the triangle inequality for the Lorentz seminorm, as well as simple corollaries.

theorem MeasureTheory.eLpNorm_withDensity_scale_constant' {f : NNReal → ENNReal} (hf : AEStronglyMeasurable f volume) {p : ENNReal} {a : NNReal} (h : a ≠ 0) : eLpNorm (fun (t : NNReal) => f (a * t)) p (volume.withDensity fun (t : NNReal) => (↑t)⁻¹) = eLpNorm f p (volume.withDensity fun (t : NNReal) => (↑t)⁻¹)

theorem MeasureTheory.eLorentzNorm_add_le'' {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p q : ENNReal} {μ : Measure α} {f g : α → ε} : eLorentzNorm (f + g) p q μ ≤ 2 ^ p.toReal⁻¹ * LpAddConst q * (eLorentzNorm f p q μ + eLorentzNorm g p q μ)

theorem MeasureTheory.lintegral_antitone_mul_le {f g k : NNReal → ENNReal} (h : ∀ {t : NNReal}, ∫⁻ (s : NNReal) in Set.Iio t, f s ≤ ∫⁻ (s : NNReal) in Set.Iio t, g s) (hk : Antitone k) : ∫⁻ (s : NNReal), k s * f s ≤ ∫⁻ (s : NNReal), k s * g s

noncomputable def MeasureTheory.lorentz_helper {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] (f : α → ε) (p q : ENNReal) (μ : Measure α) : NNReal → ENNReal

The function k in the proof of Theorem 6.7 in https://doi.org/10.1007/978-3-319-30034-4

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.eLpNorm_lorentz_helper {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p q : ENNReal} {μ : Measure α} {f : α → ε} : eLpNorm (lorentz_helper f p q μ) q.conjExponent volume = 1

theorem MeasureTheory.antitone_rpow_inv_sub_inv {p q : ENNReal} (q_le_p : q ≤ p) (p_zero : ¬p = 0) (p_top : ¬p = ⊤) : Antitone fun (x : NNReal) => ↑x ^ (p.toReal⁻¹ - q.toReal⁻¹)

theorem MeasureTheory.antitone_lorentz_helper {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p q : ENNReal} {μ : Measure α} {f : α → ε} : Antitone (lorentz_helper f p q μ)

theorem MeasureTheory.lorentz_helper_measurable {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p q : ENNReal} {μ : Measure α} {f : α → ε} : Measurable (lorentz_helper f p q μ)

theorem MeasureTheory.eLorentzNorm'_eq_lintegral_lorentz_helper_mul {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p q : ENNReal} {μ : Measure α} {f : α → ε} : eLorentzNorm' f p q μ = eLpNorm (lorentz_helper f p q μ * fun (t : NNReal) => ↑t ^ (p⁻¹.toReal - q⁻¹.toReal) * rearrangement f (↑t) μ) 1 volume

theorem MeasureTheory.eLorentzNorm_add_le {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p q : ENNReal} {μ : Measure α} {f g : α → ε} (one_le_q : 1 ≤ q) (q_le_p : q ≤ p) [NoAtoms μ] (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : eLorentzNorm (f + g) p q μ ≤ eLorentzNorm f p q μ + eLorentzNorm g p q μ

noncomputable def MeasureTheory.LorentzAddConst (p r : ENNReal) : ENNReal

A constant for the inequality ‖f + g‖_{L^{p,q}} ≤ C * (‖f‖_{L^{p,q}} + ‖g‖_{L^{p,q}}). It is equal to 1 if p = 0 or 1 ≤ r ≤ p and 2^(1/p) * LpAddConst r else.

Equations

• MeasureTheory.LorentzAddConst p r = if p = 0 ∨ r ∈ Set.Icc 1 p then 1 else 2 ^ p.toReal⁻¹ * MeasureTheory.LpAddConst r

theorem MeasureTheory.LorentzAddConst_of_one_le {p q : ENNReal} (hr : q ∈ Set.Icc 1 p) : LorentzAddConst p q = 1

theorem MeasureTheory.LorentzAddConst_zero {q : ENNReal} : LorentzAddConst 0 q = 1

theorem MeasureTheory.LorentzAddConst_lt_top {p q : ENNReal} : LorentzAddConst p q < ⊤

theorem MeasureTheory.eLorentzNorm_add_le' {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p q : ENNReal} {μ : Measure α} {f g : α → ε} [NoAtoms μ] (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : eLorentzNorm (f + g) p q μ ≤ LorentzAddConst p q * (eLorentzNorm f p q μ + eLorentzNorm g p q μ)

theorem MeasureTheory.eLorentzNorm_add_lt_top {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p q : ENNReal} {μ : Measure α} {f g : α → ε} [NoAtoms μ] (hf : MemLorentz f p q μ) (hg : MemLorentz g p q μ) : eLorentzNorm (f + g) p q μ < ⊤

theorem MeasureTheory.MemLorentz.add {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p q : ENNReal} {μ : Measure α} {f g : α → ε} [NoAtoms μ] [ContinuousAdd ε] (hf : MemLorentz f p q μ) (hg : MemLorentz g p q μ) : MemLorentz (f + g) p q μ

theorem MeasureTheory.eLorentzNorm_add_le_of_disjoint_support {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p q : ENNReal} {μ : Measure α} {f g : α → ε} (h : Disjoint (Function.support f) (Function.support g)) (hg : AEStronglyMeasurable g μ) : eLorentzNorm (f + g) p q μ ≤ LpAddConst p * LpAddConst q * (eLorentzNorm f p q μ + eLorentzNorm g p q μ)