High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.CorrectorDecay.IdentityFiniteEnergy
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.finiteCenteredEnergy_le_of_identityGoodTail
{d : ℕ}
{s : ℝ}
{a : Book.Ch03.CoeffFamily d}
{C : ℝ}
(hC : 1 ≤ C)
{n m : ℤ}
(hnm : n ≤ m)
(u : Book.Ch03.CubeSolution (originCube d m) a)
(hrecurrence :
∀ q ∈ Finset.Icc n m,
finiteCenteredCubeSolutionEnergy a m u q ≤ C * finiteCenteredCubeSolutionEnergy a m u m + C * ∑ j ∈ Finset.Ioc q m, scalarIdentityWeakError a s j * finiteCenteredCubeSolutionEnergy a m u j)
(hTail : ScalarIdentityGoodTailOnInterval a s (2 * C)⁻¹ n m)
(q : ℤ)
:
q ∈ Finset.Icc n m → finiteCenteredCubeSolutionEnergy a m u q ≤ 2 * C * finiteCenteredCubeSolutionEnergy a m u m
The exact-identity finite recurrence closes under the same summable-tail budget as the available rounded recurrence.