Box exponential and friends

@[irreducible]

def Interval.cis (t : Interval) : Box

exp (t * I)

Equations

• t.cis = { re := t.cos, im := t.sin }

@[irreducible]

def Box.exp (z : Box) : Box

exp z

Equations

• z.exp = z.re.exp • z.im.cis

@[irreducible]

def Box.sin (z : Box) : Box

sin z

Equations

• z.sin = { re := z.re.sin * (z.im.exp + (-z.im).exp).div2, im := z.re.cos * (z.im.exp - (-z.im).exp).div2 }

@[irreducible]

def Box.cos (z : Box) : Box

cos z

Equations

• z.cos = { re := z.re.cos * (z.im.exp + (-z.im).exp).div2, im := -z.re.sin * (z.im.exp - (-z.im).exp).div2 }

@[irreducible]

def Box.sinh (z : Box) : Box

Equations

• z.sinh = z.div_I.sin.mul_I

@[irreducible]

def Box.cosh (z : Box) : Box

Equations

• z.cosh = z.mul_I.cos

theorem Interval.approx_cis {t : Interval} {t' : ℝ} (m : approx t t') : approx t.cis (Complex.exp (↑t' * Complex.I))

theorem Box.approx_exp {z : Box} {z' : ℂ} (m : approx z z') : approx z.exp (Complex.exp z')

theorem Box.approx_sin {z : Box} {z' : ℂ} (m : approx z z') : approx z.sin (Complex.sin z')

theorem Box.approx_cos {z : Box} {z' : ℂ} (m : approx z z') : approx z.cos (Complex.cos z')

theorem Box.approx_sinh {z : Box} {z' : ℂ} (m : approx z z') : approx z.sinh (Complex.sinh z')

theorem Box.approx_cosh {z : Box} {z' : ℂ} (m : approx z z') : approx z.cosh (Complex.cosh z')

@[simp]

theorem Interval.cis_nan : nan.cis = { re := pm1, im := pm1 }