High-contrast homogenization: Provider.Quenched.SmallContrastOffsetDecayToOrigin

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

The offset decay read from the origin

The offset iteration concludes at (n - ns) in the exponent; the endpoint's outer composition reads a decay at n. The two differ by one factor 3 ^ (gam · ns), and below the offset the antitone sequence is bounded by its own initial value, which the same factor covers.

So the passage is an absorption, not an estimate: the shift moves into the prefactor, and the prefactor is where the endpoint already carries a polynomially bounded quantity.

theorem HCPolySupport.HighContrast.Quenched.three_rpow_neg_pow_eq (gam : ℝ) (k : ℕ) : (3 ^ (-gam)) ^ k = 3 ^ (-gam * ↑k)

The natural-power form of the geometric factor is its real power.

theorem HCPolySupport.HighContrast.Quenched.hatted_decay_of_offset_decay {F : ℕ → ℝ} {Kpre gam : ℝ} {ns : ℕ} (hgam0 : 0 < gam) (hKpre0 : 0 ≤ Kpre) (hFnn : ∀ (n : ℕ), 0 ≤ F n) (hFmono : ∀ (m n : ℕ), m ≤ n → F n ≤ F m) (hoff : ∀ (n : ℕ), ns ≤ n → F n ≤ Kpre * (3 ^ (-gam)) ^ (n - ns)) (n : ℕ) : F n ≤ (Kpre + F 0) * 3 ^ (gam * ↑ns) * 3 ^ (-gam * ↑n)

The offset decay, read from the origin. The offset joins the prefactor.