Reference · Signed rationals

rainbow.math.rational.signed.distance-multiply-absolute

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

Brick 2 of limit-product: distance scales by the ABSOLUTE value of a sign-indefinite left factor. analysis/distance-multiply-left-absolute : d(w*x, w*y) <= |w| * d(x, y) for ARBITRARY signed w. The existing signed/distance-multiply-left-nonnegative only covers 0<=w (giving w*d(x,y)); this lifts it to any w via a sign case-split on decide-at-most 0 w: - 0<=w : the nonnegative base, then |w|~w (absolute-of-nonnegative) rewrites w to |w|. - w<=0 : apply the base at -w (>=0), and transport d((-w)*x,(-w)*y) ~ d(w*x,w*y) [multiply-negate-left + distance-negate-both] while |w|~-w (absolute-of-nonpositive) rewrites (-w) to |w|. Axiom-free; additive; does not touch the LP checker.

Depends onmath.rational.signed.absolute-signmath.rational.signed.distance-negatemath.rational.signed.distance-multiply-nonnegativemath.rational.signed.multiply-ring

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