Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.ReflectedLocalInputs

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

Local one-ball data from a reflected parent solution

The global good-lambda argument extends the reflected parent solution and datum by zero. On each comparison parent that remains inside that reflected cube, this module supplies precisely the local inputs of sqWeightedMeasure_oneStoppingBall_le: global L² membership, the restricted solution, the almost-everywhere gradient identification, and the weak equation with the zero-extended datum. Thus the local PDE is derived from the single parent equation and is never an additional hypothesis.

noncomputable def HCPolySupport.CubeCalderonZygmund.reflectedParentGradientExtension {d : ℕ} (m : ℤ) (uP : H1Function (openCubeSet (originCube d (m + 1)))) : Vec d → HilbertVec d

The zero extension of the gradient of a reflected parent solution.

Equations

• HCPolySupport.CubeCalderonZygmund.reflectedParentGradientExtension m uP = (HCPolySupport.openCubeSet (HCPolySupport.originCube d (m + 1))).indicator (HCPolySupport.hilbertifyVecField uP.grad)

noncomputable def HCPolySupport.CubeCalderonZygmund.reflectedParentDatumExtension {d : ℕ} (m : ℤ) (HP : Vec d → Vec d) : Vec d → Vec d

The zero extension of a reflected parent vector datum.

Equations

• HCPolySupport.CubeCalderonZygmund.reflectedParentDatumExtension m HP = (HCPolySupport.openCubeSet (HCPolySupport.originCube d (m + 1))).indicator HP

def HCPolySupport.CubeCalderonZygmund.reflectedParentLocalSolution {d depth : ℕ} (m : ℤ) (x : Vec d) (r : ℝ) (uP : H1Function (openCubeSet (originCube d (m + 1)))) (hsub : axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth) ⊆ openCubeSet (originCube d (m + 1))) : H1Function (axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth))

The local solution on the comparison parent cut out of a reflected parent solution.

Equations

• HCPolySupport.CubeCalderonZygmund.reflectedParentLocalSolution m x r uP hsub = uP.restrict ⋯ hsub

theorem HCPolySupport.CubeCalderonZygmund.hilbertifyVecField_reflectedParentDatumExtension {d : ℕ} (m : ℤ) (HP : Vec d → Vec d) : hilbertifyVecField (reflectedParentDatumExtension m HP) = (openCubeSet (originCube d (m + 1))).indicator (hilbertifyVecField HP)

Hilbertification commutes with extension by zero.

theorem HCPolySupport.CubeCalderonZygmund.reflectedParent_oneStoppingBall_inputs {d depth : ℕ} {m : ℤ} {sigma0 : ℝ} {x : Vec d} {r : ℝ} (hx : x ∈ openCubeSet (originCube d m)) (hr : 0 < r) (hcutoff : r ≤ cubeRadius (originCube d m) / (10 * 3 ^ depth)) (uP : H1Function (openCubeSet (originCube d (m + 1)))) (HP : Vec d → Vec d) (hHP : MemVectorL2 (openCubeSet (originCube d (m + 1))) HP) (hweak : ∀ (phi : Vec d → ℝ), ContDiff ℝ (↑⊤) phi → HasCompactSupport phi → tsupport phi ⊆ openCubeSet (originCube d (m + 1)) → sigma0 * ∫ (y : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (uP.grad y) (euclideanGradient phi y) = -∫ (y : Vec d) in openCubeSet (originCube d (m + 1)), vecDot (HP y) (euclideanGradient phi y)) : MeasureTheory.MemLp (reflectedParentGradientExtension m uP) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (hilbertifyVecField (reflectedParentDatumExtension m HP)) 2 MeasureTheory.volume ∧ reflectedParentGradientExtension m uP =ᵐ[MeasureTheory.volume.restrict (axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth))] hilbertifyVecField (reflectedParentLocalSolution m x r uP ⋯).grad ∧ ∀ (phi : Vec d → ℝ), ContDiff ℝ (↑⊤) phi → HasCompactSupport phi → tsupport phi ⊆ axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth) → sigma0 * ∫ (y : Vec d) in axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth), vecDot ((reflectedParentLocalSolution m x r uP ⋯).grad y) (euclideanGradient phi y) = -∫ (y : Vec d) in axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth), vecDot (reflectedParentDatumExtension m HP y) (euclideanGradient phi y)

A fixed reflected parent solution and datum provide the local inputs for one stopping ball. The parent equation retains its exact coefficient and minus sign; the final equation is its restriction to the comparison parent.