High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.Corrector.LiouvillePrivateThresholdRestart
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Private restart for Liouville thresholds #
A summable weak-error row may be restarted after a finite prefix with any prescribed positive tolerance. Consequently the threshold selected by the deterministic Liouville terminal remains private to the exposed growth order.
theorem
HCPolySupport.HighContrast.Root.ScalarIdentityGoodTail.exists_restart_at_tolerance
{d : ℕ}
{a : Book.Ch02.TriadicCoeffFamily d}
{s delta : ℝ}
{n : ℤ}
(hgood : ScalarIdentityGoodTail a s delta n)
{target : ℝ}
(htarget : 0 < target)
:
∃ (n' : ℤ), n ≤ n' ∧ ScalarIdentityGoodTail a s target n'
A summable scalar good tail can be restarted with any positive tolerance. The coefficient family and fractional order are unchanged.