Reference · Non-negative rationals

rainbow.math.rational.nnrat.geometric-convergence

Non-negative rationalssrc/rainbow/math/rational/nnrat/geometric_convergence.clj2 definitions, 4 theorems

The geometric (contraction-rate) convergence payoff, fully self-contained: the sequence (1/2)^n converges to zero. Rather than build nat/power + an Archimedean argument, we reach it by DOMINATION from the harmonic sequence: nat/pow2-pred n := 2^n - 1 (defined directly by recursion) nat/index-le-pow2-pred : n <= 2^n - 1 (induction) nnrat/geometric-half n := 1/2^n (= make 1 (2^n - 1)) analysis/geometric-below-harmonic : geometric-half n <= 1/(n+1) analysis/geometric-half-rate-null : geometric-half -> 0 (rate-null, identity modulus) 1/2^n <= 1/(n+1) reduces (at-most-from-cross) to succ n <= succ(2^n-1) = 2^n, i.e. n <= 2^n - 1; then rate-null-dominated against harmonic-rate-null gives (1/2)^n -> 0. This is the (1/2)-contraction convergence rate -- the analytic core of value-iteration convergence for a 1/2-discounted Bellman operator. Native and axiom-free; chains rainbow.math.rational.nnrat.harmonic-convergence on d63.

Depends onmath.rational.nnrat.harmonic-convergence

nat/pow2-pred :
  (x₁ : ℕ)
  → ℕ

nnrat/geometric-half :
  (x₁ : ℕ)
  → ℚ≥0

nat/index-le-pow2-pred :
  (n : ℕ)
  → n ≤ nat/pow2-pred n

analysis/geometric-below-harmonic :
  (n : ℕ)
  → nnrat/geometric-half n ≤ nnrat/make 1 n

analysis/geometric-half-rate-null :
  → analysis/rate-null nnrat/geometric-half (fun k => k)

analysis/geometric-error-converges :
  (error : ℕ → ℚ≥0)
  (bound : ∀ (n : ℕ), error n ≤ nnrat/geometric-half n)
  → analysis/rate-null error (fun k => k)