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

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

Local one-ball data from an interior parent solution

The interior good-lambda argument extends a solution gradient and its datum by zero from the next centered parent cube. On every stopping comparison parent, this module supplies the inputs of sqWeightedMeasure_oneStoppingBall_le: global L² membership, a restricted solution, almost-everywhere gradient identification, and the restricted weak divergence equation with the zero-extended datum.

The construction starts from an arbitrary H¹ solution on the parent cube. It uses neither a zero-trace premise nor a reflection factor.

The generic API works over any open parent set containing the comparison axis cube. The centered-cube API below is its geometry-specific specialization.

noncomputable def HCPolySupport.CubeCalderonZygmund.openParentGradientExtension {d : ℕ} (U : Set (Vec d)) (uU : H1Function U) : Vec d → HilbertVec d

The zero extension of a solution gradient from an arbitrary parent set.

Equations

• HCPolySupport.CubeCalderonZygmund.openParentGradientExtension U uU = U.indicator (HCPolySupport.hilbertifyVecField uU.grad)

noncomputable def HCPolySupport.CubeCalderonZygmund.openParentDatumExtension {d : ℕ} (U : Set (Vec d)) (HU : Vec d → Vec d) : Vec d → Vec d

The zero extension of a vector datum from an arbitrary parent set.

Equations

• HCPolySupport.CubeCalderonZygmund.openParentDatumExtension U HU = U.indicator HU

def HCPolySupport.CubeCalderonZygmund.openParentLocalSolution {d : ℕ} (U : Set (Vec d)) (z : Vec d) (L : ℝ) (uU : H1Function U) (hBU : axisCube z L ⊆ U) : H1Function (axisCube z L)

Restrict a parent solution to an axis cube contained in its domain.

Equations

• HCPolySupport.CubeCalderonZygmund.openParentLocalSolution U z L uU hBU = uU.restrict ⋯ hBU

theorem HCPolySupport.CubeCalderonZygmund.hilbertifyVecField_openParentDatumExtension {d : ℕ} (U : Set (Vec d)) (HU : Vec d → Vec d) : hilbertifyVecField (openParentDatumExtension U HU) = U.indicator (hilbertifyVecField HU)

Hilbertification commutes with extension by zero from an arbitrary set.

theorem HCPolySupport.CubeCalderonZygmund.openParent_axisCube_inputs {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {z : Vec d} {L sigma0 : ℝ} (hBU : axisCube z L ⊆ U) (uU : H1Function U) (HU : Vec d → Vec d) (hHU : MemVectorL2 U HU) (hweak : ∀ (phi : Vec d → ℝ), ContDiff ℝ (↑⊤) phi → HasCompactSupport phi → tsupport phi ⊆ U → sigma0 * ∫ (y : Vec d) in U, vecDot (uU.grad y) (euclideanGradient phi y) = -∫ (y : Vec d) in U, vecDot (HU y) (euclideanGradient phi y)) : MeasureTheory.MemLp (openParentGradientExtension U uU) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (hilbertifyVecField (openParentDatumExtension U HU)) 2 MeasureTheory.volume ∧ openParentGradientExtension U uU =ᵐ[MeasureTheory.volume.restrict (axisCube z L)] hilbertifyVecField (openParentLocalSolution U z L uU hBU).grad ∧ ∀ (phi : Vec d → ℝ), ContDiff ℝ (↑⊤) phi → HasCompactSupport phi → tsupport phi ⊆ axisCube z L → sigma0 * ∫ (y : Vec d) in axisCube z L, vecDot ((openParentLocalSolution U z L uU hBU).grad y) (euclideanGradient phi y) = -∫ (y : Vec d) in axisCube z L, vecDot (openParentDatumExtension U HU y) (euclideanGradient phi y)

An H¹ solution on an arbitrary open parent set supplies all local inputs for an axis-cube comparison contained in that parent.

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

The zero extension of an interior parent solution's gradient.

Equations

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

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

The zero extension of an interior parent vector datum.

Equations

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

def HCPolySupport.CubeCalderonZygmund.interiorParentLocalSolution {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 restriction of an interior parent solution to a stopping comparison parent.

Equations

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

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

Hilbertification commutes with the interior datum's extension by zero.

theorem HCPolySupport.CubeCalderonZygmund.interiorParent_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 (interiorParentGradientExtension m uP) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (hilbertifyVecField (interiorParentDatumExtension m HP)) 2 MeasureTheory.volume ∧ interiorParentGradientExtension m uP =ᵐ[MeasureTheory.volume.restrict (axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth))] hilbertifyVecField (interiorParentLocalSolution 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 ((interiorParentLocalSolution m x r uP ⋯).grad y) (euclideanGradient phi y) = -∫ (y : Vec d) in axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth), vecDot (interiorParentDatumExtension m HP y) (euclideanGradient phi y)

One interior parent solution and datum supply all local inputs for a stopping-ball comparison. The local equation is derived by restriction from the parent equation, with its coefficient and minus sign unchanged.