Lᵖ seminorm bounds out of bounds between the integrals ∫⁻ ‖·‖ₑ ^ p

For 0 < p < ∞ the Lᵖ seminorm of an a.e. strongly measurable v is the p-th root of ∫⁻ ‖v x‖ₑ ^ p ∂μ (a function that is not a.e. strongly measurable has seminorm ∞), so a bound ∫⁻ ‖v‖ₑ ^ p ≤ c ^ p * ∫⁻ ‖w‖ₑ ^ p between those integrals implies the bound ‖v‖_p ≤ c * ‖w‖_p between the seminorms. This file records that implication, which is the direction an estimate proved by integration produces.

The two functions are allowed to take values in different spaces, and those spaces need carry nothing beyond an extended norm, since that is all eLpNorm reads. In particular the statement covers comparing a function with its derivative.

Main declarations

• TauCeti.eLpNorm_rpow_eq_lintegral: for an a.e. measurable ℝ≥0∞-valued function, the p-th power of the Lᵖ seminorm is the integral ∫⁻ f ^ p.
• TauCeti.eLpNorm_le_of_ae_tendsto_ennreal: an ℝ≥0∞-valued Fatou lemma for the Lᵖ seminorm.
• TauCeti.eLpNorm_le_eLpNorm_of_lintegral_rpow_le: for an a.e. strongly measurable v, from ∫⁻ ‖v‖ₑ ^ p ≤ c ^ p * ∫⁻ ‖w‖ₑ ^ p conclude ‖v‖_p ≤ c * ‖w‖_p; no measurability of w is needed.
• TauCeti.rpow_lintegral_le_measure_univ_rpow_mul: Hölder's extended-valued integral inequality (∫⁻ u) ^ r ≤ μ univ ^ (r - 1) * ∫⁻ u ^ r for u : α → ℝ≥0∞. On a finite measure space it expresses the nesting L^r ⊆ L¹; for a general μ it is only the inequality.

theorem TauCeti.eLpNorm_rpow_eq_lintegral {α : Type u_1} [MeasurableSpace α] {p : ENNReal} (hp0 : p ≠ 0) (hp : p ≠ ⊤) {f : α → ENNReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f μ) : MeasureTheory.eLpNorm f p μ ^ p.toReal = ∫⁻ (a : α), f a ^ p.toReal ∂μ

For a finite nonzero exponent, the p-th power of the Lᵖ seminorm of an a.e. measurable ℝ≥0∞-valued function is the integral of the p-th power of that function. This is MeasureTheory.lintegral_rpow_enorm_eq_rpow_eLpNorm' read at an ℝ≥0∞-valued exponent and at a function whose enorm is the identity, which is the shape the extended-valued estimates use.

theorem TauCeti.eLpNorm_le_of_ae_tendsto_ennreal {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : ENNReal} (hp0 : p ≠ 0) (hp : p ≠ ⊤) {f : ℕ → α → ENNReal} {g : α → ENNReal} {c : ENNReal} (hf : ∀ (n : ℕ), AEMeasurable (f n) μ) (hlim : ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (g x))) (hle : ∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ c) : MeasureTheory.eLpNorm g p μ ≤ c

Fatou's lemma for the Lᵖ seminorm of ℝ≥0∞-valued functions. For a finite nonzero exponent, an almost everywhere pointwise limit of functions whose Lᵖ seminorms are bounded by c also has Lᵖ seminorm at most c.

theorem TauCeti.eLpNorm_le_eLpNorm_of_lintegral_rpow_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {G : Type u_2} {H : Type u_3} [ENorm G] [TopologicalSpace G] [ENorm H] [TopologicalSpace H] {v : α → G} {w : α → H} {c : ℝ} (hc : 0 ≤ c) {p : ENNReal} (hp₀ : p ≠ 0) (hp : p ≠ ⊤) (hv : MeasureTheory.AEStronglyMeasurable v μ) (h : ∫⁻ (x : α), ‖v x‖ₑ ^ p.toReal ∂μ ≤ ENNReal.ofReal (c ^ p.toReal) * ∫⁻ (x : α), ‖w x‖ₑ ^ p.toReal ∂μ) : MeasureTheory.eLpNorm v p μ ≤ ENNReal.ofReal c * MeasureTheory.eLpNorm w p μ

Turn a bound between the ∫⁻ ‖·‖ₑ ^ p integrals into a bound between the Lᵖ seminorms. The two functions may have different codomains, which is what lets such a bound compare a function with its derivative; only a topology and an extended norm on each is needed.

Only the function on the left has to be a.e. strongly measurable: without that its Lᵖ seminorm is ∞ by definition, whatever the integral bound says, while a non-measurable w only makes the right-hand side larger.

theorem TauCeti.rpow_lintegral_le_measure_univ_rpow_mul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {u : α → ENNReal} (hu : AEMeasurable u μ) {r : ℝ} (hr : 1 ≤ r) : (∫⁻ (x : α), u x ∂μ) ^ r ≤ μ Set.univ ^ (r - 1) * ∫⁻ (x : α), u x ^ r ∂μ

Hölder's inequality in extended-valued ∫⁻ form, raised to the power r: the L¹ integral of u : α → ℝ≥0∞ is controlled by its L^r integral at the cost of the factor μ univ ^ (r - 1). Stated for an ℝ≥0∞-valued u, so a norm-valued application passes fun x => ‖f x‖ₑ and needs only that this composite is measurable.

On a finite measure space this is the nesting L^r ⊆ L¹; for a general μ it is only the displayed inequality, which does not by itself give that inclusion. No finiteness is assumed, and the bound is not vacuous when μ univ = ∞: arithmetic in ℝ≥0∞ makes the right-hand side 0 rather than ∞ whenever ∫⁻ ‖f‖ₑ ^ r = 0, and the inequality still holds there because f then vanishes almost everywhere.