Reference · Signed rationals

rainbow.math.rational.signed.close-product

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

Brick 4 (band) of limit-product: the product close-band. analysis/close-product : given close L es x, close M et y, and a magnitude bound |x| <= B, conclude close (L*M) (B*et + |M|*es) (x*y). Proof: read d(x,L)<=es and d(y,M)<=et off the bands; the bilinear analysis/distance-product gives d(x*y,L*M) <= |x|*d(y,M) + |M|*d(x,L); product monotonicity (|x|<=B, distances/absolutes nonnegative) bounds that by B*et + |M|*es; then convert d(x*y,L*M) <= bound back to a close-band. Axiom-free; additive.

Depends onmath.rational.signed.distance-productmath.rational.signed.additive-distancemath.rational.signed.multiply-monotonemath.rational.signed.convergence

analysis/close-product :
  (x y L M es et B : ℚ) (hLx : analysis/close L es x) (hMy : analysis/close M et y)
  (hxB : signed/absolute x ≤ B)
  → analysis/close (L · M) (B · et + signed/absolute M · es) (x · y)