Coarse-graining support:

Support.Sobolev.Foundations.CubeCalderonZygmund.InteriorHessianRowTailTransfer

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

Tail transfer from an interior gradient to a reflected Hessian row

This file is a purely measure-theoretic bridge. It consumes restricted almost-everywhere identities supplied by the reflected interior construction; it does not assert either identity or any PDE property.

theorem HCPolySupport.CubeCalderonZygmund.openParentGradientExtension_reflectedHessianRow_tail_transfer {d : ℕ} {m : ℤ} (i : Fin d) (R : Vec d → Vec d) (hR : MeasureTheory.AEStronglyMeasurable (fun (x : Vec d) => HilbertVec.ofVec (R x)) (MeasureTheory.volume.restrict (openCubeSet (originCube d m)))) (uU : H1Function (scaledOpenCubeSet (originCube d (m + 1)) (1 / 2))) (hUrow : hilbertifyVecField uU.grad =ᵐ[MeasureTheory.volume.restrict (scaledOpenCubeSet (originCube d (m + 1)) (1 / 2))] fun (x : Vec d) => HilbertVec.ofVec (cubeDirichletOddReflectionHessianRowVectorField (originCube d m) i R x)) (hQsource : openParentGradientExtension (scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)) uU =ᵐ[MeasureTheory.volume.restrict (openCubeSet (originCube d m))] fun (x : Vec d) => HilbertVec.ofVec (R x)) (a : ℝ) : (sqWeightedMeasure (openParentGradientExtension (scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)) uU) MeasureTheory.volume) ({x : Vec d | a < ‖openParentGradientExtension (scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)) uU x‖} ∩ openCubeSet (originCube d m)) = (sqWeightedMeasure (fun (x : Vec d) => HilbertVec.ofVec (R x)) MeasureTheory.volume) ({x : Vec d | a < ‖HilbertVec.ofVec (R x)‖} ∩ openCubeSet (originCube d m)) ∧ (sqWeightedMeasure (openParentGradientExtension (scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)) uU) MeasureTheory.volume) ({x : Vec d | a < ‖openParentGradientExtension (scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)) uU x‖} ∩ scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)) ≤ 3 ^ d * (sqWeightedMeasure (fun (x : Vec d) => HilbertVec.ofVec (R x)) MeasureTheory.volume) ({x : Vec d | a < ‖HilbertVec.ofVec (R x)‖} ∩ openCubeSet (originCube d m))

Transfer square-weighted tails from the zero-extended gradient on the half parent to a reflected Hessian row and then to its source row.

The two restricted a.e. identities are explicit inputs: one identifies the interior gradient with the reflected row on the half parent, and the other identifies its zero extension with the source row on the source cube.