Reference · Signed rationals

rainbow.math.rational.signed.convergent-bounded

Signed rationalssrc/rainbow/math/rational/signed/convergent_bounded.clj0 definitions, 1 theorems

Brick 1 of analysis/limit-product: a convergent sequence is bounded. `analysis/convergent-bounded` : if s converges to L with modulus Ms, then for every index n at or past `Ms 1`, `|s n| <= 1 + |L|`. This is the load-bearing prerequisite the product proof needs (to bound the varying factor s_n) and is independently the first real 'convergent => bounded' fact over signed sequences (the prior analysis/bounded-above was nnrat-only and unconnected to converges). Proof: read the radius-1 band `close L 1 (s n)` off convergence; convert it to `distance (s n) L <= 1` (distance-at-most-of-additive-closeness, after rearranging the lower band L-1<=s n into L<=s n+1); then the reverse triangle `|s n| = |(s n - L) + L| <= |s n - L| + |L| = distance (s n) L + |L| <= 1 + |L|` via absolute-add-triangle + subtract-then-add + add-monotone. Axiom-free; additive; does not touch the LP checker. Env chain: signed-convergence (converges/close), signed-additive-distance (the distance<->band bridges), signed-distance-triangle (absolute + triangle + order laws), signed-recovery-laws (subtract-then-add).

Depends onmath.rational.signed.convergencemath.rational.signed.additive-distancemath.rational.signed.distance-trianglemath.rational.signed.recovery-laws

analysis/convergent-bounded :
  (s : ℕ → ℚ) (L : ℚ) (Ms : ℚ → ℕ) (conv : analysis/converges s L Ms) (n : ℕ)
  (hn : Ms 1 ≤ n)
  → signed/absolute (s n) ≤ 1 + signed/absolute L