High-contrast homogenization: Provider.Regularity.CorrectorRealRadiusGeometry

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

Real-radius centered-cube geometry

This module compares a centered Euclidean cube of arbitrary positive side length with its canonical enclosing origin-centered triadic cube. The enclosing generation is the integer ceiling of the base-three logarithm, so the construction uses no selected cube or fallback branch.

Main definitions

• centeredOpenCube: the centered open axis cube of the given side length.
• outerTriadicGeneration: the canonical enclosing triadic generation.

Main results

• le_outerTriadicGeneration_scale and its strict companion: the sharp ceiling bounds.
• outerTriadicGeneration_scale_lt_three_mul: the factor-three rounding bound.
• centeredOpenCube_subset_openCubeSet_originCube_outerTriadicGeneration: the exact centered-cube inclusion.
• outerTriadicGeneration_volume_ratio_lt_euclideanBall: the strict dimensional volume ratio bound.

def HCPolySupport.HighContrast.centeredOpenCube (d : ℕ) (R : ℝ) : Set (Vec d)

The centered open axis cube of side length R.

Equations

• HCPolySupport.HighContrast.centeredOpenCube d R = HCPolySupport.axisCube (fun (x : Fin d) => -R / 2) R

noncomputable def HCPolySupport.HighContrast.outerTriadicGeneration (R : ℝ) (_hR : 0 < R) : ℤ

The canonical origin-cube generation enclosing a positive real side length. The positivity proof is retained in the interface and does not affect the value.

Equations

• HCPolySupport.HighContrast.outerTriadicGeneration R _hR = ⌈Real.logb 3 R⌉

theorem HCPolySupport.HighContrast.le_outerTriadicGeneration_scale {R : ℝ} (hR : 0 < R) : R ≤ 3 ^ outerTriadicGeneration R hR

The real side length does not exceed its canonical enclosing triadic scale.

theorem HCPolySupport.HighContrast.outerTriadicGeneration_scale_lt_three_mul {R : ℝ} (hR : 0 < R) : 3 ^ outerTriadicGeneration R hR < 3 * R

The canonical enclosing triadic side loses strictly less than one factor of three.

theorem HCPolySupport.HighContrast.centeredOpenCube_subset_openCubeSet_originCube_outerTriadicGeneration {d : ℕ} {R : ℝ} (hR : 0 < R) : centeredOpenCube d R ⊆ openCubeSet (originCube d (outerTriadicGeneration R hR))

The centered real-side cube lies in the origin-centered triadic cube at the canonical outer generation.

theorem HCPolySupport.HighContrast.volume_centeredOpenCube_toReal {d : ℕ} {R : ℝ} (hR : 0 < R) : (MeasureTheory.volume (centeredOpenCube d R)).toReal = R ^ d

The volume of a positive-side centered open cube is the side length to the ambient dimension.