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.eLorentzNorm_add_le'' {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {p q : ENNReal} {μ : Measure α} {f g : α → ε} [ContinuousAdd ε] : eLorentzNorm (f + g) p q μ ≤ 2 ^ p.toReal⁻¹ * q.LpAddConst * (eLorentzNorm f p q μ + eLorentzNorm g p q μ)

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 : α → ε} (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤) (one_le_q : 1 ≤ q) (q_ne_top : q ≠ ⊤) (hf : eLorentzNorm' f p q μ ≠ 0) (hf' : eLorentzNorm' f p q μ ≠ ⊤) : 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) (q_zero : q ≠ 0) : 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 : α → ε} (hq : 1 ≤ q) (q_le_p : q ≤ p) (p_top : p ≠ ⊤) : 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 : α → ε} (p_ne_zero : p ≠ 0) (p_ne_top : p ≠ ⊤) (hq : 1 ≤ q) (q_ne_top : q ≠ ⊤) (f_ne_top : eLorentzNorm' f p q μ ≠ ⊤) : 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 : α → ε} [SigmaFinite μ] [ContinuousAdd ε] (one_le_q : 1 ≤ q) (q_le_p : q ≤ p) (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⁻¹ * r.LpAddConst

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 : α → ε} [SigmaFinite μ] [ContinuousAdd ε] (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 : α → ε} [SigmaFinite μ] [ContinuousAdd ε] (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 : α → ε} [SigmaFinite μ] [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 : α → ε} [ContinuousAdd ε] (h : Disjoint (Function.support f) (Function.support g)) (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : eLorentzNorm (f + g) p q μ ≤ p.LpAddConst * q.LpAddConst * (eLorentzNorm f p q μ + eLorentzNorm g p q μ)