Reference · Rationals

rainbow.math.rational.convergence

Rationalssrc/rainbow/math/rational/convergence.clj1 definitions, 1 theorems

Convergence of a nonnegative-rational distance sequence to its limit, with an explicit rational modulus -- the analysis layer above the geometric contraction bound. A distance sequence `seq : Nat -> nnrat` (the distance d(x_n, limit)) converges when, for every accuracy epsilon, a modulus tells how far to iterate: converges-to seq modulus := forall epsilon. forall n. (modulus epsilon <= n) -> (seq n <= epsilon) using the native Prop orders `nat/at-most` and `nnrat/at-most`. No absolute value is needed (the distance is already nonnegative) and no reals are needed (the modulus is Nat-valued). For a geometric contraction (seq n = gamma^n * d0 with rational gamma < 1) the modulus is the least n with gamma^n * d0 <= epsilon, so convergence is exact rational/Nat data. Composed with a fixed-point uniqueness result this gives proved value-iteration convergence. Requires `nat/at-most` and `nnrat/at-most` in the environment.

convergence/converges-to :
  (x₁ : ℕ → ℚ≥0) (x₂ : ℚ≥0 → ℕ)
  → Prop

convergence/converges-to-unfold :
  (seq : ℕ → ℚ≥0) (modulus : ℚ≥0 → ℕ)
  → convergence/converges-to seq modulus = (∀ (epsilon : ℚ≥0), ∀ (n : ℕ), modulus epsilon ≤ n → seq n ≤ epsilon)