Integrability of dual pairings

Pointwise evaluation pairs dual-valued and vector-valued functions with Hölder conjugate exponents to give an integrable scalar function. This supplies the integrability needed to split integrals in weak integration-by-parts formulas. The result specializes Mathlib's bilinear Hölder estimate ContinuousLinearMap.memLp_of_bilin to the dual pairing.

The Hölder pairing ContinuousLinearMap.lpPairing of the multiplication of a normed algebra is the integral of the product (ContinuousLinearMap.lpPairing_mul_eq_integral).

theorem MeasureTheory.MemLp.integrable_apply {α : Type u_1} {𝕜 : Type u_2} {V : Type u_3} [MeasurableSpace α] [NontriviallyNormedField 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] {μ : Measure α} {p q : ENNReal} [p.HolderConjugate q] {f : α → StrongDual 𝕜 V} {g : α → V} (hf : MemLp f p μ) (hg : MemLp g q μ) : Integrable (fun (x : α) => (f x) (g x)) μ

Evaluating a dual-valued L^p function on an L^q function is integrable when the exponents are Hölder conjugate.

theorem ContinuousLinearMap.lpPairing_mul_eq_integral {α : Type u_1} {𝕜 : Type u_2} {R : Type u_3} [NontriviallyNormedField 𝕜] [NonUnitalNormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] [NormedSpace ℝ R] [SMulCommClass ℝ 𝕜 R] [CompleteSpace R] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {q q' : ENNReal} [Fact (1 ≤ q)] [Fact (1 ≤ q')] [q.HolderConjugate q'] (g : ↥(MeasureTheory.Lp R q μ)) (f : ↥(MeasureTheory.Lp R q' μ)) : ((lpPairing μ q q' (mul 𝕜 R)) g) f = ∫ (x : α), ↑↑g x * ↑↑f x ∂μ

The Hölder pairing of the multiplication ContinuousLinearMap.mul 𝕜 R is the integral of the product.

theorem TauCeti.enorm_integral_smul_le {α : Type u_1} {𝕜 : Type u_2} {F : Type u_3} [MeasurableSpace α] [NormedField 𝕜] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure α} {p q : ENNReal} [p.HolderConjugate q] {a : α → 𝕜} {f : α → F} : ‖∫ (x : α), a x • f x ∂μ‖ₑ ≤ MeasureTheory.eLpNorm a p μ * MeasureTheory.eLpNorm f q μ

Hölder's inequality for the Bochner integral of a scalar multiple.