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

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

Global parent geometry for cube Calderón–Zygmund stopping balls

The local harmonic comparison is made on an axis cube which realizes a sup-metric ball about a stopping point. When that point belongs to the centered cube at scale m, the conservative stopping cutoff keeps even the closed comparison parent inside the open centered cube at scale m + 1.

theorem HCPolySupport.CubeCalderonZygmund.closedBall_subset_openCubeSet_originCube_succ_of_mem {d : ℕ} {m : ℤ} {x : Vec d} {a : ℝ} (hx : x ∈ openCubeSet (originCube d m)) (ha_nonneg : 0 ≤ a) (ha : a ≤ cubeRadius (originCube d m) / 2) : Metric.closedBall x a ⊆ openCubeSet (originCube d (m + 1))

A closed ball of radius at most one quarter of the scale-m side length about a point of the centered scale-m cube lies in its open next parent.

The statement uses cubeRadius / 2 so it composes directly with the 10 * 3^n stopping cutoff.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonParentRadius_le_half_cubeRadius_of_le {d : ℕ} {m : ℤ} {r : ℝ} (n : ℕ) (hr : r ≤ cubeRadius (originCube d m) / (10 * 3 ^ n)) : stoppingComparisonParentMultiplier n * r ≤ cubeRadius (originCube d m) / 2

The depth-n comparison-parent radius is at most half the radius of the ambient centered cube under the standard stopping cutoff.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonParent_closedBall_subset_openCubeSet_originCube_succ {d : ℕ} {m : ℤ} {x : Vec d} {r : ℝ} (n : ℕ) (hx : x ∈ openCubeSet (originCube d m)) (hr_nonneg : 0 ≤ r) (hr : r ≤ cubeRadius (originCube d m) / (10 * 3 ^ n)) : Metric.closedBall x (stoppingComparisonParentMultiplier n * r) ⊆ openCubeSet (originCube d (m + 1))

The closed comparison-parent ball remains in the next centered open cube whenever the stopping point belongs to the present centered open cube and its radius obeys the standard cutoff.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonParent_axisCube_subset_openCubeSet_originCube_succ {d : ℕ} {m : ℤ} {x : Vec d} {r : ℝ} (n : ℕ) (hx : x ∈ openCubeSet (originCube d m)) (hr_pos : 0 < r) (hr : r ≤ cubeRadius (originCube d m) / (10 * 3 ^ n)) : axisCube (stoppingComparisonParentCorner x r n) (stoppingComparisonParentSide r n) ⊆ openCubeSet (originCube d (m + 1))

The open axis-cube comparison parent remains in the next centered open cube under the standard stopping cutoff.