Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.QuantitativeGoodTail

High-contrast homogenization: Provider.Regularity.QuantitativeGoodTail #

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

Quantitative weak-error tails #

This file records the pointwise power decay retained by the normalized reference certificate and proves its two basic operations: deterministic rebasing of the reference scale and projection to a summable good tail.

source
def HCPolySupport.HighContrast.ScalarIdentityPowerTail {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (s amplitude kappa x : ℝ) :
Prop

The scalar identity weak error decays with a fixed power above a real reference scale.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.ScalarIdentityPowerTail.mono_amplitude {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s amplitude amplitude' kappa x : ℝ} (h : ScalarIdentityPowerTail a s amplitude kappa x) (hAmplitude : amplitude ≤ amplitude') (hx : 0 < x) :
    ScalarIdentityPowerTail a s amplitude' kappa x

    Increasing the amplitude preserves a quantitative weak-error tail.

    source
    theorem HCPolySupport.HighContrast.ScalarIdentityPowerTail.rebase {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s amplitude kappa x y : ℝ} (h : ScalarIdentityPowerTail a s amplitude kappa x) (hx : 0 < x) (hy : 0 < y) (hxy : x ≤ y) :
    ScalarIdentityPowerTail a s (amplitude * (y / x) ^ (-kappa)) kappa y

    Rebasing to a larger positive scale divides the retained amplitude by the corresponding power, without changing the exponent or coefficient family.

    source
    theorem HCPolySupport.HighContrast.ScalarIdentityPowerTail.goodTail {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s amplitude kappa x : ℝ} (h : ScalarIdentityPowerTail a s amplitude kappa x) (hAmplitude : 0 ≤ amplitude) (hKappa : 0 < kappa) (hx : 1 ≤ x) :
    ScalarIdentityGoodTail a s (amplitude / (1 - 3 ^ (-kappa))) ↑(Quenched.triadicCeilingIndex x)

    A positive quantitative power tail is summable from the first triadic generation above its real reference scale.