Documentation

LeanPool.HighContrastHomogenization.Provider.Regularity.QuantitativeCorrectorThreshold

High-contrast homogenization: Provider.Regularity.QuantitativeCorrectorThreshold #

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

A quantitative certificate at the local-corrector threshold #

The small target amplitude is selected before coefficient samples. One common effective scale then places every quantitative certificate strictly below the joint-local-corrector threshold.

source
noncomputable def HCPolySupport.HighContrast.correctorTargetAmplitude (c kappa : ℝ) :
ℝ

Pointwise amplitude which makes the resulting summable-tail tolerance exactly c / 2.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.correctorTargetAmplitude_pos {c kappa : ℝ} (hc : 0 < c) (hKappa : 0 < kappa) :
    0 < correctorTargetAmplitude c kappa
    source
    theorem HCPolySupport.HighContrast.correctorTargetAmplitude_div {c kappa : ℝ} (hKappa : 0 < kappa) :
    correctorTargetAmplitude c kappa / (1 - 3 ^ (-kappa)) = c / 2