mathlib documentation

algebra.order.interval

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 hsve not yet integrated these with the rest of the library.

One/zero #

@[protected, instance]
Equations
@[protected, instance]
def interval.has_one {α : Type u_2} [preorder α] [has_one α] :
Equations
@[protected, instance]
def interval.has_zero {α : Type u_2} [preorder α] [has_zero α] :
Equations
@[simp]
theorem nonempty_interval.to_prod_one {α : Type u_2} [preorder α] [has_one α] :
@[simp]
theorem nonempty_interval.to_prod_zero {α : Type u_2} [preorder α] [has_zero α] :
theorem nonempty_interval.fst_one {α : Type u_2} [preorder α] [has_one α] :
theorem nonempty_interval.fst_zero {α : Type u_2} [preorder α] [has_zero α] :
theorem nonempty_interval.snd_zero {α : Type u_2} [preorder α] [has_zero α] :
theorem nonempty_interval.snd_one {α : Type u_2} [preorder α] [has_one α] :
@[simp, norm_cast]
theorem nonempty_interval.coe_one_interval {α : Type u_2} [preorder α] [has_one α] :
1 = 1
@[simp, norm_cast]
theorem nonempty_interval.coe_zero_interval {α : Type u_2} [preorder α] [has_zero α] :
0 = 0
@[simp]
@[simp]
@[simp]
theorem interval.pure_zero {α : Type u_2} [preorder α] [has_zero α] :
@[simp]
theorem interval.pure_one {α : Type u_2} [preorder α] [has_one α] :
@[simp]
theorem interval.zero_ne_bot {α : Type u_2} [preorder α] [has_zero α] :
@[simp]
theorem interval.one_ne_bot {α : Type u_2} [preorder α] [has_one α] :
@[simp]
theorem interval.bot_ne_one {α : Type u_2} [preorder α] [has_one α] :
@[simp]
theorem interval.bot_ne_zero {α : Type u_2} [preorder α] [has_zero α] :
@[simp]
theorem nonempty_interval.coe_one {α : Type u_2} [partial_order α] [has_one α] :
1 = 1
@[simp]
theorem nonempty_interval.coe_zero {α : Type u_2} [partial_order α] [has_zero α] :
0 = 0
theorem nonempty_interval.one_mem_one {α : Type u_2} [partial_order α] [has_one α] :
1 1
@[simp]
theorem interval.coe_one {α : Type u_2} [partial_order α] [has_one α] :
1 = 1
@[simp]
theorem interval.coe_zero {α : Type u_2} [partial_order α] [has_zero α] :
0 = 0
theorem interval.one_mem_one {α : Type u_2} [partial_order α] [has_one α] :
1 1
theorem interval.zero_mem_zero {α : Type u_2} [partial_order α] [has_zero α] :
0 0

Addition/multiplication #

Note that this multiplication does not apply to or .

Powers #

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[simp]
theorem nonempty_interval.coe_pow_interval {α : Type u_2} [ordered_comm_monoid α] (s : nonempty_interval α) (n : ) :
(s ^ n) = s ^ n
theorem interval.bot_pow {α : Type u_2} [ordered_comm_monoid α] {n : } (hn : n 0) :
theorem interval.bot_nsmul {α : Type u_2} [ordered_add_comm_monoid α] {n : } (hn : n 0) :

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).

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) :
a - b s - t
@[simp]
@[simp]

Division in ordered groups #

Note that this division does not apply to or .

@[protected, instance]
Equations
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) :
a / b s / t
@[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
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
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) :
-a -s
@[simp]
theorem interval.inv_bot {α : Type u_2} [ordered_comm_group α] :
@[simp]
theorem interval.neg_bot {α : Type u_2} [ordered_add_comm_group α] :
@[protected]
@[protected]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected]
theorem interval.add_eq_zero_iff {α : Type u_2} [ordered_add_comm_group α] {s t : interval α} :
s + t = 0 (a b : α), s = interval.pure a t = interval.pure b a + b = 0
@[protected]
theorem interval.mul_eq_one_iff {α : Type u_2} [ordered_comm_group α] {s t : interval α} :
s * t = 1 (a b : α), s = interval.pure a t = interval.pure b a * b = 1
@[protected, instance]
Equations
@[protected, instance]
Equations

The length of an interval is its first component minus its second component. This measures the accuracy of the approximation by an interval.

Equations
@[simp]
@[simp]
@[simp]
@[simp]
theorem nonempty_interval.length_sum {ι : Type u_1} {α : Type u_2} [ordered_add_comm_group α] (f : ι nonempty_interval α) (s : finset ι) :
(s.sum (λ (i : ι), f i)).length = s.sum (λ (i : ι), (f i).length)
def interval.length {α : Type u_2} [ordered_add_comm_group α] :

The length of an interval is its first component minus its second component. This measures the accuracy of the approximation by an interval.

Equations
@[simp]
theorem interval.length_nonneg {α : Type u_2} [ordered_add_comm_group α] (s : interval α) :
@[simp]
theorem interval.length_pure {α : Type u_2} [ordered_add_comm_group α] (a : α) :
@[simp]
theorem interval.length_zero {α : Type u_2} [ordered_add_comm_group α] :
0.length = 0
@[simp]
theorem interval.length_neg {α : Type u_2} [ordered_add_comm_group α] (s : interval α) :
theorem interval.length_add_le {α : Type u_2} [ordered_add_comm_group α] (s t : interval α) :
theorem interval.length_sub_le {α : Type u_2} [ordered_add_comm_group α] (s t : interval α) :
theorem interval.length_sum_le {ι : Type u_1} {α : Type u_2} [ordered_add_comm_group α] (f : ι interval α) (s : finset ι) :
(s.sum (λ (i : ι), f i)).length s.sum (λ (i : ι), (f i).length)

Extension for the positivity tactic: The length of an interval is always nonnegative.