Box inverse and division

@[irreducible]

def Box.div_scalar (z : Box) (x : Interval) : Box

Box / Interval via reciproval multiplication

Equations

• z.div_scalar x = x⁻¹ • z

instance Box.instInv : Inv Box

Box inversion via scalar division

Equations

• Box.instInv = { inv := fun (z : Box) => (star z).div_scalar z.normSq }

theorem Box.inv_def (z : Box) : z⁻¹ = (star z).div_scalar z.normSq

theorem Box.approx_div_scalar {w : ℂ} {a : ℝ} {z : Box} {x : Interval} (wz : approx z w) (ax : approx x a) : approx (z.div_scalar x) (w / ↑a)

Box / Interval is conservative

instance Box.instApproxInvComplex : ApproxInv Box ℂ

Box inversion is conservative