Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.RoundedEllipsoidTriadicGeometry

High-contrast homogenization: Provider.Regularity.RoundedEllipsoidTriadicGeometry #

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

Rounded-coordinate ellipsoid and triadic endpoint geometry #

The R3-A rounded map sends every physical adapted ellipsoid to the quadratic sublevel set of the inverse rounded reference matrix. The literal 99/100--101/100 ellipticity window then gives dimension-only inner and outer Euclidean comparisons. These are the geometric endpoint facts used by the Lane-C real-radius consumer.

source
noncomputable def HCPolySupport.HighContrast.roundedEllipsoidOuterGeneration (r : ℝ) (hr : 0 < r) :
ℤ

The canonical rounded outer generation for a positive physical radius.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.outerTriadicGeneration_mono {R T : ℝ} (hR : 0 < R) (hT : 0 < T) (hRT : R ≤ T) :
    outerTriadicGeneration R hR ≤ outerTriadicGeneration T hT

    Canonical outer generations are monotone in their positive side length.

    source
    noncomputable def HCPolySupport.HighContrast.roundedEllipsoidTerminalGeneration {d : ℕ} [NeZero d] (R : ℝ) (hR : 0 < R) :
    ℤ

    A deliberately interior terminal generation. Its cube is uniformly inside the rounded pullback at radius R; the factor 100*d is geometric slack only and is not inserted into the common effective scale.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.roundedEllipsoidOuterGeneration_le_terminalGeneration {d : ℕ} [NeZero d] {r R : ℝ} (hr : 0 < r) (hR : 0 < R) (hsmall : r ≤ R / (400 * ↑d)) :
      roundedEllipsoidOuterGeneration r hr ≤ roundedEllipsoidTerminalGeneration R hR

      In the small-radius branch, including its equality endpoint, the rounded query generation does not exceed the interior terminal generation.

      source
      theorem HCPolySupport.HighContrast.triadicCeilingIndex_cast_le_roundedEllipsoidOuterGeneration {x r : ℝ} (hx : 1 ≤ x) (hxr : x ≤ r) :
      ↑(Quenched.triadicCeilingIndex x) ≤ roundedEllipsoidOuterGeneration r ⋯

      At the minimal admitted real radius, and hence at every later radius, the rounded outer generation lies above the natural triadic ceiling of the common scale.