Interval arithmetic #
This file defines arithmetic operations on intervals and prove their correctness. Note that this is
full precision operations. The essentials of float operations can be found
in data.fp.basic
. We have not yet integrated these with the rest of the library.
One/zero #
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
- interval.has_one = {one := interval.pure 1}
@[protected, instance]
Equations
- interval.has_zero = {zero := interval.pure 0}
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Addition/multiplication #
Note that this multiplication does not apply to ℚ
or ℝ
.
@[protected, instance]
def
nonempty_interval.has_add
{α : Type u_2}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le] :
Equations
- nonempty_interval.has_add = {add := λ (s t : nonempty_interval α), {to_prod := s.to_prod + t.to_prod, fst_le_snd := _}}
@[protected, instance]
def
nonempty_interval.has_mul
{α : Type u_2}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le] :
Equations
- nonempty_interval.has_mul = {mul := λ (s t : nonempty_interval α), {to_prod := s.to_prod * t.to_prod, fst_le_snd := _}}
@[protected, instance]
def
interval.has_add
{α : Type u_2}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le] :
Equations
@[protected, instance]
def
interval.has_mul
{α : Type u_2}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le] :
Equations
@[simp]
theorem
nonempty_interval.to_prod_add
{α : Type u_2}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s t : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.to_prod_mul
{α : Type u_2}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s t : nonempty_interval α) :
theorem
nonempty_interval.fst_add
{α : Type u_2}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s t : nonempty_interval α) :
theorem
nonempty_interval.fst_mul
{α : Type u_2}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s t : nonempty_interval α) :
theorem
nonempty_interval.snd_mul
{α : Type u_2}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s t : nonempty_interval α) :
theorem
nonempty_interval.snd_add
{α : Type u_2}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s t : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.coe_add_interval
{α : Type u_2}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s t : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.coe_mul_interval
{α : Type u_2}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s t : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.pure_add_pure
{α : Type u_2}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(a b : α) :
@[simp]
theorem
nonempty_interval.pure_mul_pure
{α : Type u_2}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(a b : α) :
@[simp]
theorem
interval.bot_mul
{α : Type u_2}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(t : interval α) :
@[simp]
theorem
interval.bot_add
{α : Type u_2}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(t : interval α) :
@[simp]
theorem
interval.mul_bot
{α : Type u_2}
[preorder α]
[has_mul α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s : interval α) :
@[simp]
theorem
interval.add_bot
{α : Type u_2}
[preorder α]
[has_add α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s : interval α) :
Powers #
@[protected, instance]
def
nonempty_interval.has_nsmul
{α : Type u_2}
[add_monoid α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le] :
Equations
- nonempty_interval.has_nsmul = {smul := λ (n : ℕ) (s : nonempty_interval α), {to_prod := (n • s.to_prod.fst, n • s.to_prod.snd), fst_le_snd := _}}
@[protected, instance]
def
nonempty_interval.has_pow
{α : Type u_2}
[monoid α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le] :
Equations
- nonempty_interval.has_pow = {pow := λ (s : nonempty_interval α) (n : ℕ), {to_prod := s.to_prod ^ n, fst_le_snd := _}}
@[simp]
theorem
nonempty_interval.to_prod_pow
{α : Type u_2}
[monoid α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s : nonempty_interval α)
(n : ℕ) :
@[simp]
theorem
nonempty_interval.to_prod_nsmul
{α : Type u_2}
[add_monoid α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s : nonempty_interval α)
(n : ℕ) :
theorem
nonempty_interval.fst_pow
{α : Type u_2}
[monoid α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s : nonempty_interval α)
(n : ℕ) :
theorem
nonempty_interval.fst_nsmul
{α : Type u_2}
[add_monoid α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s : nonempty_interval α)
(n : ℕ) :
theorem
nonempty_interval.snd_nsmul
{α : Type u_2}
[add_monoid α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(s : nonempty_interval α)
(n : ℕ) :
theorem
nonempty_interval.snd_pow
{α : Type u_2}
[monoid α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(s : nonempty_interval α)
(n : ℕ) :
@[simp]
theorem
nonempty_interval.pure_pow
{α : Type u_2}
[monoid α]
[preorder α]
[covariant_class α α has_mul.mul has_le.le]
[covariant_class α α (function.swap has_mul.mul) has_le.le]
(a : α)
(n : ℕ) :
nonempty_interval.pure a ^ n = nonempty_interval.pure (a ^ n)
@[simp]
theorem
nonempty_interval.pure_nsmul
{α : Type u_2}
[add_monoid α]
[preorder α]
[covariant_class α α has_add.add has_le.le]
[covariant_class α α (function.swap has_add.add) has_le.le]
(a : α)
(n : ℕ) :
n • nonempty_interval.pure a = nonempty_interval.pure (n • a)
@[protected, instance]
Equations
- nonempty_interval.comm_monoid = function.injective.comm_monoid nonempty_interval.to_prod nonempty_interval.comm_monoid._proof_1 nonempty_interval.comm_monoid._proof_2 nonempty_interval.comm_monoid._proof_3 nonempty_interval.comm_monoid._proof_4
@[protected, instance]
Equations
- nonempty_interval.add_comm_monoid = function.injective.add_comm_monoid nonempty_interval.to_prod nonempty_interval.add_comm_monoid._proof_1 nonempty_interval.add_comm_monoid._proof_2 nonempty_interval.add_comm_monoid._proof_3 nonempty_interval.add_comm_monoid._proof_4
@[protected, instance]
Equations
- interval.add_zero_class = {zero := 0, add := has_add.add interval.has_add, zero_add := _, add_zero := _}
@[protected, instance]
Equations
- interval.mul_one_class = {one := 1, mul := has_mul.mul interval.has_mul, one_mul := _, mul_one := _}
@[protected, instance]
Equations
- interval.comm_monoid = {mul := mul_one_class.mul interval.mul_one_class, mul_assoc := _, one := mul_one_class.one interval.mul_one_class, one_mul := _, mul_one := _, npow := monoid.npow._default mul_one_class.one mul_one_class.mul interval.comm_monoid._proof_4 interval.comm_monoid._proof_5, npow_zero' := _, npow_succ' := _, mul_comm := _}
@[protected, instance]
Equations
- interval.add_comm_monoid = {add := add_zero_class.add interval.add_zero_class, add_assoc := _, zero := add_zero_class.zero interval.add_zero_class, zero_add := _, add_zero := _, nsmul := add_monoid.nsmul._default add_zero_class.zero add_zero_class.add interval.add_comm_monoid._proof_4 interval.add_comm_monoid._proof_5, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[simp]
theorem
nonempty_interval.coe_nsmul_interval
{α : Type u_2}
[ordered_add_comm_monoid α]
(s : nonempty_interval α)
(n : ℕ) :
@[simp]
theorem
nonempty_interval.coe_pow_interval
{α : Type u_2}
[ordered_comm_monoid α]
(s : nonempty_interval α)
(n : ℕ) :
Subtraction #
Subtraction is defined more generally than division so that it applies to ℕ
(and has_ordered_div
is not a thing and probably should not become one).
@[protected, instance]
def
nonempty_interval.has_sub
{α : Type u_2}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
[covariant_class α α has_add.add has_le.le] :
@[protected, instance]
def
interval.has_sub
{α : Type u_2}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
[covariant_class α α has_add.add has_le.le] :
Equations
@[simp]
theorem
nonempty_interval.fst_sub
{α : Type u_2}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
[covariant_class α α has_add.add has_le.le]
(s t : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.snd_sub
{α : Type u_2}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
[covariant_class α α has_add.add has_le.le]
(s t : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.coe_sub_interval
{α : Type u_2}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
[covariant_class α α has_add.add has_le.le]
(s t : nonempty_interval α) :
theorem
nonempty_interval.sub_mem_sub
{α : Type u_2}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
[covariant_class α α has_add.add has_le.le]
(s t : nonempty_interval α)
{a b : α}
(ha : a ∈ s)
(hb : b ∈ t) :
@[simp]
theorem
nonempty_interval.pure_sub_pure
{α : Type u_2}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
[covariant_class α α has_add.add has_le.le]
(a b : α) :
@[simp]
theorem
interval.bot_sub
{α : Type u_2}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
[covariant_class α α has_add.add has_le.le]
(t : interval α) :
@[simp]
theorem
interval.sub_bot
{α : Type u_2}
[preorder α]
[add_comm_semigroup α]
[has_sub α]
[has_ordered_sub α]
[covariant_class α α has_add.add has_le.le]
(s : interval α) :
Division in ordered groups #
Note that this division does not apply to ℚ
or ℝ
.
@[protected, instance]
def
nonempty_interval.has_div
{α : Type u_2}
[preorder α]
[comm_group α]
[covariant_class α α has_mul.mul has_le.le] :
@[protected, instance]
def
interval.has_div
{α : Type u_2}
[preorder α]
[comm_group α]
[covariant_class α α has_mul.mul has_le.le] :
Equations
@[simp]
theorem
nonempty_interval.fst_div
{α : Type u_2}
[preorder α]
[comm_group α]
[covariant_class α α has_mul.mul has_le.le]
(s t : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.snd_div
{α : Type u_2}
[preorder α]
[comm_group α]
[covariant_class α α has_mul.mul has_le.le]
(s t : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.coe_div_interval
{α : Type u_2}
[preorder α]
[comm_group α]
[covariant_class α α has_mul.mul has_le.le]
(s t : nonempty_interval α) :
theorem
nonempty_interval.div_mem_div
{α : Type u_2}
[preorder α]
[comm_group α]
[covariant_class α α has_mul.mul has_le.le]
(s t : nonempty_interval α)
(a b : α)
(ha : a ∈ s)
(hb : b ∈ t) :
@[simp]
theorem
nonempty_interval.pure_div_pure
{α : Type u_2}
[preorder α]
[comm_group α]
[covariant_class α α has_mul.mul has_le.le]
(a b : α) :
@[simp]
theorem
interval.bot_div
{α : Type u_2}
[preorder α]
[comm_group α]
[covariant_class α α has_mul.mul has_le.le]
(t : interval α) :
@[simp]
theorem
interval.div_bot
{α : Type u_2}
[preorder α]
[comm_group α]
[covariant_class α α has_mul.mul has_le.le]
(s : interval α) :
Negation/inversion #
@[protected, instance]
Equations
- nonempty_interval.has_inv = {inv := λ (s : nonempty_interval α), {to_prod := ((s.to_prod.snd)⁻¹, (s.to_prod.fst)⁻¹), fst_le_snd := _}}
@[protected, instance]
Equations
- nonempty_interval.has_neg = {neg := λ (s : nonempty_interval α), {to_prod := (-s.to_prod.snd, -s.to_prod.fst), fst_le_snd := _}}
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem
nonempty_interval.fst_neg
{α : Type u_2}
[ordered_add_comm_group α]
(s : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.snd_neg
{α : Type u_2}
[ordered_add_comm_group α]
(s : nonempty_interval α) :
@[simp]
@[simp]
theorem
nonempty_interval.coe_inv_interval
{α : Type u_2}
[ordered_comm_group α]
(s : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.coe_neg_interval
{α : Type u_2}
[ordered_add_comm_group α]
(s : nonempty_interval α) :
theorem
nonempty_interval.inv_mem_inv
{α : Type u_2}
[ordered_comm_group α]
(s : nonempty_interval α)
(a : α)
(ha : a ∈ s) :
theorem
nonempty_interval.neg_mem_neg
{α : Type u_2}
[ordered_add_comm_group α]
(s : nonempty_interval α)
(a : α)
(ha : a ∈ s) :
@[simp]
@[simp]
@[protected]
theorem
nonempty_interval.mul_eq_one_iff
{α : Type u_2}
[ordered_comm_group α]
{s t : nonempty_interval α} :
@[protected]
theorem
nonempty_interval.add_eq_zero_iff
{α : Type u_2}
[ordered_add_comm_group α]
{s t : nonempty_interval α} :
@[protected, instance]
Equations
- nonempty_interval.subtraction_comm_monoid = {add := add_comm_monoid.add nonempty_interval.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero nonempty_interval.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul nonempty_interval.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg nonempty_interval.has_neg, sub := has_sub.sub nonempty_interval.has_sub, sub_eq_add_neg := _, zsmul := subtraction_monoid.zsmul._default add_comm_monoid.add nonempty_interval.subtraction_comm_monoid._proof_8 add_comm_monoid.zero nonempty_interval.subtraction_comm_monoid._proof_9 nonempty_interval.subtraction_comm_monoid._proof_10 add_comm_monoid.nsmul nonempty_interval.subtraction_comm_monoid._proof_11 nonempty_interval.subtraction_comm_monoid._proof_12 has_neg.neg, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _, add_comm := _}
@[protected, instance]
Equations
- nonempty_interval.division_comm_monoid = {mul := comm_monoid.mul nonempty_interval.comm_monoid, mul_assoc := _, one := comm_monoid.one nonempty_interval.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow nonempty_interval.comm_monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv nonempty_interval.has_inv, div := has_div.div nonempty_interval.has_div, div_eq_mul_inv := _, zpow := division_monoid.zpow._default comm_monoid.mul nonempty_interval.division_comm_monoid._proof_7 comm_monoid.one nonempty_interval.division_comm_monoid._proof_8 nonempty_interval.division_comm_monoid._proof_9 comm_monoid.npow nonempty_interval.division_comm_monoid._proof_10 nonempty_interval.division_comm_monoid._proof_11 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _, mul_comm := _}
@[protected]
@[protected]
@[protected, instance]
Equations
- interval.subtraction_comm_monoid = {add := add_comm_monoid.add interval.add_comm_monoid, add_assoc := _, zero := add_comm_monoid.zero interval.add_comm_monoid, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul interval.add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg interval.has_neg, sub := has_sub.sub interval.has_sub, sub_eq_add_neg := _, zsmul := subtraction_monoid.zsmul._default add_comm_monoid.add interval.subtraction_comm_monoid._proof_8 add_comm_monoid.zero interval.subtraction_comm_monoid._proof_9 interval.subtraction_comm_monoid._proof_10 add_comm_monoid.nsmul interval.subtraction_comm_monoid._proof_11 interval.subtraction_comm_monoid._proof_12 has_neg.neg, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, neg_neg := _, neg_add_rev := _, neg_eq_of_add := _, add_comm := _}
@[protected, instance]
Equations
- interval.division_comm_monoid = {mul := comm_monoid.mul interval.comm_monoid, mul_assoc := _, one := comm_monoid.one interval.comm_monoid, one_mul := _, mul_one := _, npow := comm_monoid.npow interval.comm_monoid, npow_zero' := _, npow_succ' := _, inv := has_inv.inv interval.has_inv, div := has_div.div interval.has_div, div_eq_mul_inv := _, zpow := division_monoid.zpow._default comm_monoid.mul interval.division_comm_monoid._proof_7 comm_monoid.one interval.division_comm_monoid._proof_8 interval.division_comm_monoid._proof_9 comm_monoid.npow interval.division_comm_monoid._proof_10 interval.division_comm_monoid._proof_11 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, inv_inv := _, mul_inv_rev := _, inv_eq_of_mul := _, mul_comm := _}
def
nonempty_interval.length
{α : Type u_2}
[ordered_add_comm_group α]
(s : nonempty_interval α) :
α
The length of an interval is its first component minus its second component. This measures the accuracy of the approximation by an interval.
@[simp]
theorem
nonempty_interval.length_nonneg
{α : Type u_2}
[ordered_add_comm_group α]
(s : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.length_pure
{α : Type u_2}
[ordered_add_comm_group α]
(a : α) :
(nonempty_interval.pure a).length = 0
@[simp]
@[simp]
theorem
nonempty_interval.length_neg
{α : Type u_2}
[ordered_add_comm_group α]
(s : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.length_add
{α : Type u_2}
[ordered_add_comm_group α]
(s t : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.length_sub
{α : Type u_2}
[ordered_add_comm_group α]
(s t : nonempty_interval α) :
@[simp]
theorem
nonempty_interval.length_sum
{ι : Type u_1}
{α : Type u_2}
[ordered_add_comm_group α]
(f : ι → nonempty_interval α)
(s : finset ι) :
@[simp]
@[simp]
theorem
interval.length_pure
{α : Type u_2}
[ordered_add_comm_group α]
(a : α) :
(interval.pure a).length = 0
@[simp]
@[simp]