Reference · Analysis

rainbow.math.analysis.geometric-modulus

Analysissrc/rainbow/math/analysis/geometric_modulus.clj0 definitions, 2 theorems

In Rainbow 1.4.1, lein verify rainbow.math.analysis.geometric-modulus fails on its own: the module uses lemmas from math.nat.power-growth without listing them in its dependencies. It checks once those are installed.

The geometric-convergence MODULUS -- the last ingredient of the general forall-epsilon rational convergence theorem. For a positive accuracy eps = make (succ p) q (numerator succ p >= 1, so eps > 0) and start distance d0, the contraction distance is at most eps after N = numerator(d0) * denominator(eps) halving steps: seq d0 N <= eps. Proved native and axiom-free by assembling the finished pieces. Through nnrat/at-most-from-cross the goal reduces to the cross inequality num(seq d0 N)*den(eps) <= num(eps)*den(seq d0 N); substituting the sequence closed form (geometric/seq-numerator-invariant, geometric/seq-denominator) it becomes num(d0)*den(eps) <= num(eps)*(den(d0)*2^N); and since the left side is exactly N, the chain N <= 2^N (nat/at-most-power-two) <= den(d0) * 2^N (nat/le-multiply-succ, den(d0) succ-headed) <= num(eps) * (den(d0) * 2^N) (nat/le-multiply-succ, num(eps) succ-headed) closes it. Combined with geometric/seq-decreases-with-iteration (every later iterate is no larger) this yields convergence/converges-to for the geometric contraction with the explicit rational/Nat modulus. Requires the full analysis stack: geometric/seq(+numerator-invariant), geometric/seq-denominator, nat/power, nat/at-most-power-two, nat/le-multiply-succ, nnrat/at-most-from-cross, and the equality transport lemmas.

geometric/reaches-below-epsilon :
  (d0 : ℚ≥0) (p q : ℕ)
  → geometric/seq d0 (multiply) ≤ nnrat/make (data/succ p) q
  where multiply := nat/multiply (nnrat/numerator d0) (nnrat/denominator (nnrat/make (data/succ p) q))

geometric/converges-for-positive-epsilon :
  (d0 : ℚ≥0) (p q n : ℕ)
  (bound : nat/multiply (nnrat/numerator d0) (nnrat/denominator (nnrat/make (data/succ p) q)) ≤ n)
  → geometric/seq d0 n ≤ nnrat/make (data/succ p) q