Reference · Signed rationals

rainbow.math.rational.signed.distance-product

Signed rationalssrc/rainbow/math/rational/signed/distance_product.clj0 definitions, 2 theorems

Brick 4 (core) of limit-product: the bilinear distance bound for a product. analysis/distance-product : d(x*y, L*M) <= |x|*d(y,M) + |M|*d(x,L). Proof: triangle through x*M, d(x*y,x*M) <= |x|*d(y,M) by brick 2 (distance-multiply-left-absolute at w=x), and d(x*M,L*M) <= |M|*d(x,L) by the right-factor variant distance-multiply-right-absolute (brick 2 + commutativity); add-monotone + transitivity combine. Axiom-free; additive. Also exports signed/distance-multiply-right-absolute : d(x*w, y*w) <= |w|*d(x,y).

Depends onmath.rational.signed.distance-multiply-absolutemath.rational.signed.distance-trianglemath.rational.signed.multiply-ring

signed/distance-multiply-right-absolute :
  (x y w : ℚ)
  → signed/distance (x · w) (y · w) ≤ signed/absolute w · signed/distance x y

analysis/distance-product :
  (x y L M : ℚ)
  → signed/distance (x · y) (L · M) ≤ signed/absolute x · signed/distance y M + signed/absolute M · signed/distance x L