Reference · Non-negative rationals

rainbow.math.rational.nnrat.radius-cancel

Non-negative rationalssrc/rainbow/math/rational/nnrat/radius_cancel.clj0 definitions, 1 theorems

The reciprocal radius-cancellation for a general positive nnrat, the linchpin of the limit-product modulus. analysis/nnrat-radius-cancel : 1 <= numerator D -> (from-nnrat D) * ((from-nnrat (recip (make (succ (pred (num D))) (den-pred D)))) * eps) ~ eps Everything is kept in the make(succ p, q) form mmag := make(succ(pred(num D)))(den-pred D) (so analysis/scale-reciprocal-radius-cancel from the limit-scale work applies directly), and D ~ mmag (nnrat/make-succ-of-positive-numerator) is lifted to from-nnrat D ~ from-nnrat mmag (from-nnrat-respects-equivalence) then under the scale (multiply-right-respects). No nnrat/reciprocal-respects needed. Axiom-free; additive.

Depends onmath.rational.signed.limit-scale-lawmath.rational.nnrat.positive-succ-formmath.rational.signed.multiply-ring

analysis/nnrat-radius-cancel :
  (D : ℚ≥0) (eps : ℚ)
  (h : 1 ≤ nnrat/numerator D)
  → signed/from-nnrat D · (signed/from-nnrat (nnrat/reciprocal (data/pair ℕ ℕ (data/succ (nat/predecessor (nnrat/numerator D))) (nnrat/denominator-predecessor D))) · eps) = eps