Reference · Signed rationals

rainbow.math.rational.signed.convergent-bounded-below

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

Brick 1 of analysis/limit-reciprocal: a convergent sequence is bounded BELOW near its limit. Mirror of analysis/convergent-bounded. `analysis/convergent-bounded-below` : if s converges to L with modulus Ms, then for every radius r and index n at or past `Ms r`, `|L| - r <= |s n|`. Stated generally in r (no half-identity, no L != 0 hypothesis); the reciprocal proof instantiates r = |L|/2 to obtain the constant lower bound |s n| >= |L|/2 that keeps the eps-scaling divisor fixed (not varying in n). Proof: read the radius-r band `close L r (s n)` off convergence; convert to `distance (s n) L <= r`; then the OTHER reverse triangle `|L| = |(L - s n) + s n| <= |L - s n| + |s n| = distance L (s n) + |s n|`, with `distance L (s n) ~ distance (s n) L <= r` (distance-symmetric), gives `|L| <= r + |s n|`, hence `|L| - r <= |s n|` (subtract-at-most-of-additive-upper). Axiom-free; additive; does not touch the LP checker. Env chain: signed-convergence, signed-additive-distance, signed-distance-triangle, signed-recovery-laws (as convergent-bounded), plus signed-distance (distance-symmetric).

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

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