Reference · Signed rationals

rainbow.math.rational.signed.convergence

Signed rationalssrc/rainbow/math/rational/signed/convergence.clj2 definitions, 1 theorems

Real-analysis roadmap step 5: the epsilon-N convergence predicate over signed-rational sequences, and the SQUEEZE THEOREM -- the first genuinely-frontier analysis result and the checkpoint that the epsilon-N machinery goes through in this kernel. analysis/close L eps x := (L - eps <= x) AND (x <= L + eps) (order band) analysis/converges s L M := forall eps n, M eps <= n -> close L eps (s n) analysis/squeeze : a <= s <= b pointwise, a -> L, b -> L ==> s -> L with combined modulus M eps = Ma eps + Mb eps. The squeeze needs no new signed arithmetic -- only the signed order transitivity from step 4: for n >= Ma+Mb we get n >= Ma and n >= Mb (nat le-add via witnesses), read off L-eps <= a(n) and b(n) <= L+eps from the two convergences (conjunction projections), and chain L-eps <= a(n) <= s(n) and s(n) <= b(n) <= L+eps through signed/at-most-transitive. Native and axiom-free; chains rainbow.math.rational.signed.order-transitivity on d63.

Depends onmath.rational.signed.order-transitivity

analysis/close :
  (x₁ x₂ x₃ : ℚ)
  → Prop

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

analysis/squeeze :
  (a b s : ℕ → ℚ) (L : ℚ) (Ma Mb : ℚ → ℕ)
  (ha-s : ∀ (n : ℕ), a n ≤ s n)
  (hs-b : ∀ (n : ℕ), s n ≤ b n)
  (ca : analysis/converges a L Ma) (cb : analysis/converges b L Mb)
  → analysis/converges s L (fun eps => algebra/nat-add (Ma eps) (Mb eps))