Reference · Non-negative rationals

rainbow.math.rational.nnrat.value-iteration

Non-negative rationalssrc/rainbow/math/rational/nnrat/value_iteration.clj0 definitions, 5 theorems

The self-contained value-iteration convergence theorem: a contraction recurrence drives the error to zero. analysis/contraction-converges : e 0 <= 1 -> (forall n, e (n+1) <= (1/2) * e n) [1/2-contraction recurrence] -> rate-null e [e converges to zero] This is the frontier-OR payoff on the analysis track: if the value-iteration error contracts by 1/2 each sweep (a 1/2-discounted Bellman operator), the iterates provably converge. Proof: induction gives e n <= (1/2)^n (the step uses nnrat/multiply-monotone on the recurrence + the bridge equivalence (1/2)*(1/2)^n ~ (1/2)^(n+1), transported by at-most-respects-equivalence), then geometric-error-converges (dominated by (1/2)^n -> 0) closes it. The bridge reduces to the nat identity 2*(p+1) = (p+p)+2, proved here via multiply-successor-right + multiply-one-right. Native and axiom-free; chains nnrat-geometric-convergence and nnrat-multiply-monotone.

Depends onmath.rational.nnrat.geometric-convergencemath.rational.nnrat.multiply-monotone

nat/two-times :
  (p : ℕ)
  → nat/multiply 2 p = algebra/nat-add p p

nat/two-times-succ :
  (p : ℕ)
  → nat/multiply 2 (data/succ p) = data/succ (data/succ (algebra/nat-add p p))

nnrat/geometric-half-halving :
  (n : ℕ)
  → nnrat/half · nnrat/geometric-half n = nnrat/geometric-half (data/succ n)

analysis/contraction-error-below-geometric :
  (e : ℕ → ℚ≥0)
  (e0 : e 0 ≤ nnrat/geometric-half 0)
  (rec : ∀ (n : ℕ), e (data/succ n) ≤ nnrat/half · e n)
  (n : ℕ)
  → e n ≤ nnrat/geometric-half n

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