Coarse-graining support:

Support.Sobolev.Foundations.CubeCalderonZygmund.ScalarDivergenceGradientW1p

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

Paired-witness scalar divergence gradient endpoint

This internal bridge converts synchronized H¹ and W^{1,q} vector representatives into the W^{1,q} gradient endpoint supplied by the scalar Poisson Hessian estimate. The H¹ witness supplies the L² divergence and the integration-by-parts identity; the W^{1,q} witness supplies the finite exponent control.

def HCPolySupport.CubeCalderonZygmund.vectorW1pDivergence {d : ℕ} {Q : TriadicCube d} {q : FiniteLpExponent} (G : CubeVectorW1pFunction Q q) : Vec d → ℝ

The weak divergence of a cube vector W^{1,q} function, defined as its Jacobian trace.

Equations

• HCPolySupport.CubeCalderonZygmund.vectorW1pDivergence G x = ∑ i : Fin d, G.jacobian x i i

theorem HCPolySupport.CubeCalderonZygmund.exists_cubeVectorW1p_scalarDivergence_cz_of_paired (d : ℕ) [NeZero d] (q : FiniteLpExponent) : ∃ C < ⊤, ∀ (m : ℤ) (G2 : CubeVectorH1Function (originCube d m)) (Gq : CubeVectorW1pFunction (originCube d m) q), G2.toField = Gq.toField → (∀ (x : Vec d) (i j : Fin d), (G2.coord i).grad x j = Gq.jacobian x i j) → ∀ (u : H10Function (openCubeSet (originCube d m))), CubeDirichletDivergenceProblem (originCube d m) u G2.toField → ∃ (V : CubeVectorW1pFunction (originCube d m) q), V.toField = u.grad ∧ MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat (V.jacobian x)) q.exponent (normalizedCubeMeasure (originCube d m)) ≤ C * MeasureTheory.eLpNorm (fun (x : Vec d) => HilbertMat.ofMat (Gq.jacobian x)) q.exponent (normalizedCubeMeasure (originCube d m))

Internal paired-witness W^{1,q} endpoint for the gradient of a scalar Dirichlet divergence solution. The paired H¹ witness is used only to supply the L² forcing and weak integration by parts required by the scalar Hessian endpoint.