Reference · Natural numbers

rainbow.math.nat.power-growth

Natural numberssrc/rainbow/math/nat/power_growth.clj0 definitions, 3 theorems

Growth lemmas for nat exponentiation, on the road to the geometric-convergence modulus. The first is positivity of the powers of two: 1 <= 2^n for every n, proved by induction on n. The base case 2^0 = 1 is reflexive; the step uses that 2^(n+1) = 2 * 2^n reduces (through nat/multiply) to 2^n + (2^n + 0), so 2^n <= 2^(n+1) by nat/le-add-right, and transitivity with the induction hypothesis 1 <= 2^n gives 1 <= 2^(n+1). Positivity is the first ingredient of the archimedean bound d0 <= eps * 2^n that completes the forall-epsilon convergence theorem. Requires nat/power, nat/at-most(-reflexive,-transitive), nat/le-add-right, algebra/nat-add (d63 checkpoint + nat-add-order).

nat/power-two-at-least-one :
  (n : ℕ)
  → 1 ≤ nat/power 2 n

nat/at-most-power-two :
  (n : ℕ)
  → n ≤ nat/power 2 n

nat/le-multiply-succ :
  (f x : ℕ)
  → x ≤ nat/multiply (data/succ f) x