Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.GoodMax

High-contrast homogenization: Provider.Regularity.GoodMax #

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

Uniform weak-error bounds on finite scale intervals #

This module records the pointwise maximum-row event for the scalar identity comparison on centered cubes and its elementary relation to the summable finite-tail event.

source
def HCPolySupport.HighContrast.ScalarIdentityGoodMaxOnInterval {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (s δ : ℝ) (n m : ℤ) :
Prop

Every scalar identity weak error on the integer interval [n,m] is at most δ.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.ScalarIdentityGoodMaxOnInterval.weakError_le {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ : ℝ} {n m k : ℤ} (h : ScalarIdentityGoodMaxOnInterval a s δ n m) (hk : k ∈ Finset.Icc n m) :
    scalarIdentityWeakError a s k ≤ δ

    Extract the pointwise weak-error bound from a finite good-max row.

    source
    theorem HCPolySupport.HighContrast.ScalarIdentityGoodMaxOnInterval.mono {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ δ' : ℝ} {n m : ℤ} (h : ScalarIdentityGoodMaxOnInterval a s δ n m) (δh : δ ≤ δ') :
    ScalarIdentityGoodMaxOnInterval a s δ' n m

    Increasing the tolerance preserves a finite good-max row.

    source
    theorem HCPolySupport.HighContrast.ScalarIdentityGoodMaxOnInterval.mono_interval {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ : ℝ} {n n' m' m : ℤ} (h : ScalarIdentityGoodMaxOnInterval a s δ n m) (hn : n ≤ n') (hm : m' ≤ m) :
    ScalarIdentityGoodMaxOnInterval a s δ n' m'

    Restricting the scale interval preserves a finite good-max row.

    source
    theorem HCPolySupport.HighContrast.ScalarIdentityGoodTailOnInterval.toGoodMax {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ : ℝ} {n m : ℤ} (h : ScalarIdentityGoodTailOnInterval a s δ n m) :
    ScalarIdentityGoodMaxOnInterval a s δ n m

    A summable finite weak-error row controls the pointwise maximum row at the same tolerance.

    source
    theorem HCPolySupport.HighContrast.ScalarIdentityGoodTail.goodMaxOnInterval {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s δ : ℝ} {n m : ℤ} (h : ScalarIdentityGoodTail a s δ n) (hnm : n ≤ m) :
    ScalarIdentityGoodMaxOnInterval a s δ n m

    An infinite summable tail controls the finite good-max row on every admissible terminal interval.