Coarse-graining support: Support.Sobolev.Fractional.EuclideanWspCompletedDualExtension

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Finite smooth-dual extension to the completed fractional-Sobolev graph

On the finite locus of the smooth negative fractional-Sobolev dual norm, the normalized pairing extends canonically from smooth tests to the completed two-component graph.

noncomputable def HCPolySupport.CubeEuclideanWspSmoothTest.pairingLinearMap {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q FiniteLpExponent.two) : CubeEuclideanWspSmoothTest Q s p.conjugate →ₗ[ℝ] ℝ

The normalized smooth pairing, bundled as a real linear functional.

Equations

• HCPolySupport.CubeEuclideanWspSmoothTest.pairingLinearMap F = { toFun := HCPolySupport.cubeEuclideanNormalizedSmoothPairing F, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def HCPolySupport.CubeEuclideanWspSmoothTest.completedPairingExtension {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q FiniteLpExponent.two) (_hD : cubeEuclideanNegativeWspSmoothDualENorm Q s p F < ⊤) : CubeEuclideanWspCompletedDualGraph Q s p.conjugate →L[ℝ] ℝ

The canonical extension of the smooth normalized pairing to the completed fractional-Sobolev graph.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.CubeEuclideanWspSmoothTest.completedPairingExtension_apply_graphToCompleted {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q FiniteLpExponent.two) (hD : cubeEuclideanNegativeWspSmoothDualENorm Q s p F < ⊤) (h : CubeEuclideanWspSmoothTest Q s p.conjugate) : (completedPairingExtension F hD) (graphToCompleted h) = cubeEuclideanNormalizedSmoothPairing F h

On the finite dual-norm locus, the completed pairing agrees exactly with the normalized smooth pairing on every smooth graph point.

theorem HCPolySupport.CubeEuclideanWspSmoothTest.completedPairingExtension_unique {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q FiniteLpExponent.two) (hD : cubeEuclideanNegativeWspSmoothDualENorm Q s p F < ⊤) (G : CubeEuclideanWspCompletedDualGraph Q s p.conjugate →L[ℝ] ℝ) (hG : ∀ (h : CubeEuclideanWspSmoothTest Q s p.conjugate), G (graphToCompleted h) = cubeEuclideanNormalizedSmoothPairing F h) : completedPairingExtension F hD = G

The finite-locus extension is unique among continuous linear maps that agree with the normalized pairing on the dense smooth graph.

theorem HCPolySupport.CubeEuclideanWspSmoothTest.enorm_completedPairingExtension_eq_negativeWspSmoothDualENorm {d : ℕ} {Q : TriadicCube d} {s : ↑FractionalOrder} {p : FiniteLpExponent} (F : CubeEuclideanLpField Q FiniteLpExponent.two) (hD : cubeEuclideanNegativeWspSmoothDualENorm Q s p F < ⊤) : ‖completedPairingExtension F hD‖ₑ = cubeEuclideanNegativeWspSmoothDualENorm Q s p F

On the finite locus, the extension has exactly the smooth negative dual norm as its extended operator norm.