High-contrast homogenization: Provider.Regularity.LiouvilleOriginCubeBallBridge

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

Comparing origin cubes with scale-matched Euclidean balls

The radius sqrt d * 3^q encloses the origin cube Q_q, with a dimension-only normalized-volume loss. This is the geometric bridge needed to feed the frozen continuous-radius Liouville limit into finite Caccioppoli.

theorem HCPolySupport.HighContrast.openCubeSet_originCube_subset_scaleMatchedEuclideanBall {d : ℕ} [NeZero d] (q : ℕ) : openCubeSet (originCube d ↑q) ⊆ euclideanBall d (√↑d * 3 ^ q)

The origin cube at natural generation q lies in the centered Euclidean ball of radius sqrt d * 3^q.

theorem HCPolySupport.HighContrast.scaleMatchedEuclideanBall_volume_ratio_le {d : ℕ} [NeZero d] (q : ℕ) : MeasureTheory.volume (euclideanBall d (√↑d * 3 ^ q)) / MeasureTheory.volume (openCubeSet (originCube d ↑q)) ≤ ENNReal.ofReal ((2 * √↑d) ^ d)

The scale-matched ball-to-cube volume ratio is bounded by the volume of a dimension-only centered cube.

theorem HCPolySupport.HighContrast.normalizedL2Norm_originCube_le_scaleMatchedEuclideanBall {d : ℕ} [NeZero d] (q : ℕ) (v : Vec d → ℝ) : normalizedL2Norm (openCubeSet (originCube d ↑q)) v ≤ ENNReal.ofReal ((2 * √↑d) ^ d) ^ (1 / 2) * normalizedL2Norm (euclideanBall d (√↑d * 3 ^ q)) v

The normalized L² norm on an origin cube is controlled by the frozen norm on its scale-matched enclosing ball with a dimension-only ENNReal factor.

theorem HCPolySupport.HighContrast.tendsto_scaleMatchedRadius_normalizedL2Norm_originCube_of_liouvilleGrowth {d : ℕ} [NeZero d] {theta : ℝ} {v : Vec d → ℝ} (hgrowth : Filter.Tendsto (fun (r : ℝ) => ENNReal.ofReal (r ^ (-(1 + theta))) * normalizedL2Norm (euclideanBall d r) v) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (q : ℕ) => ENNReal.ofReal ((√↑d * 3 ^ q) ^ (-(1 + theta))) * normalizedL2Norm (openCubeSet (originCube d ↑q)) v) Filter.atTop (nhds 0)

Along natural triadic generations, the scale-matched frozen prefactor times the normalized cube norm tends to zero.

theorem HCPolySupport.HighContrast.tendsto_scaleMatchedRadius_zeroAffineError_of_liouvilleGrowth {d : ℕ} [NeZero d] {theta : ℝ} {v : Vec d → ℝ} (hmem : ∀ (q : ℕ), MeasureTheory.MemLp v 2 (normalizedCubeMeasure (originCube d ↑q))) (hgrowth : Filter.Tendsto (fun (r : ℝ) => ENNReal.ofReal (r ^ (-(1 + theta))) * normalizedL2Norm (euclideanBall d r) v) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (q : ℕ) => ENNReal.ofReal ((√↑d * 3 ^ q) ^ (-theta) * normalizedAffineCandidateError (originCube d ↑q) v 0 0)) Filter.atTop (nhds 0)

With local L² membership available, the preceding frozen-norm limit is exactly the o(R^theta) statement for the scale-normalized zero-affine candidate error used by finite Caccioppoli.

theorem HCPolySupport.HighContrast.tendsto_scaleMatchedRadius_zeroAffineError_of_memLiouvilleClass {d : ℕ} [NeZero d] {b : CoeffField d} {theta : ℝ} {v : Vec d → ℝ} {Dv : Vec d → Vec d} (hv : MemLiouvilleClass b theta v Dv) : Filter.Tendsto (fun (q : ℕ) => ENNReal.ofReal ((√↑d * 3 ^ q) ^ (-theta) * normalizedAffineCandidateError (originCube d ↑q) v 0 0)) Filter.atTop (nhds 0)

The Liouville-growth input in frozen-class form: a Liouville member has scale-normalized zero-affine error o(R^theta) along the triadic radii.