High-contrast homogenization: Provider.Regularity.SmallTailIteration

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

theorem HCPolySupport.HighContrast.smallTail_interval_bound {n m : ℤ} (C : ℝ) (D E : ℤ → ℝ) (hnm : n ≤ m) (hC : 1 ≤ C) (hD : ∀ j ∈ Finset.Icc n m, 0 ≤ D j) (hE : ∀ j ∈ Finset.Icc n m, 0 ≤ E j) (hrec : ∀ h ∈ Finset.Icc n m, D h ≤ C * D m + C * ∑ j ∈ Finset.Ioc h m, E j * D j) (hsmall : ∑ j ∈ Finset.Icc n m, E j ≤ (2 * C)⁻¹) (h : ℤ) : h ∈ Finset.Icc n m → D h ≤ 2 * C * D m

A nonnegative recurrence with a sufficiently small accumulated tail is uniformly controlled by its terminal value.