Documentation

LeanPool.HighContrastHomogenization.Provider.Quenched.SmallContrastRowValueIsotropy

High-contrast homogenization: Provider.Quenched.SmallContrastRowValueIsotropy #

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

The isotropy row value and coefficient #

The unparametrized row value and row coefficient contain boundaryConst Cd g mAl · 3^{g((t+G)-s)}, so no bound against them is independent of Π. The definitions here instead carry the row constant as an abstract scalar cRow:

rowCoefficientIsotropy d cRow kap = cRow · (kap · 36(1+d))
rowValue2Isotropy     d cRow kap eps = cRow · (kap · 36(1+d)·eps²)

Neither mentions Cd, g, mAl or G, so neither can carry Π; the aspect-ratio obligation moves to the caller, who must supply a cRow the row cap proves. rowSplitConstant combines a Π-independent head with a deep-leg term that tends to zero beyond the threshold.

Two simplifications follow. The original coefficient needs a congruence lemma (the row coefficient must be shown to depend on the window only through its height) at the fusion's hrowEq step; rowCoefficientIsotropy does not mention the window at all, so that step disappears. The definition quadCoefficient is already abstract in the row coefficient and is reused directly.

The scalar-parametrized pair #

source
def HCPolySupport.HighContrast.Quenched.rowCoefficientIsotropy (d : ℕ) (cRow kap : ℝ) :
ℝ

The isotropy row coefficient. The parallel definition beside rowCoefficient, with the row's constant abstract.

Equations
Instances For
    source
    def HCPolySupport.HighContrast.Quenched.rowValue2Isotropy (d : ℕ) (cRow kap eps : ℝ) :
    ℝ

    The isotropy row value. The parallel definition beside the unparametrized one.

    Equations
    Instances For
      source
      theorem HCPolySupport.HighContrast.Quenched.rowValue2Isotropy_eq_coefficient (d : ℕ) (cRow kap eps : ℝ) :
      rowValue2Isotropy d cRow kap eps = rowCoefficientIsotropy d cRow kap * eps ^ 2

      The isotropy analogue of the row-value equation. This is the equation the one-step chain consumes.

      source
      theorem HCPolySupport.HighContrast.Quenched.rowCoefficientIsotropy_nonneg {d : ℕ} {cRow kap : ℝ} (hcRow : 0 ≤ cRow) (hkap : 0 ≤ kap) :
      0 ≤ rowCoefficientIsotropy d cRow kap

      The value the split row cap proves #

      source
      noncomputable def HCPolySupport.HighContrast.Quenched.rowSplitConstant (cIso cDeep : ℝ) :
      ℝ

      The split row cap's constant: a Π-free head at ratio 3^{-3/2}, plus the deep leg, which the caller's threshold drives below any prescribed tolerance.

      Equations
      Instances For
        source
        theorem HCPolySupport.HighContrast.Quenched.one_le_row_head_geometric :
        1 ≤ 1 / (1 - 3 ^ (-(3 / 2)))
        source
        theorem HCPolySupport.HighContrast.Quenched.rowSplitConstant_nonneg {cIso cDeep : ℝ} (hcIso : 0 ≤ cIso) (hcDeep : 0 ≤ cDeep) :
        0 ≤ rowSplitConstant cIso cDeep