High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorComposition.ClosedBallVolumeRatio

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

the large-scale C¹ slope approximation clause (b2), second step: the two volume ratios are

law-free constants

weightedGradNorm_mono_set_le_volumeRatio pays (volume V / volume U) ^ (1/2) for a domain change. For (b2) that ratio must be bounded by a constant depending on d alone — otherwise the decay (r/R)^η the cube row supplies would be eaten by the geometry. Both bounds are proved here, from ingredients:

• inner side, outerTriadicGeneration_volume_ratio_lt_euclideanBall at radius 2 r plus the exact doubling volume_euclideanBall_two_mul, giving (3√d)^d · 2^d = (6√d)^d;
• outer side, scaleMatchedEuclideanBall_volume_ratio_le plus the exact dilation volume_euclideanBall_eq_ofReal_pow_mul, giving 6^d · (2√d)^d = (12√d)^d.

Neither uses an estimate, a law, a sample or a scale: they are volumes of explicit sets.

Inner side

theorem HCPolySupport.HighContrast.CorrectorComposition.outerCube_closedNormBall_volume_ratio_le {d : ℕ} [NeZero d] {r : ℝ} (hr : 0 < r) : MeasureTheory.volume (openCubeSet (originCube d (outerTriadicGeneration (2 * (2 * r)) ⋯))) / MeasureTheory.volume (closedNormBall d r) ≤ ENNReal.ofReal ((6 * √↑d) ^ d)

The inner volume ratio is law-free. The canonical triadic cube enclosing the closed ball of radius r has volume at most (6√d)^d times the ball's.

Outer side

theorem HCPolySupport.HighContrast.CorrectorComposition.volume_euclideanBall_const_mul {d : ℕ} {c x : ℝ} (hc : 0 < c) (hx : 0 < x) : MeasureTheory.volume (euclideanBall d (c * x)) = ENNReal.ofReal (c ^ d) * MeasureTheory.volume (euclideanBall d x)

The exact dilation of the ball volume by a positive factor.

theorem HCPolySupport.HighContrast.CorrectorComposition.closedNormBall_cube_volume_ratio_le {d : ℕ} [NeZero d] {R : ℝ} (q : ℕ) (hq : √↑d * 3 ^ q ≤ R) (hqmax : R < 3 * (√↑d * 3 ^ q)) : MeasureTheory.volume (closedNormBall d R) / MeasureTheory.volume (openCubeSet (originCube d ↑q)) ≤ ENNReal.ofReal ((12 * √↑d) ^ d)

The outer volume ratio is law-free. If the scale-matched ball of the triadic cube at generation q has radius between R / 3 and R, the closed ball of radius R has volume at most (12√d)^d times the cube's.