Reference · Signed rationals

rainbow.math.rational.signed.limit-square

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

A direct corollary of analysis/limit-product: the square of a convergent signed sequence converges to the square of the limit. analysis/limit-square : converges s L Ms -> converges (n |-> (s n)*(s n)) (L*L) M' M' is limit-product's own modulus instantiated at t=s, M=L, Mt=Ms. The proof is the single application `limit-product s s L L Ms Ms convS convS`. This is the degree-2 case of the (existentially-moduled) limit-power induction; the general limit-power (positive powers, by Nat.rec on the exponent using limit-product at each step, with an existential modulus to avoid modulus-matching) is the natural next extension. Axiom-free; additive; does not touch the LP checker; does NOT depend on the reciprocal arc.

Depends onmath.rational.signed.limit-product

analysis/limit-square :
  (s : ℕ → ℚ) (L : ℚ) (Ms : ℚ → ℕ) (convS : analysis/converges s L Ms)
  → analysis/converges (fun n => s n · s n) (L · L) (fun eps => algebra/nat-add (algebra/nat-add (Ms (signed/from-nnrat (nnrat/reciprocal (pair)) · eps)) (Ms (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 L)))