Reference · Non-negative rationals

rainbow.math.rational.nnrat.contraction-general

Non-negative rationalssrc/rainbow/math/rational/nnrat/contraction_general.clj0 definitions, 1 theorems

Generalized contraction convergence: ANY contraction rate gamma <= 1/2 drives the error to zero. analysis/contraction-converges-general : gamma <= 1/2 -> e 0 <= 1 -> (forall n, e (n+1) <= gamma * e n) -> rate-null e Reduces to the 1/2 theorem by factor comparison: from gamma <= 1/2, nnrat/multiply-right-monotone gives gamma * e n <= (1/2) * e n, so the gamma-recurrence implies the 1/2-recurrence, and analysis/contraction-converges closes it. Covers the whole strong-contraction regime (rates up to 1/2). Native and axiom-free; chains nnrat-value-iteration and nnrat-multiply-right-monotone.

Depends onmath.rational.nnrat.value-iterationmath.rational.nnrat.multiply-right-monotone

analysis/contraction-converges-general :
  (gamma : ℚ≥0) (e : ℕ → ℚ≥0)
  (hgamma : gamma ≤ nnrat/half)
  (e0 : e 0 ≤ nnrat/geometric-half 0)
  (rec : ∀ (n : ℕ), e (data/succ n) ≤ gamma · e n)
  → analysis/rate-null e (fun k => k)