Reference · Signed rationals

rainbow.math.rational.signed.limit-scalar-laws

Signed rationalssrc/rainbow/math/rational/signed/limit_scalar_laws.clj1 definitions, 3 theorems

Axiom-free constant and nonnegative-scalar laws for signed order bands. `analysis/converges` quantifies over every signed radius, including negative radii. A constant sequence therefore cannot inhabit it: `close C eps C` entails that eps is nonnegative. This module leaves that committed predicate untouched and supplies the non-vacuous radius-corrected predicate `analysis/converges-nonnegative`, together with its constant limit law. Scaling does not require changing the source predicate. At every radius and index admitted by a source convergence proof, the committed `analysis/close-scale-nonnegative` theorem gives the corresponding band with center, radius, and sequence value all multiplied by `from-nnrat c`.

Depends onmath.rational.signed.limit-scale

analysis/converges-nonnegative :
  (x₁ : ℕ → ℚ) (x₂ : ℚ) (x₃ : ℚ → ℕ)
  → Prop

analysis/close-self-nonnegative :
  (C eps : ℚ) (eps-nonnegative : signed/nonnegative eps)
  → analysis/close C eps C

analysis/limit-const :
  (C : ℚ)
  → analysis/converges-nonnegative (fun x₄ => C) C (fun x₅ => 0)

analysis/scaled-sequence-close-to-scaled-limit :
  (c : ℚ≥0) (s : ℕ → ℚ) (L : ℚ) (M : ℚ → ℕ) (s-converges : analysis/converges s L M)
  (eps : ℚ) (n : ℕ)
  (large-enough : M eps ≤ n)
  → analysis/close (signed/from-nnrat c · L) (signed/from-nnrat c · eps) (signed/from-nnrat c · s n)