Coarse-graining support:

Support.Book.Ch05.Theorems.Section56.SmallContrastAlgebraicDecay.Iteration

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

The pure algebraic decay theorem for the Section 5.6 recurrence

theorem HCPolySupport.Book.Ch05.Section56.SmallContrastAlgebraicDecay.algebraic_decay_of_threeQuarter_recursion {L : ℕ} {θ α0 B : ℝ} (hL_pos : 0 < L) (hθ_pos : 0 < θ) (hθ_lt_one : θ < 1) (hα0_pos : 0 < α0) (hB_nonneg : 0 ≤ B) : ∃ (α : ℝ) (δ : ℝ) (K : ℝ), 0 < α ∧ 0 < δ ∧ 0 < K ∧ ∀ (F : ℕ → ℝ), (∀ (m : ℕ), 0 ≤ F m) → (∀ (m : ℕ), F m ≤ δ) → (∀ (m : ℕ), 8 * L + 4 ≤ m → F m ≤ θ * F (m - L) + F (threeQuarterScale m) ^ 2 + B * Real.rpow 3 (-α0 * ↑m)) → ∀ (m : ℕ), F m ≤ K * Real.rpow 3 (-α * ↑m)