Interval powers

These are easy on top of exp and log.

@[irreducible]

def Interval.pow (x y : Interval) : Interval

x^y = exp (x.log * y)

Equations

• x.pow y = (x.log * y).exp

instance instPowInterval : Pow Interval Interval

Equations

• instPowInterval = { pow := Interval.pow }

theorem Interval.pow_def {x y : Interval} : x ^ y = (x.log * y).exp

theorem Interval.approx_pow {x y : Interval} {x' y' : ℝ} (xm : approx x x') (ym : approx y y') : approx (x ^ y) (x' ^ y')

Interval.pow is conservative

theorem Interval.approx_pow_nat {x : Interval} {x' : ℝ} {n : ℕ} (xm : approx x x') : approx (x ^ ↑n) (x' ^ n)

Interval.pow is conservative for ℕ powers

@[simp]

theorem Interval.nan_pow {y : Interval} : nan ^ y = nan

Interval.pow propagates nan

@[simp]

theorem Interval.pow_nan {x : Interval} : x ^ nan = nan

Interval.pow propagates nan

Interval ^ ℕ powers

@[irreducible]

def Floating.powNatSlow (x : Floating) (n : ℕ) : Interval

For use within Interval.powNat for large n (not very optimised)

Equations

• x.powNatSlow n = bif n == 0 then 1 else have p := ↑x.abs ^ ↑n; bif decide ((n % 2 == 1) = true ∧ x < 0) then -p else p

@[irreducible]

def Interval.powNat (x : Interval) (n : ℕ) : Interval

Special case low powers, and use Floating.powNatSlow for larger n

Equations

• x.powNat 0 = 1
• x.powNat 1 = x
• x.powNat 2 = x.sqr
• x.powNat 3 = x.sqr * x
• x.powNat 4 = x.sqr.sqr
• x.powNat n = bif decide (x.lo < 0) && decide (0 ≤ x.hi) && decide (n % 2 = 0) then 0 ∪ (x.lo.powNatSlow n ∪ x.hi.powNatSlow n) else x.lo.powNatSlow n ∪ x.hi.powNatSlow n

instance instPowIntervalNat : Pow Interval ℕ

Equations

• instPowIntervalNat = { pow := Interval.powNat }

theorem Interval.powNat_def {x : Interval} {n : ℕ} : x ^ n = x.powNat n

theorem Floating.approx_powNatSlow {x' : ℝ} {x : Floating} (xm : approx x x') (n : ℕ) : approx (x.powNatSlow n) (x' ^ n)

Floating.powNatSlow is conservative

@[simp]

theorem Floating.nan_powNatSlow {n : ℕ} (n0 : n ≠ 0) : nan.powNatSlow n = nan

theorem Interval.approx_powNat {x : Interval} {x' : ℝ} {n : ℕ} (xm : approx x x') : approx (x ^ n) (x' ^ n)

Interval ^ ℕ is conservative

Interval ^ ℤ powers

@[irreducible]

def Interval.powInt (x : Interval) (n : ℤ) : Interval

Equations

• x.powInt n = bif decide (n < 0) then (x ^ n.natAbs).inv else x ^ n.natAbs

instance instPowIntervalInt : Pow Interval ℤ

Equations

• instPowIntervalInt = { pow := Interval.powInt }

theorem Interval.powInt_def {x : Interval} {n : ℤ} : x ^ n = x.powInt n

theorem Interval.approx_powInt {x : Interval} {x' : ℝ} {n : ℤ} (xm : approx x x') : approx (x ^ n) (x' ^ n)

Interval.powInt is conservative