Coarse-graining support:

Support.Sobolev.Foundations.CubeCalderonZygmund.ReflectedParentHessianRowIdentification

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

Identifying the reflected-parent weak Hessian

The canonical interior H² construction on the half-scaled reflected parent produces an abstract weak Hessian. This file identifies each of its rows almost everywhere with the mixed-parity reflection of the corresponding source row. The proof uses weak-derivative uniqueness on each open reflection cell and the fact that the finitely many cells cover the centered parent modulo reflecting faces of measure zero.

theorem HCPolySupport.HasWeakHessianOn.cubeDirichletOddReflectionParent_innerHalf_hessianRow_ae_eq {d : ℕ} {m : ℤ} {u : H1Function (openCubeSet (originCube d m))} (Hsrc : HasWeakHessianOn (openCubeSet (originCube d m)) u) {uP : H1Function (openCubeSet (originCube d (m + 1)))} (huP_grad : uP.grad = cubeDirichletOddReflectionVectorField (originCube d m) fun (y : Vec d) => u.grad y) {uU : H1Function (scaledOpenCubeSet (originCube d (m + 1)) (1 / 2))} (huU_grad : uU.grad = uP.grad) (HU : HasWeakHessianOn (scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)) uU) (i : Fin d) : (fun (x : Vec d) => HilbertVec.ofVec fun (j : Fin d) => HU.hess i j x) =ᵐ[MeasureTheory.volume.restrict (scaledOpenCubeSet (originCube d (m + 1)) (1 / 2))] fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField (originCube d m) i (fun (y : Vec d) (j : Fin d) => Hsrc.hess i j y) x)

On the half-scaled reflected parent, the weak Hessian row of the canonical interior representative is the mixed-parity reflection of the source row.

The two exact gradient identities are precisely those returned by exists_cubeDirichletOddReflectionParent_innerHalf_hasWeakHessianOn.