High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.ClosedBallGeometry

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

the large-scale C¹ slope approximation clause (b2), first step: the exact-root pullback set is a

closed Euclidean ball

ExactRootGaugeTerminal states its row on {y | vecNormSq y ≤ r ^ 2}, because that set is exactly the exact-root pullback of the ellipsoid (Root.matImage_normalizedRoot_inv_ellipsoid_eq), whereas the ball geometry is all stated for the open ball euclideanBall d r = {y | vecNormSq y < r ^ 2}.

The closed-ball analogue of volume_euclideanBall_ne_zero/_ne_top — volume {y | vecNormSq y ≤ r^2} ≠ 0, ≠ ⊤, the sphere being null — is the one measure fact of (b2) that is not already available.

It is not needed, and this module removes it. A null-sphere argument would be required only to prove the two volumes equal; every use in (b2) needs no more than the two-sided sandwich

euclideanBall d r  ⊆  closedNormBall d r  ⊆  euclideanBall d (2 * r)

which is elementary, together with the volume_euclideanBall_ne_zero / _ne_top and monotonicity of the measure. The cost is a factor 2 ^ d in the law-free constants — (6√d)^d rather than (3√d)^d on the inner side — and no measure theory beyond measure_mono.

Nothing here is an estimate: it is set inclusion and measure monotonicity.

def HCPolySupport.HighContrast.CorrectorComposition.closedNormBall (d : ℕ) (r : ℝ) : Set (Vec d)

The exact-root pullback of the ellipsoid. The closed Euclidean ball, in the literal shape ExactRootGaugeTerminal names it.

Equations

• HCPolySupport.HighContrast.CorrectorComposition.closedNormBall d r = {y : HCPolySupport.Vec d | HCPolySupport.vecNormSq y ≤ r ^ 2}

theorem HCPolySupport.HighContrast.CorrectorComposition.euclideanBall_subset_closedNormBall (d : ℕ) (r : ℝ) : euclideanBall d r ⊆ closedNormBall d r

The open ball sits inside the closed one.

theorem HCPolySupport.HighContrast.CorrectorComposition.closedNormBall_subset_euclideanBall_two_mul {d : ℕ} {r : ℝ} (hr : 0 < r) : closedNormBall d r ⊆ euclideanBall d (2 * r)

The closed ball sits inside the doubled open one. This is the step that replaces a null-sphere argument.

theorem HCPolySupport.HighContrast.CorrectorComposition.isBounded_closedNormBall (d : ℕ) (r : ℝ) : Bornology.IsBounded (closedNormBall d r)

The closed ball is bounded.

The two measure facts, with no null-sphere argument

theorem HCPolySupport.HighContrast.CorrectorComposition.volume_closedNormBall_ne_zero {d : ℕ} {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (closedNormBall d r) ≠ 0

theorem HCPolySupport.HighContrast.CorrectorComposition.volume_closedNormBall_ne_top {d : ℕ} {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (closedNormBall d r) ≠ ⊤

The exact-root pullback identification, restated at closedNormBall

theorem HCPolySupport.HighContrast.CorrectorComposition.matImage_normalizedRoot_inv_ellipsoid_eq_closedNormBall {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (r : ℝ) : matImage (Selection.normalizedRoot (symmPart abar))⁻¹ (ellipsoid abar r) = closedNormBall d r

The exact-root pullback of the ellipsoid is the closed Euclidean ball. Restatement of the pullback identity in this module's vocabulary, so the two volume comparisons below can be read directly against ExactRootGaugeTerminal.

The two volume comparisons of (b2), in structural form

theorem HCPolySupport.HighContrast.CorrectorComposition.weightedGradNorm_closedNormBall_le_cube {d : ℕ} {r : ℝ} (hr : 0 < r) {m : ℤ} (hcube : closedNormBall d r ⊆ openCubeSet (originCube d m)) (hczero : MeasureTheory.volume (openCubeSet (originCube d m)) ≠ 0) (hctop : MeasureTheory.volume (openCubeSet (originCube d m)) ≠ ⊤) (b : CoeffField d) (F : Vec d → Vec d) : weightedGradNorm b (closedNormBall d r) F ≤ (MeasureTheory.volume (openCubeSet (originCube d m)) / MeasureTheory.volume (closedNormBall d r)) ^ (1 / 2) * weightedGradNorm b (openCubeSet (originCube d m)) F

(b2), inner side. The energy on the closed ball of radius r is controlled by the energy on any triadic cube containing it, at the price of the volume ratio — and the closed ball's two measure facts are the ones proved above, with no null-sphere argument.

theorem HCPolySupport.HighContrast.CorrectorComposition.weightedGradNorm_cube_le_closedNormBall {d : ℕ} {R : ℝ} (hR : 0 < R) {m : ℤ} (hcube : openCubeSet (originCube d m) ⊆ closedNormBall d R) (hczero : MeasureTheory.volume (openCubeSet (originCube d m)) ≠ 0) (hctop : MeasureTheory.volume (openCubeSet (originCube d m)) ≠ ⊤) (b : CoeffField d) (F : Vec d → Vec d) : weightedGradNorm b (openCubeSet (originCube d m)) F ≤ (MeasureTheory.volume (closedNormBall d R) / MeasureTheory.volume (openCubeSet (originCube d m))) ^ (1 / 2) * weightedGradNorm b (closedNormBall d R) F

(b2), outer side. The energy on a triadic cube contained in the closed ball of radius R is controlled by the energy on that ball.

The two inclusions, at explicit generations

theorem HCPolySupport.HighContrast.CorrectorComposition.closedNormBall_subset_outerCube {d : ℕ} {r : ℝ} (hr : 0 < r) : closedNormBall d r ⊆ openCubeSet (originCube d (outerTriadicGeneration (2 * (2 * r)) ⋯))

The closed ball of radius r lies in the triadic cube canonically enclosing the open ball of radius 2 r, i.e. the one at radius 2 * (2 * r) = 4 r. (The radius is left in the 2 * (2 * r) form the inclusion produces; the generation congruence converts it to 4 * r wherever a consumer prefers that shape.)

theorem HCPolySupport.HighContrast.CorrectorComposition.openCubeSet_originCube_subset_closedNormBall {d : ℕ} [NeZero d] {R : ℝ} (q : ℕ) (hq : √↑d * 3 ^ q ≤ R) : openCubeSet (originCube d ↑q) ⊆ closedNormBall d R

A triadic cube whose scale-matched ball has radius at most R lies in the closed ball of radius R.