Reference · Signed rationals

rainbow.math.rational.signed.limit-product

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

The product limit law: the pointwise product of two convergent signed-rational sequences converges to the product of the limits. This is the capstone of the real-analysis limit-product arc. Axiom-free; additive. analysis/limit-product : converges s L Ms -> converges t M Mt -> converges (n |-> (s n) * (t n)) (L * M) M' with modulus M' eps = nadd (nadd (Ms (d eps)) (Mt (d eps))) (Ms one) and scaled radius d eps = (from-nnrat (recip mmag)) * eps, where V = (1+|L|)+|M|, D = magnitude V, mmag = make (succ (pred (num D))) (den-pred D). The radius (B*(d eps) + |M|*(d eps)) produced by close-product collapses to eps: distributivity gathers it to V*(d eps), from-nnrat-magnitude replaces V by from-nnrat D (V is nonnegative -- product-radius-nonneg), and nnrat-radius-cancel cancels the reciprocal (num D is positive -- product-radius-numerator-positive). Threshold extraction and the final close-respects-radius-equivalence follow the analysis/limit-sum template exactly.

Depends onmath.rational.signed.close-productmath.rational.signed.convergent-boundedmath.rational.signed.limit-arithmeticmath.rational.nnrat.radius-cancelmath.rational.signed.product-radius-nonnegmath.rational.signed.product-radius-positivemath.rational.signed.distributivemath.rational.signed.equivalence-laws

analysis/limit-product :
  (s t : ℕ → ℚ) (L M : ℚ) (Ms Mt : ℚ → ℕ) (convS : analysis/converges s L Ms)
  (convT : analysis/converges t M Mt)
  → analysis/converges (fun n => s n · t n) (L · M) (fun eps => algebra/nat-add (algebra/nat-add (Ms (signed/from-nnrat (nnrat/reciprocal (pair)) · eps)) (Mt (signed/from-nnrat (nnrat/reciprocal (pair)) · eps))) (Ms 1))
  where pair := data/pair ℕ ℕ (data/succ (nat/predecessor (nnrat/numerator (signed/magnitude (…⟨1⟩ + …⟨3⟩ + …⟨1⟩ …⟨1⟩))))) (nnrat/denominator-predecessor (signed/magnitude (1 + signed/absolute L + signed/absolute M)))