Weak L^p norm

The weak L^p (quasi)norm wnorm f p μ, defined as the Lorentz norm eLorentzNorm f p ∞ μ, the its explicit formula wnorm_eq_iSup_mul_distribution_rpow, and the predicate MemWLp.

noncomputable def MeasureTheory.wnorm {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [ENorm ε] [TopologicalSpace ε] (f : α → ε) (p : ENNReal) (μ : Measure α) : ENNReal

The weak L^p norm of a function, defined as the Lorentz norm with second exponent ∞.

Equations

• MeasureTheory.wnorm f p μ = MeasureTheory.eLorentzNorm f p ⊤ μ

theorem MeasureTheory.wnorm_of_not_aestronglyMeasurable {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] {f : α → ε} [TopologicalSpace ε] (hf : ¬AEStronglyMeasurable f μ) : wnorm f p μ = ⊤

@[simp]

theorem MeasureTheory.wnorm_zero {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} [TopologicalSpace ε] (hf : AEStronglyMeasurable f μ) : wnorm f 0 μ = 0

@[simp]

theorem MeasureTheory.wnorm_top {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} [TopologicalSpace ε] (hf : AEStronglyMeasurable f μ) : wnorm f ⊤ μ = eLpNormEssSup f μ

theorem MeasureTheory.wnorm_eq_iSup_mul_distribution_rpow {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] {f : α → ε} [TopologicalSpace ε] (hf : AEStronglyMeasurable f μ) (h₀ : p ≠ 0) (h : p ≠ ⊤) : wnorm f p μ = ⨆ (t : NNReal), ↑t * distribution f (↑t) μ ^ p.toReal⁻¹

theorem MeasureTheory.wnorm_one {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [ENorm ε] {f : α → ε} [TopologicalSpace ε] (hf : AEStronglyMeasurable f μ) : wnorm f 1 μ = ⨆ (t : NNReal), ↑t * distribution f (↑t) μ

theorem MeasureTheory.wnorm_toReal_le {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} {p : ENNReal} : wnorm (ENNReal.toReal ∘ f) p μ ≤ wnorm f p μ

theorem MeasureTheory.wnorm_toReal_eq {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {f : α → ENNReal} {p : ENNReal} (hf : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : wnorm (ENNReal.toReal ∘ f) p μ = wnorm f p μ

theorem MeasureTheory.wnorm_eq_iSup_rpow_mul_rearrangement {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [ENorm ε] [TopologicalSpace ε] {p : ENNReal} (p_nonzero : p ≠ 0) (p_ne_top : p ≠ ⊤) {f : α → ε} {μ : Measure α} (hf : AEStronglyMeasurable f μ) : wnorm f p μ = ⨆ (t : NNReal), ↑t ^ p.toReal⁻¹ * rearrangement f (↑t) μ

theorem MeasureTheory.eLorentzNorm_eq_wnorm {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {p : ENNReal} [ENorm ε] [TopologicalSpace ε] {f : α → ε} {μ : Measure α} : eLorentzNorm f p ⊤ μ = wnorm f p μ

theorem MeasureTheory.wnorm_mono_enorm_ae {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] [TopologicalSpace ε] {ε' : Type u_12} [TopologicalSpace ε'] [ENorm ε'] {f : α → ε} {g : α → ε'} (hf : AEStronglyMeasurable f μ) (h : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) : wnorm f p μ ≤ wnorm g p μ

theorem MeasureTheory.wnorm_indicator_const {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε : Type u_12} [TopologicalSpace ε] [ESeminormedAddMonoid ε] {a : ε} {s : Set α} (hs : MeasurableSet s) (h₀ : p ≠ 0) (h₁ : p ≠ ⊤) : wnorm (s.indicator (Function.const α a)) p μ = μ s ^ p.toReal⁻¹ * ‖a‖ₑ

theorem MeasureTheory.wnorm_iSup_of_monotone {α : Type u_12} [MeasurableSpace α] {p : ENNReal} (hp : p ≠ 0) (f : ℕ → α → ENNReal) (hf : Monotone f) (μ : Measure α) (hf' : ∀ (n : ℕ), AEMeasurable (f n) μ) : wnorm (fun (x : α) => ⨆ (n : ℕ), f n x) p μ = ⨆ (n : ℕ), wnorm (f n) p μ

def MeasureTheory.MemWLp {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} [ENorm ε] [TopologicalSpace ε] (f : α → ε) (p : ENNReal) (μ : Measure α) : Prop

A function is in weak-L^p if it has finite weak L^p norm. This implies that it is (strongly a.e.)-measurable, see MemWLp.aeStronglyMeasurable.

Equations

• MeasureTheory.MemWLp f p μ = (MeasureTheory.wnorm f p μ < ⊤)

theorem MeasureTheory.memWLp_iff_memLorentz {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] {f : α → ε} [TopologicalSpace ε] : MemWLp f p μ ↔ MemLorentz f p ⊤ μ

theorem MeasureTheory.MemWLp.aeStronglyMeasurable {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] {f : α → ε} [TopologicalSpace ε] (hf : MemWLp f p μ) : AEStronglyMeasurable f μ

theorem MeasureTheory.MemWLp.wnorm_lt_top {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] {f : α → ε} [TopologicalSpace ε] (hf : MemWLp f p μ) : wnorm f p μ < ⊤

theorem MeasureTheory.MemWLp.ennreal_toReal {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {f : α → ENNReal} (hf : MemWLp f p μ) : MemWLp (ENNReal.toReal ∘ f) p μ

theorem MeasureTheory.MemWLp.ae_ne_top {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [ENorm ε] {f : α → ε} [TopologicalSpace ε] (hf : MemWLp f p μ) (hp_zero : p ≠ 0 := by positivity) : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≠ ⊤

If a function f is MemWLp for p ≠ 0, then its norm is almost everywhere finite. For p = 0, the weak norm is always zero, so hf is vacuous.

theorem MeasureTheory.iSup_mul_distribution_rpow_le_eLpNorm' {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {p : ℝ} (p0 : 0 < p) : ⨆ (t : NNReal), ↑t * distribution f (↑t) μ ^ p⁻¹ ≤ eLpNorm' f p μ

theorem MeasureTheory.wnorm_le_eLpNorm {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) {p : ENNReal} (hp : 0 < p) : wnorm f p μ ≤ eLpNorm f p μ

theorem MeasureTheory.MemLp.memWLp {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hp : 0 < p) (hf : MemLp f p μ) : MemWLp f p μ

theorem MeasureTheory.wnorm_eq_zero_iff {α : Type u_1} {ε : Type u_3} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [TopologicalSpace ε] [ContinuousENorm ε] {f : α → ε} (hf : AEStronglyMeasurable f μ) (hp : p ≠ 0) : wnorm f p μ = 0 ↔ (fun (x : α) => ‖f x‖ₑ) =ᵐ[μ] 0

theorem MeasureTheory.wnorm_const_smul_le {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} {ε' : Type u_12} [TopologicalSpace ε'] [ESeminormedAddCommMonoid ε'] [Module NNReal ε'] [ENormSMulClass NNReal ε'] [ContinuousConstSMul NNReal ε'] (hp : p ≠ 0) {f : α → ε'} (hf : AEStronglyMeasurable f μ) (k : NNReal) : wnorm (k • f) p μ ≤ ‖k‖ₑ * wnorm f p μ

theorem MeasureTheory.wnorm_const_smul_le' {α : Type u_1} {𝕜 : Type u_7} {E : Type u_8} {m : MeasurableSpace α} {p : ENNReal} {μ : Measure α} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [MulActionWithZero 𝕜 E] [NormSMulClass 𝕜 E] [IsBoundedSMul 𝕜 E] (hp : p ≠ 0) {f : α → E} (hf : AEStronglyMeasurable f μ) (k : 𝕜) : wnorm (k • f) p μ ≤ ‖k‖ₑ * wnorm f p μ