High-contrast homogenization: Provider.PolynomialHomogenization.Root.Dirichlet.ActivationFold

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

The activation length folded into the eccentricity factor

The certificate's activation length is a triadic power of the formulaic tail shift; the shift is a logarithm of the absorption prefactor; and the prefactor carries the homogenized matrix only through the triadic bracket of its witness eccentricity, at the row order. Composing those three facts writes any fixed nonnegative power of the activation length as a law-free constant times the eccentricity fold factor raised to the rate — which is exactly what the folded homogenization length pays for.

The exponent of the fold factor is rho * c / (2 kappa^2), with rho the row order, c the power of the activation length being folded and kappa the rate: law-free, as the frozen polynomial-length clause requires.

The fold factor as a power of the truncated eccentricity

theorem HCPolySupport.HighContrast.RowSupply.eccentricityFoldFactor_eq_max_rpow {d : ℕ} (abar : Mat d) {p : ℝ} (hp : 0 ≤ p) : eccentricityFoldFactor abar p = max 1 (witnessEccentricity (symmPart abar)) ^ p

The fold factor is the truncated eccentricity raised to its exponent.

The law-free prefactor

noncomputable def HCPolySupport.HighContrast.RowSupply.foldPrefactorBase (d : ℕ) (g kappaRate : ℝ) : ℝ

The law-free part of the absorption prefactor, at the root the fold takes.

Equations

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

noncomputable def HCPolySupport.HighContrast.RowSupply.activationFoldConstant (d : ℕ) (g kappaRate c : ℝ) : ℝ

The law-free constant multiplying the folded activation power.

Equations

• HCPolySupport.HighContrast.RowSupply.activationFoldConstant d g kappaRate c = (3 * max 1 (HCPolySupport.HighContrast.RowSupply.foldPrefactorBase d g kappaRate)) ^ c

The fold

theorem HCPolySupport.HighContrast.RowSupply.rpow_activation_le_foldFactor {d : ℕ} {abar : Mat d} {g kappaRate c : ℝ} {G L : ℕ} (hkappa : 0 < kappaRate) (hc : 0 ≤ c) (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)) : (3 ^ ↑L) ^ c ≤ activationFoldConstant d g kappaRate c * eccentricityFoldFactor abar (Certificate.printRowOrder g * c / (2 * kappaRate * kappaRate)) ^ kappaRate

The activation power folds. Any nonnegative power of the certificate's activation length is a law-free constant times the eccentricity fold factor raised to the rate.