EuclideanWspSmoothDualBesovBound

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Source negative-Besov control of the smooth fractional dual

This module uses finite block projections. In particular, the represented field is used only through its L² integrability, never through a spurious Lᵖ upgrade.

noncomputable def HCPolySupport.cubeEuclideanNegativeWspSmoothDualBesovConstant (d : ℕ) : ENNReal

A finite dimension-only coefficient for the finite-projection smooth-dual estimate.

Equations

• HCPolySupport.cubeEuclideanNegativeWspSmoothDualBesovConstant d = ↑d * 3 ^ (↑d + 1) * HCPolySupport.cubeEuclideanWspExactOverlapFullControlConstant d

noncomputable def HCPolySupport.cubeEuclideanNegativeWspSmoothDualBesovScalarConstant (d : ℕ) : ENNReal

The dimension-dependent scalar constant for the smooth negative Sobolev dual bound.

Equations

• HCPolySupport.cubeEuclideanNegativeWspSmoothDualBesovScalarConstant d = 3 ^ (↑d + 1) * HCPolySupport.cubeEuclideanWspExactOverlapFullControlConstant d

theorem HCPolySupport.cubeEuclideanNegativeWspSmoothDualBesovConstant_lt_top (d : ℕ) : cubeEuclideanNegativeWspSmoothDualBesovConstant d < ⊤

theorem HCPolySupport.cubeBesovCoordinatePairing_le_negativeBesov_mul_fullSobolevNorm {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) (h : CubeEuclideanWspSmoothTest Q s p.conjugate) (i : Fin d) : ENNReal.ofReal |cubeBesovPairing Q (fun (x : Vec d) => F.toField x i) fun (x : Vec d) => h.toField x i| ≤ cubeEuclideanNegativeWspSmoothDualBesovScalarConstant d * Book.Ch03.ABK26.cubeEuclideanNegativeBesovESeminorm Q s p F * cubeEuclideanWspFullENorm Q s p.conjugate h.toField

A scalar-coordinate source-negative Besov bound for the smooth fractional-Sobolev dual pairing.

theorem HCPolySupport.normalizedSmoothPairing_le_negativeBesov_mul_fullSobolevNorm {d : ℕ} (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) (h : CubeEuclideanWspSmoothTest Q s p.conjugate) : ENNReal.ofReal |cubeEuclideanNormalizedSmoothPairing F h| ≤ cubeEuclideanNegativeWspSmoothDualBesovConstant d * Book.Ch03.ABK26.cubeEuclideanNegativeBesovESeminorm Q s p F * cubeEuclideanWspFullENorm Q s p.conjugate h.toField

theorem HCPolySupport.cubeEuclideanNegativeWspSmoothDualENorm_le_cubeEuclideanNegativeBesovESeminorm (d : ℕ) (Q : TriadicCube d) (s : ↑FractionalOrder) (p : FiniteLpExponent) (F : CubeEuclideanLpField Q FiniteLpExponent.two) : cubeEuclideanNegativeWspSmoothDualENorm Q s p F ≤ cubeEuclideanNegativeWspSmoothDualBesovConstant d * Book.Ch03.ABK26.cubeEuclideanNegativeBesovESeminorm Q s p F