Documentation

Init.Data.Dyadic.Inv

Inversion for dyadic numbers #

source
def Dyadic.invAtPrec (x : Dyadic) (prec : Int) :
Dyadic

Inverts a dyadic number at a given (maximum) precision. Returns the greatest dyadic number with precision at most prec which is less than or equal to 1/x. For x = 0, returns 0.

Equations
Instances For
    source
    theorem Dyadic.invAtPrec_mul_le_one {x : Dyadic} (hx : 0 < x) (prec : Int) :
    x.invAtPrec prec * x ≤ 1

    For a positive dyadic x, invAtPrec x prec * x ≤ 1.

    source
    theorem Dyadic.one_lt_invAtPrec_add_inc_mul {x : Dyadic} (hx : 0 < x) (prec : Int) :
    1 < (x.invAtPrec prec + ofIntWithPrec 1 prec) * x

    For a positive dyadic x, 1 < (invAtPrec x prec + 2^(-prec)) * x.