Reference · Analysis

rainbow.math.analysis.geometric-convergence

Analysissrc/rainbow/math/analysis/geometric_convergence.clj0 definitions, 4 theorems

Worked geometric convergence: the contraction distance provably reaches below each accuracy threshold at a computable step. For gamma = 1/2 and starting distance 8, the distances are 8, 4, 2, 1, 1/2, 1/4, ...; so the modulus that achieves accuracy epsilon is the least step whose distance is <= epsilon: step 3 reaches <= 1, step 4 reaches <= 1/2, step 5 reaches <= 1/4. Each bound is a native `nnrat/at-most` proved through the decidable comparison (`nnrat/decide-at-most-true-sound` applied to the reflexivity that the decision computes to true). These are the concrete instances of the convergence modulus underlying `convergence/converges-to`; the fully general `forall epsilon` statement composes them with monotonicity of gamma^n. Requires `nnrat/at-most`, `audit/decide-nnrat-at-most`, and `nnrat/decide-at-most-true-sound` in the environment.

convergence/reaches-one-at-step-3 :
  → nnrat/half · (nnrat/half · (nnrat/half · 8)) ≤ 1

convergence/reaches-half-at-step-4 :
  → nnrat/half · (nnrat/half · (nnrat/half · (nnrat/half · 8))) ≤ nnrat/half

convergence/monotone-decrease :
  → nnrat/half · (nnrat/half · (nnrat/half · (nnrat/half · 8))) ≤ nnrat/half · (nnrat/half · (nnrat/half · 8))

convergence/reaches-below-half-at-step-5 :
  → nnrat/half · (nnrat/half · (nnrat/half · (nnrat/half · (nnrat/half · 8)))) ≤ nnrat/half