Reference · Analysis

rainbow.math.analysis.geometric-decay

Analysissrc/rainbow/math/analysis/geometric_decay.clj1 definitions, 5 theorems

The geometric contraction bound -- the analysis entry point for value-iteration convergence. A strict contraction with rational modulus gamma < 1 shrinks the distance to the fixed point by a factor gamma each step: d_{n+1} = gamma * d_n so d_n = gamma^n * d_0 With a rational gamma the whole trajectory is exact rational arithmetic (no reals, no logarithms), so the geometric decay is proved directly: from a starting distance 8 with gamma = 1/2 the distances are 8, 4, 2, 1, ... halving toward 0. This is the quantitative core that, composed with a fixed-point uniqueness result, gives a rational modulus of convergence: to reach distance below any epsilon it suffices to iterate until gamma^n * d_0 < epsilon. The full convergence theorem (the limit is the unique fixed point) is built on top of this with a rational convergence modulus.

decay/contract :
  (x₁ x₂ : ℚ≥0)
  → ℚ≥0

decay/contract-unfold :
  (gamma distance : ℚ≥0)
  → decay/contract gamma distance = gamma · distance

decay/step1-eight-to-four :
  → decay/contract nnrat/half 8 = 4

decay/step2-four-to-two :
  → decay/contract nnrat/half 4 = 2

decay/step3-two-to-one :
  → decay/contract nnrat/half 2 = 1

decay/three-steps-eight-to-one :
  → decay/contract nnrat/half (contract) = 1
  where contract := decay/contract nnrat/half (decay/contract nnrat/half 8)