High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.WitnessErrorEccentricityBound

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

The witness observation error, bounded by an eccentricity power

The energy module's residue is: with Cwit selected before every law binder,

Book.Ch02.HomogenizationErrorOnCube (originCube d j) s .infinity (.finite 2)
  aFam (1 : Mat d) ≤ Cwit

and its λ-route bounds the left side by

√( max 1 (54 d² Rad) · geometricDiscount (1 − 2r) 1 ⁻¹ )
  · 3 ^ ((r − κ) M − r j + κ L) · √δ'

with r = responseWindowOrder g. The first factor is law-free and proved in that module. The other two are what the rate leg pays for by the printed fold of the response order, and the energy leg has no rate factor to absorb them into — which is where that module stopped.

This module supplies the missing law-level bound: the parent-gap power together with the certificate amplitude is below a law-free constant times a fixed power of the witness eccentricity. It is exactly the leak quantification of this module, generalised from the anchored provider's particular parent generation M = max (max L (J+1)) 1 to any M with 1 ≤ M ≤ L + J + 2, which is the form the energy route's parent selection produces.

The exponent is q = printRowOrder g · max (responseWindowOrder g) kappaRate / (2 kappaRate), a function of (g, kappaRate) only.

The frame exponent fold at a general parent generation

theorem HCPolySupport.HighContrast.RowSupply.rpow_three_frameExponent_le_fold_of_bounds {d : ℕ} {abar : Mat d} {g kappaRate : ℝ} {G L J : ℕ} {M : ℤ} (hkappa : 0 < kappaRate) (hrho : 0 ≤ Certificate.printRowOrder g) (hgeom : 0 < 1 - 3 ^ (-(2 * responseWindowOrder g - Certificate.printRowOrder g))) (hP : 0 < Certificate.shiftedTailAbsorptionPrefactor d (responseWindowOrder g) (Certificate.printRowOrder g) G) (hLeq : L = Certificate.formulaicNormalizedReferenceTailShift d (responseWindowOrder g) (Certificate.printRowOrder g) (2 * kappaRate) G) (hGupper : 3 ^ ↑G ≤ 1 + 3 * (witnessEccentricity (symmPart abar) * √↑d)) (hM1 : 1 ≤ M) (hMle : M ≤ ↑L + ↑J + 2) : 3 ^ ((responseWindowOrder g - kappaRate) * ↑M + kappaRate * ↑L) ≤ frameFoldConstant d g kappaRate ↑J * eccentricityFoldFactor abar (Certificate.printRowOrder g * max (responseWindowOrder g) kappaRate / (2 * kappaRate * kappaRate)) ^ kappaRate

The frame exponent folds at any admissible parent generation. This is HCPoly.Provider.PolynomialHomogenization.Root.Dirichlet.FrameExponentFold's theorem with the anchored provider's explicit M = max (max L (J+1)) 1 replaced by the two inequalities it was used through, so that the energy route's own parent selection qualifies.

The eccentricity exponent of the witness error

noncomputable def HCPolySupport.HighContrast.RowSupply.witnessErrorEccentricityExponent (g kappaRate : ℝ) : ℝ

The law-free exponent of the witness eccentricity in the energy leg's constant: the fold exponent multiplied by the rate.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.RowSupply.foldedFrameEccentricityExponent_nonneg_of_orders {g kappaRate : ℝ} (hkappa : 0 < kappaRate) (hrho : 0 ≤ Certificate.printRowOrder g) : 0 ≤ foldedFrameEccentricityExponent g kappaRate

theorem HCPolySupport.HighContrast.RowSupply.eccentricityFoldFactor_rpow_eq_witnessPow {d : ℕ} (abar : Mat d) {g kappaRate : ℝ} (hkappa : 0 < kappaRate) (hrho : 0 ≤ Certificate.printRowOrder g) : eccentricityFoldFactor abar (foldedFrameEccentricityExponent g kappaRate) ^ kappaRate = max 1 (witnessEccentricity (symmPart abar)) ^ witnessErrorEccentricityExponent g kappaRate

The folded factor raised to the rate is a single power of the truncated witness eccentricity, at the law-free exponent above.

The witness error bound