Reference · Analysis

rainbow.math.analysis.geometric-denominator

Analysissrc/rainbow/math/analysis/geometric_denominator.clj0 definitions, 1 theorems

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

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. Proved axiom-free by induction on N. The base uses nat/multiply-one-right (2^0 = 1). The step uses that halving doubles the denominator -- denominator (seq d0 (succ N)) reduces to D + (D + 0) where D = denominator (seq d0 N) -- and that 2^(N+1) = 2 * 2^N reduces to P + (P + 0) where P = 2^N; substituting the induction hypothesis D = den(d0) * P and expanding den(d0) * (P + (P + 0)) with the freshly proved nat/multiply-distributes-add and nat/multiply-zero-right makes both sides equal. Requires geometric/seq, nnrat/denominator, nat/power, nat/multiply, nat/multiply-distributes-add, nat/multiply-zero-right, nat/multiply-one-right (d63 + nat-add-order + half-monotone + geometric-sequence + nat-power + nat-distributive).

geometric/seq-denominator :
  (d0 : ℚ≥0) (n : ℕ)
  → nnrat/denominator (geometric/seq d0 n) = nat/multiply (nnrat/denominator d0) (nat/power 2 n)