Reference
Analysis
6 modules in src/rainbow/math/analysis/. All folders
| Module | What it proves | Theorems |
|---|---|---|
| math.analysis.geometric-convergence | Worked geometric convergence: the contraction distance provably reaches below each accuracy threshold at a computable step. | 4 |
| math.analysis.geometric-decay | The geometric contraction bound -- the analysis entry point for value-iteration convergence. | 5 |
| math.analysis.geometric-denominator | The denominator half of the geometric-sequence closed form: denominator (seq d0 N) = denominator d0 * 2^N for every N, completing (with geometric/seq-numerator-invariant) the closed form seq d0 N = num(d0) / (den(d0) * 2^N) that the convergence modulus needs. | 1 |
| math.analysis.geometric-modulus | The geometric-convergence MODULUS -- the last ingredient of the general forall-epsilon rational convergence theorem. | 2 |
| math.analysis.geometric-sequence | The geometric contraction sequence as a native recursive function and its general (forall-n) step monotonicity -- the sequence-level consequence of the halving-monotonicity keystone (nnrat/half-le-self). | 4 |
| math.analysis.geometric-threshold | The first fully-general-over-n convergence statement for the geometric contraction: for the worked start distance d0 = 8 and threshold eps = 1, the distance is at most 1 at EVERY step from the modulus 3 onward: forall n. | 1 |