High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.PowerTailAtScale

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

theorem HCPolySupport.HighContrast.powerTail_goodTail_at_nat {d : ℕ} {a : Book.Ch02.TriadicCoeffFamily d} {s amplitude kappa x : ℝ} (hPower : ScalarIdentityPowerTail a s amplitude kappa x) (hAmplitude : 0 ≤ amplitude) (hKappa : 0 < kappa) {q : ℕ} (hxq : x ≤ 3 ^ q) (hx : 0 < x) : ScalarIdentityGoodTail a s (amplitude * (3 ^ q / x) ^ (-kappa) / (1 - 3 ^ (-kappa))) ↑q

A power tail can be restarted at any natural generation above its real reference scale, retaining the exact power price at that generation.

theorem HCPolySupport.HighContrast.canonical_restarted_tolerance_eq {c kappa x : ℝ} {q : ℕ} (hKappa : 0 < kappa) : correctorTargetAmplitude c kappa * (3 ^ q / x) ^ (-kappa) / (1 - 3 ^ (-kappa)) = c / 2 * (3 ^ q / x) ^ (-kappa)

At the canonical target amplitude, the restarted tolerance is exactly one half of the successor smallness times the physical power price.