High-contrast homogenization: Provider.PolynomialHomogenization.RootInterface.SmallnessMonotone

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

The rate-bearing certificate is increasing in the corrector smallness

PrintOrderRateBearingCommonAffineGoodScale d g c κ abar a x pins its scale by

x = commonQuantitativeAffineScale sourceAmplitude (correctorTargetAmplitude c κ)
      κ Caff overlinePi κ X a  =  M(c) · X a

and M(c) is decreasing in c, because the corrector target amplitude (c/2) · (1 - 3^(-κ)) is increasing in c and the amplitude reduction factor max 1 (sourceAmplitude / target) is decreasing in the target. Combined with the certificate's upward closure in the scale, the predicate is therefore increasing in c at a fixed scale: a certificate at a smaller corrector smallness serves every larger one.

This is the fact the decay and Lipschitz adapters need: they demand the certificate at their own chosen c (canonicalCorrectorSmallness d g hg and (2 * Crec)⁻¹ respectively), while the root instantiation fixes one c for all five deterministic holes.

theorem HCPolySupport.HighContrast.RootInterface.correctorTargetAmplitude_mono {c c' kappa : ℝ} (hkappa : 0 < kappa) (hcc : c ≤ c') : correctorTargetAmplitude c kappa ≤ correctorTargetAmplitude c' kappa

The corrector target amplitude is increasing in the smallness parameter.

theorem HCPolySupport.HighContrast.RootInterface.PrintOrderRateBearingCommonAffineGoodScale.mono_smallness {d : ℕ} [NeZero d] {g c c' kappaRate x : ℝ} {abar : Mat d} {a : CoeffSpace d} (h : PrintOrderRateBearingCommonAffineGoodScale d g c kappaRate abar a x) (hkappa : 0 < kappaRate) (hc : 0 < c) (hcc : c ≤ c') : PrintOrderRateBearingCommonAffineGoodScale d g c' kappaRate abar a x

The rate-bearing certificate is increasing in the corrector smallness.