Density form of the distributional pairing identity

A continuous dual pairing on Lᵖ agrees on a dense set if it agrees there pointwise. Here the dense set is that of classes represented by smooth compactly supported functions, which is the form in which the distributional identity is checked against test functions in the Caffarelli–Kohn–Nirenberg argument. The continuous linear maps testPairing implement the pairing against a fixed dual class and are the device used to pass the identity from the dense set to every Lᵖ input.

noncomputable def CKN.Foundation.Euclidean.testPairing {p q : ENNReal} [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q] (g : ↥(MeasureTheory.Lp ℝ q MeasureTheory.volume)) : ↥(MeasureTheory.Lp ℝ p MeasureTheory.volume) →L[ℝ] ℝ

Continuous test-function pairing used to pass operator identities through Lᵖ limits.

Equations

• CKN.Foundation.Euclidean.testPairing g = (ContinuousLinearMap.apply ℝ ℝ) g ∘SL ContinuousLinearMap.lpPairing MeasureTheory.volume p q (ContinuousLinearMap.mul ℝ ℝ)

theorem CKN.Foundation.Euclidean.lpExtension_pairing_of_smooth_identity {p q : ENNReal} [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q] {C : ℝ} (hp : p ≠ ⊤) (h : LpExtensionInput p C) {test rhs : Parabolic.Vec3 → ℝ} (htest : MeasureTheory.MemLp test q MeasureTheory.volume) (hrhs : MeasureTheory.MemLp rhs q MeasureTheory.volume) (hidentity : ∀ (F : Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) F → HasCompactSupport F → ∫ (x : Parabolic.Vec3), lpExtensionRepresentative hp h F x * test x = ∫ (x : Parabolic.Vec3), F x * rhs x) {f : Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : ∫ (x : Parabolic.Vec3), lpExtensionRepresentative hp h f x * test x = ∫ (x : Parabolic.Vec3), f x * rhs x

The distributional pairing identity for an Lᵖ extension, assumed on the dense set of smooth compactly supported classes, holds for every Lᵖ input. This is the Caffarelli–Kohn–Nirenberg distributional pairing step in the form used when the identity is available against smooth test functions.