Reference · Analysis

rainbow.math.analysis.geometric-sequence

Analysissrc/rainbow/math/analysis/geometric_sequence.clj1 definitions, 4 theorems

In Rainbow 1.4.1, lein verify rainbow.math.analysis.geometric-sequence fails on its own: the module uses lemmas from math.logic.half-monotone, math.nat.add-order without listing them in its dependencies. It checks once those are installed.

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). For a starting distance d0 the sequence seq d0 0 = d0 seq d0 (succ n) = (1/2) * (seq d0 n) (= (1/2)^n * d0) is defined by recursion on n (data/Nat.rec). Its step monotonicity seq d0 (succ n) <= seq d0 n for every n is exactly nnrat/half-le-self instantiated at the term (seq d0 n): the next distance is half the current one, hence no larger. This is the general monotone-decrease of the contraction distances (the worked instances live in geometric-convergence), one of the two ingredients -- with a modulus that drives the distance below any threshold -- of the forall-epsilon convergence theorem convergence/converges-to. Requires nnrat/multiply, nnrat/half, nnrat/at-most, and nnrat/half-le-self.

geometric/seq :
  (x₁ : ℚ≥0) (x₂ : ℕ)
  → ℚ≥0

geometric/seq-step-unfold :
  (d0 : ℚ≥0) (n : ℕ)
  → geometric/seq d0 (data/succ n) = nnrat/half · geometric/seq d0 n

geometric/seq-step-monotone :
  (d0 : ℚ≥0) (n : ℕ)
  → geometric/seq d0 (data/succ n) ≤ geometric/seq d0 n

geometric/seq-decreases-with-iteration :
  (d0 : ℚ≥0) (n k : ℕ)
  → geometric/seq d0 (algebra/nat-add n k) ≤ geometric/seq d0 k

geometric/seq-numerator-invariant :
  (d0 : ℚ≥0) (n : ℕ)
  → nnrat/numerator (geometric/seq d0 n) = nnrat/numerator d0