High-contrast homogenization: Provider.Regularity.CorrectorRealRadiusBallGeometry

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

Euclidean-ball geometry at a real radius

The frozen Liouville class is normalized on Euclidean balls, whereas the corrector estimates are normalized on centered triadic cubes. This module provides both inclusions and a dimension-only volume-ratio bound.

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

A Euclidean ball of radius r lies in the centered open cube of side length 2r.

theorem HCPolySupport.HighContrast.centeredOpenCube_two_mul_div_sqrt_subset_euclideanBall {d : ℕ} [NeZero d] {r : ℝ} (hr : 0 < r) : centeredOpenCube d (2 * (r / √↑d)) ⊆ euclideanBall d r

The centered sup-norm cube with half-side r / √d lies in the Euclidean ball of radius r.

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

The Euclidean ball is enclosed by the canonical origin-centered triadic cube chosen from side length 2r.

theorem HCPolySupport.HighContrast.two_mul_div_sqrt_pow_le_volume_euclideanBall_toReal {d : ℕ} [NeZero d] {r : ℝ} (hr : 0 < r) : (2 * (r / √↑d)) ^ d ≤ (MeasureTheory.volume (euclideanBall d r)).toReal

The explicit inner centered cube gives a positive dimension-only lower bound for the real volume of a Euclidean ball.

theorem HCPolySupport.HighContrast.outerTriadicGeneration_volume_ratio_lt_euclideanBall {d : ℕ} [NeZero d] {r : ℝ} (hr : 0 < r) : (MeasureTheory.volume (openCubeSet (originCube d (outerTriadicGeneration (2 * r) ⋯)))).toReal / (MeasureTheory.volume (euclideanBall d r)).toReal < (3 * √↑d) ^ d

The canonical enclosing triadic cube has at most a dimension-only real volume ratio over the Euclidean ball.