Reference · Signed rationals

rainbow.math.rational.signed.reciprocal-absolute-bound

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

Layer A of the limit-reciprocal assembly: bound the absolute reciprocal of x by the reciprocal of a positive lower bound on |x|. signed/absolute-reciprocal-at-most-of-lower-bound : nonneg b -> 1<=num(mag(b*b)) -> 1<=num(mag(x*x)) -> 1<=num(mag(|x|*|x|)) -> b <= |x| -> |reciprocal x| <= reciprocal b |reciprocal x| ~ reciprocal|x| by uniqueness of inverse (both times |x| give 1: absolute-reciprocal-times-self and multiply-reciprocal-self), then reciprocal-antitone on b <= |x| gives reciprocal|x| <= reciprocal b. In the assembly, b = |L|/2 and the convergent-bounded-below lower bound |L|/2 <= |s n| yield the CONSTANT bound |reciprocal (s n)| <= reciprocal(|L|/2) = 2/|L|. Axiom-free; additive; no LP-checker touch.

Depends onmath.rational.signed.absolute-reciprocal-times-selfmath.rational.signed.reciprocalmath.rational.signed.inverse-uniquemath.rational.signed.reciprocal-antitonemath.rational.signed.multiply-ringmath.rational.signed.order-respects

signed/absolute-reciprocal-at-most-of-lower-bound :
  (b x : ℚ) (hbnn : signed/nonnegative b)
  (hb2 : 1 ≤ nnrat/numerator (signed/magnitude (b · b)))
  (hx2 : 1 ≤ nnrat/numerator (signed/magnitude (x · x)))
  (habsx2 : 1 ≤ nnrat/numerator (signed/magnitude (signed/absolute x · signed/absolute x)))
  (hbx : b ≤ signed/absolute x)
  → signed/absolute (signed/reciprocal x) ≤ signed/reciprocal b