High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.ClosedBallNearRatio

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

The near-terminal ball comparison

The large-scale C¹ slope approximation's ball terminal necessarily has a band on which the cube row is silent: the canonical outer cube of r overshoots every triadic cube contained in the ball of radius R as soon as 108 * (√d * r) > R, and — since 2 ≤ d — that band always contains r = R.

On that band the only available comparison is ball against ball, with a law-free volume ratio. This module supplies it, in the same style as ClosedBallVolumeRatio: the closed ball of radius R sits inside the open ball of radius 216 √d · r, whose volume is (216 √d) ^ d times the open ball of radius r, which the closed ball of radius r contains.

Nothing here is an estimate.

theorem HCPolySupport.HighContrast.CorrectorComposition.closedNormBall_mono {d : ℕ} {r R : ℝ} (hr : 0 ≤ r) (hrR : r ≤ R) : closedNormBall d r ⊆ closedNormBall d R

The closed balls are monotone in the radius.

theorem HCPolySupport.HighContrast.CorrectorComposition.closedNormBall_volume_ratio_le_of_near {d : ℕ} [NeZero d] {r R : ℝ} (hr : 0 < r) (hR : 0 < R) (hnear : R < 108 * (√↑d * r)) : MeasureTheory.volume (closedNormBall d R) / MeasureTheory.volume (closedNormBall d r) ≤ ENNReal.ofReal ((216 * √↑d) ^ d)

The near-terminal ball volume ratio is law-free.

theorem HCPolySupport.HighContrast.CorrectorComposition.weightedGradNorm_closedNormBall_le_of_near {d : ℕ} [NeZero d] {r R : ℝ} (hr : 0 < r) (hR : 0 < R) (hrR : r ≤ R) (hnear : R < 108 * (√↑d * r)) (b : CoeffField d) (F : Vec d → Vec d) : weightedGradNorm b (closedNormBall d r) F ≤ ENNReal.ofReal ((216 * √↑d) ^ d) ^ (1 / 2) * weightedGradNorm b (closedNormBall d R) F

The near-terminal energy comparison.