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

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

Axis cubes at a good-lambda stopping scale

The Vitali argument is formulated with sup-metric balls in Vec d. This module identifies those balls with the axis cubes used by the harmonic replacement and harmonic-gain APIs. The comparison parent has radius 5 * 3^n * r; its concentric depth-n descendant is exactly the comparison ball of radius 5 * r.

def HCPolySupport.CubeCalderonZygmund.stoppingAxisCubeCorner {d : ℕ} (x : Vec d) (S r : ℝ) : Vec d

The lower corner of the axis cube representing the sup-metric ball of radius S * r around x.

Equations

• HCPolySupport.CubeCalderonZygmund.stoppingAxisCubeCorner x S r i = x i - S * r

def HCPolySupport.CubeCalderonZygmund.stoppingAxisCubeSide (S r : ℝ) : ℝ

The side length of the axis cube representing the sup-metric ball of radius S * r around x.

Equations

• HCPolySupport.CubeCalderonZygmund.stoppingAxisCubeSide S r = 2 * S * r

theorem HCPolySupport.CubeCalderonZygmund.axisCube_stoppingAxisCubeCorner_eq_ball {d : ℕ} (x : Vec d) {S r : ℝ} (hS : 0 < S) (hr : 0 < r) : axisCube (stoppingAxisCubeCorner x S r) (stoppingAxisCubeSide S r) = Metric.ball x (S * r)

A positive-radius sup-metric ball is exactly its open axis-cube realization.

theorem HCPolySupport.CubeCalderonZygmund.axisCube_stoppingAxisCubeCorner_ae_eq_closedBall {d : ℕ} [NeZero d] (x : Vec d) {S r : ℝ} (hS : 0 < S) (hr : 0 < r) : axisCube (stoppingAxisCubeCorner x S r) (stoppingAxisCubeSide S r) =ᵐ[MeasureTheory.volume] Metric.closedBall x (S * r)

The open stopping cube and its closed sup-metric ball agree almost everywhere for Lebesgue measure.

def HCPolySupport.CubeCalderonZygmund.stoppingComparisonParentMultiplier (n : ℕ) : ℝ

The comparison parent multiplier: after n concentric contractions, a radius 5 * 3^n * r becomes 5 * r.

Equations

• HCPolySupport.CubeCalderonZygmund.stoppingComparisonParentMultiplier n = 5 * 3 ^ n

def HCPolySupport.CubeCalderonZygmund.stoppingComparisonParentCorner {d : ℕ} (x : Vec d) (r : ℝ) (n : ℕ) : Vec d

The parent cube used for a depth-n harmonic comparison at stopping radius r.

Equations

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

def HCPolySupport.CubeCalderonZygmund.stoppingComparisonParentSide (r : ℝ) (n : ℕ) : ℝ

The side length of the comparison parent cube.

Equations

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

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonParent_axisCube_eq_ball {d : ℕ} (x : Vec d) {r : ℝ} (hr : 0 < r) (n : ℕ) : axisCube (stoppingComparisonParentCorner x r n) (stoppingComparisonParentSide r n) = Metric.ball x (stoppingComparisonParentMultiplier n * r)

The comparison parent is the open sup-metric ball with radius 5 * 3^n * r.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonParent_axisCube_ae_eq_closedBall {d : ℕ} [NeZero d] (x : Vec d) {r : ℝ} (hr : 0 < r) (n : ℕ) : axisCube (stoppingComparisonParentCorner x r n) (stoppingComparisonParentSide r n) =ᵐ[MeasureTheory.volume] Metric.closedBall x (stoppingComparisonParentMultiplier n * r)

The comparison parent and its closed sup-metric ball agree almost everywhere.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparison_concentricDepth_axisCube_eq_ball {d : ℕ} (x : Vec d) {r : ℝ} (hr : 0 < r) (n : ℕ) : axisCube (axisCubeConcentricDepthCorner (stoppingComparisonParentCorner x r n) (stoppingComparisonParentSide r n) n) (axisCubeConcentricDepthSide (stoppingComparisonParentSide r n) n) = Metric.ball x (5 * r)

The depth-n concentric descendant of the comparison parent is exactly the stopping-scale comparison ball of radius 5 * r.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparison_concentricDepth_axisCube_ae_eq_closedBall {d : ℕ} [NeZero d] (x : Vec d) {r : ℝ} (hr : 0 < r) (n : ℕ) : axisCube (axisCubeConcentricDepthCorner (stoppingComparisonParentCorner x r n) (stoppingComparisonParentSide r n) n) (axisCubeConcentricDepthSide (stoppingComparisonParentSide r n) n) =ᵐ[MeasureTheory.volume] Metric.closedBall x (5 * r)

The depth-n comparison descendant and the closed stopping-scale ball agree almost everywhere.

def HCPolySupport.CubeCalderonZygmund.stoppingComparisonRadius (r : ℝ) (n : ℕ) : ℝ

The largest comparison radius required by the depth-n parent.

Equations

• HCPolySupport.CubeCalderonZygmund.stoppingComparisonRadius r n = 10 * 3 ^ n * r

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonRadius_eq_two_mul_parentRadius (r : ℝ) (n : ℕ) : stoppingComparisonRadius r n = 2 * (stoppingComparisonParentMultiplier n * r)

theorem HCPolySupport.CubeCalderonZygmund.le_stoppingComparisonRadius {r : ℝ} (hr : 0 ≤ r) (n : ℕ) : r ≤ stoppingComparisonRadius r n

A positive stopping radius is no larger than its comparison radius.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonRadius_le_of_le {r R : ℝ} (n : ℕ) (h : r ≤ R / (10 * 3 ^ n)) : stoppingComparisonRadius r n ≤ R

The stopping-scale cutoff ensures that the full comparison parent remains within the radius on which the last-exit bound is available.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonRadius_bounds_of_le {r R : ℝ} (hr : 0 ≤ r) (n : ℕ) (h : r ≤ R / (10 * 3 ^ n)) : r ≤ stoppingComparisonRadius r n ∧ stoppingComparisonRadius r n ≤ R

A stopping radius bounded by R / (10 * 3^n) can be used both at its own scale and at the comparison-parent scale before the last-exit radius R.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonParentRadius_mem_Icc_of_le {r R : ℝ} (hr : 0 ≤ r) (n : ℕ) (h : r ≤ R / (10 * 3 ^ n)) : stoppingComparisonParentMultiplier n * r ∈ Set.Icc r R

Under the conservative 10 * 3^n cutoff, the actual comparison-parent radius 5 * 3^n * r lies in the last-exit interval from r to R.