Comparison of Lᵖ seminorms

On a finite measure space, Mathlib's exponent comparison eLpNorm_le_eLpNorm_mul_rpow_measure_univ bounds the L¹ seminorm by the Lᵖ seminorm (for 1 ≤ p) times a finite constant. This file packages that comparison as a convergence statement both for the L¹ seminorm and for the Bochner integral ∫ ‖f i‖ ∂μ, the form in which L¹ convergence of a difference f i = W i - a is usually consumed.

It also contains the comparison of seminorms of exponents related by 1 / s = r / p for pointwise bounds ‖u‖ ≤ ‖f‖ ^ r.

On an arbitrary measure space, a common bound for the Lᵖ seminorm and the essential supremum also bounds every intermediate Lᵠ seminorm (MeasureTheory.eLpNorm_le_of_exponent_le). This comparison is useful for embeddings of real interpolation spaces.

Main declarations

• TauCeti.eLpNorm_le_eLpNorm_rpow: if ‖u‖ ≤ ‖f‖ ^ r, then ‖u‖_s ≤ ‖f‖_p ^ r when 1 / s = r / p.
• TauCeti.eLpNorm_le_eLpNorm_rpow_toReal_sub_one: its form for Hölder conjugate exponents.
• TauCeti.MeasureTheory.tendsto_eLpNorm_one_of_tendsto_eLpNorm: convergence to zero in Lᵖ for 1 ≤ p implies convergence to zero in L¹.
• TauCeti.MeasureTheory.tendsto_integral_norm_of_tendsto_eLpNorm: if eLpNorm (f i) p μ → 0 for some 1 ≤ p, then ∫ ‖f i‖ ∂μ → 0.
• TauCeti.MeasureTheory.not_tendsto_eLpNorm_sub_of_separated: a sequence whose terms stay a definite L¹ distance apart has no subsequence converging in Lᵖ for any 1 ≤ p.

theorem TauCeti.eLpNorm_le_eLpNorm_rpow {α : Type u_1} {E : Type u_2} {F : Type u_3} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {f : α → E} {u : α → F} {p s : ENNReal} {r : ℝ} (hr : 0 ≤ r) (hu : MeasureTheory.AEStronglyMeasurable u μ) (hs : s⁻¹ = ENNReal.ofReal r * p⁻¹) (hle : ∀ᵐ (x : α) ∂μ, ‖u x‖ ≤ ‖f x‖ ^ r) : MeasureTheory.eLpNorm u s μ ≤ MeasureTheory.eLpNorm f p μ ^ r

If ‖u‖ ≤ ‖f‖ ^ r almost everywhere with r ≥ 0, then ‖u‖_s ≤ ‖f‖_p ^ r for the exponent 1 / s = r / p. For r = 0 this reads ‖u‖_∞ ≤ 1.

theorem TauCeti.eLpNorm_le_eLpNorm_rpow_toReal_sub_one {α : Type u_1} {E : Type u_2} {F : Type u_3} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [NormedAddCommGroup E] [NormedAddCommGroup F] {q q' : ENNReal} [hqq : q.HolderConjugate q'] (hq : q ≠ ⊤) {f : α → E} {g : α → F} (hg : MeasureTheory.AEStronglyMeasurable g μ) (hle : ∀ᵐ (x : α) ∂μ, ‖g x‖ ≤ ‖f x‖ ^ (q.toReal - 1)) : MeasureTheory.eLpNorm g q' μ ≤ MeasureTheory.eLpNorm f q μ ^ (q.toReal - 1)

If ‖g‖ ≤ ‖f‖ ^ (q - 1) almost everywhere, then ‖g‖_{q'} ≤ ‖f‖_q ^ (q - 1) for Hölder conjugate exponents q < ∞ and q'.

theorem TauCeti.MeasureTheory.sub_one_div_toReal_nonneg {p : ENNReal} (hp : 1 ≤ p) : 0 ≤ 1 / ENNReal.toReal 1 - 1 / p.toReal

The exponent 1 / 1 - 1 / p comparing L¹ with Lᵖ on a finite measure is nonnegative when 1 ≤ p.

theorem TauCeti.MeasureTheory.tendsto_eLpNorm_one_of_tendsto_eLpNorm {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {l : Filter ι} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : ι → Ω → E} {p : ENNReal} (hp : 1 ≤ p) (h : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (f i) p μ) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (f i) 1 μ) l (nhds 0)

On a finite measure space, convergence to zero in Lᵖ for 1 ≤ p implies convergence to zero in L¹. No measurability hypothesis or finiteness assumption on p is needed.

theorem TauCeti.MeasureTheory.tendsto_integral_norm_of_tendsto_eLpNorm {Ω : Type u_1} [MeasurableSpace Ω] {ι : Type u_2} {E : Type u_3} [NormedAddCommGroup E] {l : Filter ι} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : ι → Ω → E} {p : ENNReal} (hp : 1 ≤ p) (h : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (f i) p μ) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => ∫ (ω : Ω), ‖f i ω‖ ∂μ) l (nhds 0)

Lᵖ convergence implies L¹ convergence on a finite measure space. If 1 ≤ p and a family f tends to 0 in Lᵖ along a filter l, then ∫ ‖f i‖ tends to 0 along l. No measurability hypothesis is needed: eLpNorm (f i) p μ is finite eventually along l, which forces f i to be a.e. strongly measurable.

theorem TauCeti.MeasureTheory.not_tendsto_eLpNorm_sub_of_separated {Ω : Type u_1} [MeasurableSpace Ω] {E : Type u_2} [NormedAddCommGroup E] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : ℕ → Ω → E} {ε : ENNReal} (hε : 0 < ε) (hsep : ∀ᶠ (m : ℕ) (n : ℕ) in Filter.atTop, ε ≤ MeasureTheory.eLpNorm (f m - f n) 1 μ) {p : ENNReal} (hp : 1 ≤ p) {φ : ℕ → ℕ} (hφ : StrictMono φ) {g : Ω → E} : ¬Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm (f (φ k) - g) p μ) Filter.atTop (nhds 0)

If, for all large m, the terms f n with n large stay at L¹ distance at least ε from f m, then no subsequence of f converges in Lᵖ for any 1 ≤ p, on a finite measure.

theorem MeasureTheory.eLpNorm_le_one_of_exponent_le {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [SeminormedAddCommGroup E] {μ : Measure α} {f : α → E} {p q : ENNReal} (hf : AEStronglyMeasurable f μ) (hp : 0 < p) (hpq : p ≤ q) (hfp : eLpNorm f p μ ≤ 1) (hf1 : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ 1) : eLpNorm f q μ ≤ 1

If both the Lᵖ seminorm and the essential supremum are at most one, every larger-exponent Lᵠ seminorm is at most one, even on an infinite measure space.

theorem MeasureTheory.eLpNorm_le_of_exponent_le {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [SeminormedAddCommGroup E] {μ : Measure α} {f : α → E} {p q : ENNReal} (hf : AEStronglyMeasurable f μ) (hp : 0 < p) (hpq : p ≤ q) {M : ℝ} (hM : 0 < M) (hfp : eLpNorm f p μ ≤ ENNReal.ofReal M) (hfM : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ M) : eLpNorm f q μ ≤ ENNReal.ofReal M

A common positive bound for the Lᵖ seminorm and the essential supremum bounds every Lᵠ seminorm with p ≤ q. No finiteness assumption on the measure is needed.