IterationLemma

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Fast geometric-decay iteration lemma

A standalone real-analysis prelude for a De Giorgi / Stampacchia iteration. If a nonnegative sequence Y starting below 1 satisfies a superlinear recursion Y (n+1) ≤ A · Bⁿ · (Y n)^{1+β} with the compatibility bound A ≤ B^{-1/β}, then Y n ≤ B^{-n/β} for every n, and (when 1 < B) Y → 0.

All exponents are real (Real.rpow). No sorry, no axioms, no heartbeat overrides.

theorem HCPolySupport.iteration_geometric_decay {Y : ℕ → ℝ} {A B β : ℝ} (hY0 : Y 0 ≤ 1) (hYnn : ∀ (n : ℕ), 0 ≤ Y n) (hβ : 0 < β) (hB : 1 ≤ B) (hA : 0 ≤ A) (hAB : A ≤ B ^ (-(1 / β))) (hrec : ∀ (n : ℕ), Y (n + 1) ≤ A * B ^ ↑n * Y n ^ (1 + β)) (n : ℕ) : Y n ≤ B ^ (-↑n / β)

Fast geometric decay. A nonnegative sequence obeying a superlinear recursion with a compatible leading constant decays at least like the geometric rate B^{-n/β}.

theorem HCPolySupport.iteration_geometric_decay_tendsto_zero {Y : ℕ → ℝ} {A B β : ℝ} (hY0 : Y 0 ≤ 1) (hYnn : ∀ (n : ℕ), 0 ≤ Y n) (hβ : 0 < β) (hB : 1 < B) (hA : 0 ≤ A) (hAB : A ≤ B ^ (-(1 / β))) (hrec : ∀ (n : ℕ), Y (n + 1) ≤ A * B ^ ↑n * Y n ^ (1 + β)) : Filter.Tendsto Y Filter.atTop (nhds 0)

Fast geometric decay (corollary). Under the same recursion with a genuine contraction rate 1 < B, the sequence tends to 0.