Norming Lᵖ functions by test functions

For Hölder conjugate exponents 1 / q + 1 / q' = 1, the L^q norm of a function h is the supremum of the pairings |∫ h g| over simple functions g of L^{q'} norm at most one. This file proves the half of that duality which is used to bound a norm: if ‖∫ h g‖ ≤ C ‖g‖_{q'} for every simple g ∈ L^{q'}, then ‖h‖_q ≤ C.

For q < ∞ this holds for every h ∈ L^q, on any measure space. The test function is the extremal one conj g * |g| ^ (q - 2) of a simple approximation g of h. For q = ∞ it needs the measure to be σ-finite (on a measure with an atom of infinite measure every integrable g vanishes on the atom), and it reduces to the case q = 1 on a set of finite positive measure where ‖h‖ is close to its essential supremum.

Testing against simple functions only, rather than against all of L^{q'}, is what makes the statement usable when the pairings can only be computed on simple functions, as in the Riesz–Thorin theorem. Together with Hölder's inequality, the duality bound shows that the integral pairing g ↦ (f ↦ ∫ g f dμ) is a linear isometry from L^q(μ) to the continuous dual of L^q'(μ) on a σ-finite measure space.

For functions with values in an inner product space, paired by ∫ ⟪h, g⟫, the file also proves a version for q < ∞ that does not assume h ∈ L^q in advance: the test functions are bounded and vanish off a set of finite measure, and the extremal function |h| ^ (q - 2) h is truncated where h is large and outside a spanning set of a σ-finite measure. This is the form needed to prove that an operator defined on L² maps L² ∩ Lᵖ into L^q by duality.

The integral Hölder bounds apply to arbitrary functions, using the convention that eLpNorm is ∞ outside the almost everywhere strongly measurable functions.

Main declarations

• TauCeti.enorm_integral_mul_le: Hölder's inequality ‖∫ u v‖ ≤ ‖u‖_p ‖v‖_q for an integral.
• MeasureTheory.MemLp.eLpNorm_le_of_forall_enorm_integral_mul_le_of_ne_top: the duality bound for q < ∞.
• MeasureTheory.AEStronglyMeasurable.eLpNorm_top_le_of_forall_enorm_integral_mul_le and MeasureTheory.MemLp.eLpNorm_top_le_of_forall_enorm_integral_mul_le: the duality bound for q = ∞ on a σ-finite measure space, the first without assuming h ∈ L^∞ in advance.
• MeasureTheory.MemLp.eLpNorm_le_of_forall_enorm_integral_mul_le: the duality bound for every 1 ≤ q ≤ ∞ on a σ-finite measure space.
• MeasureTheory.Lp.enorm_integral_mul_le_of_apply_eq: a continuous linear functional on L^q' that is integration against h satisfies the hypothesis of these duality bounds.
• MeasureTheory.Lp.toDual: on a σ-finite measure space, the integral pairing is a linear isometry L^q(μ) → L^q'(μ)*.
• MeasureTheory.Lp.toDual_indicatorConstLp: the value of the pairing at an indicator function.
• TauCeti.enorm_integral_inner_le: Hölder's inequality ‖∫ ⟪u, v⟫‖ ≤ ‖u‖_p ‖v‖_q.
• MeasureTheory.AEStronglyMeasurable.eLpNorm_le_of_forall_enorm_integral_inner_le: the duality bound for q < ∞ for inner product space valued functions, against bounded test functions of finite-measure support, without assuming h ∈ L^q.

References

• G. B. Folland, Real Analysis, second edition, Theorem 6.14.

theorem TauCeti.enorm_integral_mul_le {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_4} [NonUnitalNormedRing 𝕜] [NormedSpace ℝ 𝕜] {p q : ENNReal} [p.HolderConjugate q] {u v : α → 𝕜} : ‖∫ (x : α), u x * v x ∂μ‖ₑ ≤ MeasureTheory.eLpNorm u p μ * MeasureTheory.eLpNorm v q μ

Hölder's inequality for the integral of a product: ‖∫ u v‖ ≤ ‖u‖_p ‖v‖_q for Hölder conjugate exponents p and q.

theorem TauCeti.enorm_integral_inner_le {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {𝕜 : Type u_4} {H : Type u_5} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {p q : ENNReal} [p.HolderConjugate q] {u v : α → H} : ‖∫ (x : α), inner 𝕜 (u x) (v x) ∂μ‖ₑ ≤ MeasureTheory.eLpNorm u p μ * MeasureTheory.eLpNorm v q μ

Hölder's inequality for the integral of an inner product: ‖∫ ⟪u, v⟫‖ ≤ ‖u‖_p ‖v‖_q for Hölder conjugate exponents p and q.

theorem MeasureTheory.MemLp.eLpNorm_le_of_forall_enorm_integral_mul_le_of_ne_top {α : Type u_1} {𝕜 : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [RCLike 𝕜] {q q' : ENNReal} [hqq : q.HolderConjugate q'] {h : α → 𝕜} (hh : MemLp h q μ) (hq : q ≠ ⊤) {C : ENNReal} (hC : ∀ (g : SimpleFunc α 𝕜), MemLp (⇑g) q' μ → ‖∫ (x : α), h x * g x ∂μ‖ₑ ≤ C * eLpNorm (⇑g) q' μ) : eLpNorm h q μ ≤ C

Norming by simple functions, q < ∞. Let q < ∞ and q' be Hölder conjugate. If h ∈ L^q satisfies ‖∫ h g‖ ≤ C ‖g‖_{q'} for every simple function g ∈ L^{q'}, then ‖h‖_q ≤ C.

theorem MeasureTheory.AEStronglyMeasurable.eLpNorm_top_le_of_forall_enorm_integral_mul_le {α : Type u_1} {𝕜 : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [RCLike 𝕜] [SigmaFinite μ] {h : α → 𝕜} (hmeas : AEStronglyMeasurable h μ) (hint : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn h s μ) {C : ENNReal} (hC : ∀ (g : SimpleFunc α 𝕜), MemLp (⇑g) 1 μ → ‖∫ (x : α), h x * g x ∂μ‖ₑ ≤ C * eLpNorm (⇑g) 1 μ) : eLpNorm h ⊤ μ ≤ C

Norming by simple functions, q = ∞. On a σ-finite measure space, let h be almost everywhere strongly measurable and integrable on every set of finite measure. If h satisfies ‖∫ h g‖ ≤ C ‖g‖₁ for every simple function g ∈ L¹, then ‖h‖_∞ ≤ C. In particular h ∈ L^∞ as soon as C < ∞.

theorem MeasureTheory.MemLp.eLpNorm_top_le_of_forall_enorm_integral_mul_le {α : Type u_1} {𝕜 : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [RCLike 𝕜] [SigmaFinite μ] {h : α → 𝕜} (hh : MemLp h ⊤ μ) {C : ENNReal} (hC : ∀ (g : SimpleFunc α 𝕜), MemLp (⇑g) 1 μ → ‖∫ (x : α), h x * g x ∂μ‖ₑ ≤ C * eLpNorm (⇑g) 1 μ) : eLpNorm h ⊤ μ ≤ C

Norming by simple functions, q = ∞. On a σ-finite measure space, if h ∈ L^∞ satisfies ‖∫ h g‖ ≤ C ‖g‖₁ for every simple function g ∈ L¹, then ‖h‖_∞ ≤ C.

theorem MeasureTheory.MemLp.eLpNorm_le_of_forall_enorm_integral_mul_le {α : Type u_1} {𝕜 : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [RCLike 𝕜] [SigmaFinite μ] {q q' : ENNReal} [q.HolderConjugate q'] {h : α → 𝕜} (hh : MemLp h q μ) {C : ENNReal} (hC : ∀ (g : SimpleFunc α 𝕜), MemLp (⇑g) q' μ → ‖∫ (x : α), h x * g x ∂μ‖ₑ ≤ C * eLpNorm (⇑g) q' μ) : eLpNorm h q μ ≤ C

Norming by simple functions. On a σ-finite measure space, let q and q' be Hölder conjugate. If h ∈ L^q satisfies ‖∫ h g‖ ≤ C ‖g‖_{q'} for every simple function g ∈ L^{q'}, then ‖h‖_q ≤ C.

theorem MeasureTheory.Lp.enorm_integral_mul_le_of_apply_eq {α : Type u_1} {𝕜 : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [RCLike 𝕜] {q' : ENNReal} [Fact (1 ≤ q')] (Λ : StrongDual 𝕜 ↥(Lp 𝕜 q' μ)) {h σ : α → 𝕜} (hσ : MemLp σ q' μ) (hΛ : Λ (MemLp.toLp σ hσ) = ∫ (x : α), h x * ↑↑(MemLp.toLp σ hσ) x ∂μ) : ‖∫ (x : α), h x * σ x ∂μ‖ₑ ≤ ‖Λ‖ₑ * eLpNorm σ q' μ

If a continuous linear functional Λ on L^q'(μ) is integration against h at the class of σ, then ‖∫ h σ‖ ≤ ‖Λ‖ ‖σ‖_q'. This is the hypothesis of the norming lemmas above.

theorem MeasureTheory.AEStronglyMeasurable.eLpNorm_le_of_forall_enorm_integral_inner_le {α : Type u_1} {𝕜 : Type u_2} {mα : MeasurableSpace α} {μ : Measure α} [RCLike 𝕜] {H : Type u_3} [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] [SigmaFinite μ] {q q' : ENNReal} [hqq : q.HolderConjugate q'] (hq : q ≠ ⊤) {h : α → H} (hh : AEStronglyMeasurable h μ) {C : ENNReal} (hC : ∀ (g : α → H) (s : Set α), μ s ≠ ⊤ → (∀ x ∉ s, g x = 0) → MemLp g ⊤ μ → ‖∫ (x : α), inner 𝕜 (h x) (g x) ∂μ‖ₑ ≤ C * eLpNorm g q' μ) : eLpNorm h q μ ≤ C

Norming by bounded functions of finite-measure support. On a σ-finite measure space, let q < ∞ and q' be Hölder conjugate. If an almost everywhere strongly measurable h with values in an inner product space satisfies ‖∫ ⟪h, g⟫‖ ≤ C ‖g‖_{q'} for every bounded g vanishing off a set of finite measure, then ‖h‖_q ≤ C.

Unlike MemLp.eLpNorm_le_of_forall_enorm_integral_mul_le_of_ne_top, h is not assumed to lie in L^q: when C < ∞, membership in L^q follows from the conclusion. The test functions lie in every Lˢ, so the hypothesis only involves pairings that are defined, for instance, for every h ∈ L².

noncomputable def MeasureTheory.Lp.toDual {α : Type u_1} (𝕜 : Type u_2) [RCLike 𝕜] {mα : MeasurableSpace α} (μ : Measure α) (q q' : ENNReal) [Fact (1 ≤ q)] [Fact (1 ≤ q')] [q.HolderConjugate q'] [SigmaFinite μ] : ↥(Lp 𝕜 q μ) →ₗᵢ[𝕜] StrongDual 𝕜 ↥(Lp 𝕜 q' μ)

On a σ-finite measure space, for Hölder conjugate exponents q and q', the integral pairing g ↦ (f ↦ ∫ g f dμ) is a linear isometry from L^q(μ) to the continuous dual of L^q'(μ): integration against g is a continuous linear functional on L^q'(μ) of norm ‖g‖_q.

@[simp]

theorem MeasureTheory.Lp.toDual_apply {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mα : MeasurableSpace α} {μ : Measure α} {q q' : ENNReal} [Fact (1 ≤ q)] [Fact (1 ≤ q')] [q.HolderConjugate q'] [SigmaFinite μ] (g : ↥(Lp 𝕜 q μ)) (f : ↥(Lp 𝕜 q' μ)) : ((toDual 𝕜 μ q q') g) f = ∫ (x : α), ↑↑g x * ↑↑f x ∂μ

@[simp]

theorem MeasureTheory.Lp.toDual_indicatorConstLp {α : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {mα : MeasurableSpace α} {μ : Measure α} {q q' : ENNReal} [Fact (1 ≤ q)] [Fact (1 ≤ q')] [q.HolderConjugate q'] [SigmaFinite μ] (g : ↥(Lp 𝕜 q μ)) {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : 𝕜) : ((toDual 𝕜 μ q q') g) (indicatorConstLp q' hs hμs c) = (∫ (x : α) in s, ↑↑g x ∂μ) * c

Pairing g ∈ L^q(μ) with the indicator function of a set s of finite measure, scaled by c, gives c times the integral of g over s.