Coarse-graining support: Support.Sobolev.Foundations.CubePoisson.DualTestNorm

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

Positive dual test-norm estimates for Poisson gradients

The endpoint inputs that the full-dual Besov pairing proof actually uses: each component of the Poisson gradient admits a positive uniform bound for all finite-depth dual test norms. The L²-facing wrapper combines this with the Calderon-Zygmund estimate, and the core wrapper packages the epsilon-free clean componentwise estimate into the positive B-bundle used downstream.

def HCPolySupport.CubePoissonGradientDualTestNormEstimate {d : ℕ} (Q : TriadicCube d) (C : ℝ) : Prop

Positive-test-norm control for Poisson gradients.

This is the endpoint input that the full-dual Besov pairing proof actually uses: each component of the Poisson gradient admits a positive uniform bound for all finite-depth dual test norms, and the sum of those bounds is controlled by the B¹_{2,∞} circ norm of the Poisson gradient up to an arbitrary epsilon. The epsilon slack keeps the zero-gradient case available while still implying the exact endpoint duality bound by a limiting argument.

Equations

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

def HCPolySupport.CubePoissonGradientDualTestNormL2Estimate {d : ℕ} (Q : TriadicCube d) (C : ℝ) : Prop

L²-facing positive-test-norm control for Poisson gradients.

This is the form obtained after composing the positive-test/circ estimate with the Neumann Calderon-Zygmund estimate. It is closer to the elliptic regularity statement that remains to be proved: the admissible positive Besov test bounds for ∇W are controlled directly by the normalized L² norm of the right-hand side.

Equations

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

def HCPolySupport.CubePoissonGradientDualTestNormL2CoreEstimate {d : ℕ} (Q : TriadicCube d) (C : ℝ) : Prop

Core direct L² positive-test bound for Poisson gradients.

This is the epsilon-free form one expects from Neumann W^{2,2}/CZ plus local Poincare: each component of ∇W has all finite positive dual test norms bounded by the same multiple of ‖F‖_{L²(Q)}. The theorem below turns this clean componentwise estimate into the positive B-package used by the endpoint duality wrapper.

Equations

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

theorem HCPolySupport.CubePoissonGradientDualTestNormL2CoreEstimate.to_l2Estimate {d : ℕ} {Q : TriadicCube d} {C : ℝ} (h : CubePoissonGradientDualTestNormL2CoreEstimate Q C) : CubePoissonGradientDualTestNormL2Estimate Q (↑d * C)

theorem HCPolySupport.CubePoissonGradientDualTestNormEstimate.to_l2Estimate {d : ℕ} {Q : TriadicCube d} {Ctest Ccz : ℝ} (htest : CubePoissonGradientDualTestNormEstimate Q Ctest) (hcz : CubeNeumannPoissonGradientBesovEstimate Q Ccz) : CubePoissonGradientDualTestNormL2Estimate Q (Ctest * Ccz)