Distributional pairing for the completed pressure operator

Continuous dual pairings extend the L² identity from the dense intersection to every L^(3/2) input. Compact support is required only of the test function, not of a chosen representative of an Lp class.

noncomputable def CKN.Core.Endgame.lpPairingWith {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 linear functional obtained by pairing with a fixed function of conjugate exponent.

Equations

• CKN.Core.Endgame.lpPairingWith g = (ContinuousLinearMap.apply ℝ ℝ) g ∘SL ContinuousLinearMap.lpPairing MeasureTheory.volume p q (ContinuousLinearMap.mul ℝ ℝ)

theorem CKN.Core.Endgame.lpExtension_pairing_of_l2_identity {p q : ENNReal} [Fact (1 ≤ p)] [Fact (1 ≤ q)] [p.HolderConjugate q] {C : ℝ} (hp : p ≠ ⊤) (h : Foundation.Euclidean.LpExtensionInput p C) {lap rhs : Foundation.Parabolic.Vec3 → ℝ} (hlap : MeasureTheory.MemLp lap q MeasureTheory.volume) (hrhs : MeasureTheory.MemLp rhs q MeasureTheory.volume) (hidentity : ∀ (v : ↥(MeasureTheory.Lp ℝ p MeasureTheory.volume)), MeasureTheory.MemLp (↑↑v) 2 MeasureTheory.volume → ∫ (x : Foundation.Parabolic.Vec3), h.T (↑↑v) x * lap x = ∫ (x : Foundation.Parabolic.Vec3), ↑↑v x * rhs x) {f : Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f p MeasureTheory.volume) : ∫ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.lpExtensionRepresentative hp h f x * lap x = ∫ (x : Foundation.Parabolic.Vec3), f x * rhs x

A distributional pairing on the L² intersection extends to every Lp input.

theorem CKN.Core.Endgame.rieszSecondP1Extension_distributional_identity {i j : Fin 3} (hL2 : Foundation.Euclidean.RieszSecondL2Input i j) (hWeak11 : ∀ (f : Foundation.Parabolic.Vec3 → ℝ), Measurable f → MeasureTheory.Integrable f MeasureTheory.volume → MeasureTheory.MemLp f 2 MeasureTheory.volume → ∀ (l : ℝ), 0 < l → MeasureTheory.volume {x : Foundation.Parabolic.Vec3 | l < |Foundation.Euclidean.rieszSecondL2RawOperator hL2 f x|} ≤ (ENNReal.ofReal Foundation.Euclidean.rieszSecondWeakTypeConstant * ∫⁻ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.absE f x) / ENNReal.ofReal l) {f ψ : Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.rieszSecondP1ExtensionOperator hL2 hWeak11 f x * spatialLaplacian ψ x = ∫ (x : Foundation.Parabolic.Vec3), f x * mixedSecond ψ i j x

The actual completed pressure operator satisfies the distributional Hessian identity for every L^(3/2) input and smooth compactly supported test.