Documentation

Mathlib.Algebra.Order.Interval.Basic

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 #

@[implicit_reducible]

instance instOneNonemptyInterval {α : Type u_2} [Preorder α] [One α] :

One (NonemptyInterval α)

@[implicit_reducible]

instance instZeroNonemptyInterval {α : Type u_2} [Preorder α] [Zero α] :

Zero (NonemptyInterval α)

@[simp]

theorem NonemptyInterval.toProd_one {α : Type u_2} [Preorder α] [One α] :

toProd 1 = 1

@[simp]

theorem NonemptyInterval.toProd_zero {α : Type u_2} [Preorder α] [Zero α] :

toProd 0 = 0

theorem NonemptyInterval.fst_one {α : Type u_2} [Preorder α] [One α] :

(toProd 1).1 = 1

theorem NonemptyInterval.fst_zero {α : Type u_2} [Preorder α] [Zero α] :

(toProd 0).1 = 0

theorem NonemptyInterval.snd_one {α : Type u_2} [Preorder α] [One α] :

(toProd 1).2 = 1

theorem NonemptyInterval.snd_zero {α : Type u_2} [Preorder α] [Zero α] :

(toProd 0).2 = 0

@[simp]

theorem NonemptyInterval.coe_one_interval {α : Type u_2} [Preorder α] [One α] :

↑1 = 1

@[simp]

theorem NonemptyInterval.coe_zero_interval {α : Type u_2} [Preorder α] [Zero α] :

↑0 = 0

@[simp]

theorem NonemptyInterval.pure_one {α : Type u_2} [Preorder α] [One α] :

pure 1 = 1

@[simp]

theorem NonemptyInterval.pure_zero {α : Type u_2} [Preorder α] [Zero α] :

pure 0 = 0

@[simp]

theorem Interval.pure_one {α : Type u_2} [Preorder α] [One α] :

pure 1 = 1

@[simp]

theorem Interval.pure_zero {α : Type u_2} [Preorder α] [Zero α] :

pure 0 = 0

theorem Interval.one_ne_bot {α : Type u_2} [Preorder α] [One α] :

1 ≠ ⊥

theorem Interval.zero_ne_bot {α : Type u_2} [Preorder α] [Zero α] :

0 ≠ ⊥

theorem Interval.bot_ne_one {α : Type u_2} [Preorder α] [One α] :

⊥ ≠ 1

theorem Interval.bot_ne_zero {α : Type u_2} [Preorder α] [Zero α] :

⊥ ≠ 0

@[simp]

theorem NonemptyInterval.coe_one {α : Type u_2} [PartialOrder α] [One α] :

↑1 = 1

@[simp]

theorem NonemptyInterval.coe_zero {α : Type u_2} [PartialOrder α] [Zero α] :

↑0 = 0

theorem NonemptyInterval.one_mem_one {α : Type u_2} [PartialOrder α] [One α] :

1 ∈ 1

theorem NonemptyInterval.zero_mem_zero {α : Type u_2} [PartialOrder α] [Zero α] :

0 ∈ 0

@[simp]

theorem Interval.coe_one {α : Type u_2} [PartialOrder α] [One α] :

↑1 = 1

@[simp]

theorem Interval.coe_zero {α : Type u_2} [PartialOrder α] [Zero α] :

↑0 = 0

theorem Interval.one_mem_one {α : Type u_2} [PartialOrder α] [One α] :

1 ∈ 1

theorem Interval.zero_mem_zero {α : Type u_2} [PartialOrder α] [Zero α] :

0 ∈ 0

Addition/multiplication #

Note that this multiplication does not apply to ℚ or ℝ.

@[implicit_reducible]

instance instMulNonemptyInterval {α : Type u_2} [Preorder α] [Mul α] [MulLeftMono α] [MulRightMono α] :

Mul (NonemptyInterval α)

@[implicit_reducible]

instance instAddNonemptyInterval {α : Type u_2} [Preorder α] [Add α] [AddLeftMono α] [AddRightMono α] :

Add (NonemptyInterval α)

@[implicit_reducible]

instance instMulInterval {α : Type u_2} [Preorder α] [Mul α] [MulLeftMono α] [MulRightMono α] :

Mul (Interval α)

@[implicit_reducible]

instance instAddInterval {α : Type u_2} [Preorder α] [Add α] [AddLeftMono α] [AddRightMono α] :

Add (Interval α)

@[simp]

theorem NonemptyInterval.toProd_mul {α : Type u_2} [Preorder α] [Mul α] [MulLeftMono α] [MulRightMono α] (s t : NonemptyInterval α) :

(s * t).toProd = s.toProd * t.toProd

@[simp]

theorem NonemptyInterval.toProd_add {α : Type u_2} [Preorder α] [Add α] [AddLeftMono α] [AddRightMono α] (s t : NonemptyInterval α) :

(s + t).toProd = s.toProd + t.toProd

theorem NonemptyInterval.fst_mul {α : Type u_2} [Preorder α] [Mul α] [MulLeftMono α] [MulRightMono α] (s t : NonemptyInterval α) :

(s * t).toProd.1 = s.toProd.1 * t.toProd.1

theorem NonemptyInterval.fst_add {α : Type u_2} [Preorder α] [Add α] [AddLeftMono α] [AddRightMono α] (s t : NonemptyInterval α) :

(s + t).toProd.1 = s.toProd.1 + t.toProd.1

theorem NonemptyInterval.snd_mul {α : Type u_2} [Preorder α] [Mul α] [MulLeftMono α] [MulRightMono α] (s t : NonemptyInterval α) :

(s * t).toProd.2 = s.toProd.2 * t.toProd.2

theorem NonemptyInterval.snd_add {α : Type u_2} [Preorder α] [Add α] [AddLeftMono α] [AddRightMono α] (s t : NonemptyInterval α) :

(s + t).toProd.2 = s.toProd.2 + t.toProd.2

@[simp]

theorem NonemptyInterval.coe_mul_interval {α : Type u_2} [Preorder α] [Mul α] [MulLeftMono α] [MulRightMono α] (s t : NonemptyInterval α) :

↑(s * t) = ↑s * ↑t

@[simp]

theorem NonemptyInterval.coe_add_interval {α : Type u_2} [Preorder α] [Add α] [AddLeftMono α] [AddRightMono α] (s t : NonemptyInterval α) :

↑(s + t) = ↑s + ↑t

@[simp]

theorem NonemptyInterval.pure_mul_pure {α : Type u_2} [Preorder α] [Mul α] [MulLeftMono α] [MulRightMono α] (a b : α) :

pure a * pure b = pure (a * b)

@[simp]

theorem NonemptyInterval.pure_add_pure {α : Type u_2} [Preorder α] [Add α] [AddLeftMono α] [AddRightMono α] (a b : α) :

pure a + pure b = pure (a + b)

@[simp]

theorem Interval.bot_mul {α : Type u_2} [Preorder α] [Mul α] [MulLeftMono α] [MulRightMono α] (t : Interval α) :

⊥ * t = ⊥

@[simp]

theorem Interval.bot_add {α : Type u_2} [Preorder α] [Add α] [AddLeftMono α] [AddRightMono α] (t : Interval α) :

⊥ + t = ⊥

@[simp]

theorem Interval.mul_bot {α : Type u_2} [Preorder α] [Mul α] [MulLeftMono α] [MulRightMono α] (s : Interval α) :

s * ⊥ = ⊥

theorem Interval.add_bot {α : Type u_2} [Preorder α] [Add α] [AddLeftMono α] [AddRightMono α] (s : Interval α) :

s + ⊥ = ⊥

Powers #

@[implicit_reducible]

instance NonemptyInterval.instPow {α : Type u_2} [Monoid α] [Preorder α] [MulLeftMono α] [MulRightMono α] :

Pow (NonemptyInterval α) ℕ

@[implicit_reducible]

instance NonemptyInterval.instNSMul {α : Type u_2} [AddMonoid α] [Preorder α] [AddLeftMono α] [AddRightMono α] :

SMul ℕ (NonemptyInterval α)

@[simp]

theorem NonemptyInterval.toProd_pow {α : Type u_2} [Monoid α] [Preorder α] [MulLeftMono α] [MulRightMono α] (s : NonemptyInterval α) (n : ℕ) :

(s ^ n).toProd = s.toProd ^ n

@[simp]

theorem NonemptyInterval.toProd_nsmul {α : Type u_2} [AddMonoid α] [Preorder α] [AddLeftMono α] [AddRightMono α] (s : NonemptyInterval α) (n : ℕ) :

(n • s).toProd = n • s.toProd

theorem NonemptyInterval.fst_pow {α : Type u_2} [Monoid α] [Preorder α] [MulLeftMono α] [MulRightMono α] (s : NonemptyInterval α) (n : ℕ) :

(s ^ n).toProd.1 = s.toProd.1 ^ n

theorem NonemptyInterval.fst_nsmul {α : Type u_2} [AddMonoid α] [Preorder α] [AddLeftMono α] [AddRightMono α] (s : NonemptyInterval α) (n : ℕ) :

(n • s).toProd.1 = n • s.toProd.1

theorem NonemptyInterval.snd_pow {α : Type u_2} [Monoid α] [Preorder α] [MulLeftMono α] [MulRightMono α] (s : NonemptyInterval α) (n : ℕ) :

(s ^ n).toProd.2 = s.toProd.2 ^ n

theorem NonemptyInterval.snd_nsmul {α : Type u_2} [AddMonoid α] [Preorder α] [AddLeftMono α] [AddRightMono α] (s : NonemptyInterval α) (n : ℕ) :

(n • s).toProd.2 = n • s.toProd.2

@[simp]

theorem NonemptyInterval.pure_pow {α : Type u_2} [Monoid α] [Preorder α] [MulLeftMono α] [MulRightMono α] (a : α) (n : ℕ) :

pure a ^ n = pure (a ^ n)

@[simp]

theorem NonemptyInterval.pure_nsmul {α : Type u_2} [AddMonoid α] [Preorder α] [AddLeftMono α] [AddRightMono α] (a : α) (n : ℕ) :

n • pure a = pure (n • a)

@[implicit_reducible]

instance NonemptyInterval.commMonoid {α : Type u_2} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] :

CommMonoid (NonemptyInterval α)

@[implicit_reducible]

instance NonemptyInterval.addCommMonoid {α : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] :

AddCommMonoid (NonemptyInterval α)

@[implicit_reducible]

instance Interval.mulOneClass {α : Type u_2} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] :

MulOneClass (Interval α)

@[implicit_reducible]

instance Interval.addZeroClass {α : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] :

AddZeroClass (Interval α)

@[implicit_reducible]

instance Interval.commMonoid {α : Type u_2} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] :

CommMonoid (Interval α)

@[implicit_reducible]

instance Interval.addCommMonoid {α : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] :

AddCommMonoid (Interval α)

@[simp]

theorem NonemptyInterval.coe_pow_interval {α : Type u_2} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] (s : NonemptyInterval α) (n : ℕ) :

↑(s ^ n) = ↑s ^ n

theorem NonemptyInterval.coe_nsmul_interval {α : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] (s : NonemptyInterval α) (n : ℕ) :

↑(n • s) = n • ↑s

theorem Interval.bot_pow {α : Type u_2} [CommMonoid α] [Preorder α] [IsOrderedMonoid α] {n : ℕ} :

n ≠ 0 → ⊥ ^ n = ⊥

theorem Interval.bot_nsmul {α : Type u_2} [AddCommMonoid α] [Preorder α] [IsOrderedAddMonoid α] {n : ℕ} :

n ≠ 0 → n • ⊥ = ⊥

Semiring structure #

When α is a canonically OrderedCommSemiring, the previous + and * on NonemptyInterval α form a CommSemiring.

@[implicit_reducible]

instance NonemptyInterval.instNatCast {α : Type u_2} [Preorder α] [NatCast α] :

NatCast (NonemptyInterval α)

theorem NonemptyInterval.fst_natCast {α : Type u_2} [Preorder α] [NatCast α] (n : ℕ) :

(↑n).toProd.1 = ↑n

theorem NonemptyInterval.snd_natCast {α : Type u_2} [Preorder α] [NatCast α] (n : ℕ) :

(↑n).toProd.2 = ↑n

@[simp]

theorem NonemptyInterval.pure_natCast {α : Type u_2} [Preorder α] [NatCast α] (n : ℕ) :

pure ↑n = ↑n

@[implicit_reducible]

instance NonemptyInterval.instCommSemiringOfCanonicallyOrderedAdd {α : Type u_2} [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] :

CommSemiring (NonemptyInterval α)

Subtraction #

Subtraction is defined more generally than division so that it applies to ℕ (and OrderedDiv is not a thing and probably should not become one).

However, this means that we can't use to_additive in this section.

@[implicit_reducible]

instance instSubNonemptyInterval {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] :

Sub (NonemptyInterval α)

@[implicit_reducible]

instance instSubInterval {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] :

Sub (Interval α)

@[simp]

theorem NonemptyInterval.fst_sub {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] (s t : NonemptyInterval α) :

(s - t).toProd.1 = s.toProd.1 - t.toProd.2

@[simp]

theorem NonemptyInterval.snd_sub {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] (s t : NonemptyInterval α) :

(s - t).toProd.2 = s.toProd.2 - t.toProd.1

@[simp]

theorem NonemptyInterval.coe_sub_interval {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] (s t : NonemptyInterval α) :

↑(s - t) = ↑s - ↑t

theorem NonemptyInterval.sub_mem_sub {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] (s t : NonemptyInterval α) {a b : α} (ha : a ∈ s) (hb : b ∈ t) :

a - b ∈ s - t

@[simp]

theorem NonemptyInterval.pure_sub_pure {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] (a b : α) :

pure a - pure b = pure (a - b)

@[simp]

theorem Interval.bot_sub {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] (t : Interval α) :

⊥ - t = ⊥

@[simp]

theorem Interval.sub_bot {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [AddLeftMono α] (s : Interval α) :

s - ⊥ = ⊥

Division in ordered groups #

Note that this division does not apply to ℚ or ℝ.

@[implicit_reducible]

instance instDivNonemptyInterval {α : Type u_2} [Preorder α] [CommGroup α] [MulLeftMono α] :

Div (NonemptyInterval α)

@[implicit_reducible]

instance instDivInterval {α : Type u_2} [Preorder α] [CommGroup α] [MulLeftMono α] :

Div (Interval α)

@[simp]

theorem NonemptyInterval.fst_div {α : Type u_2} [Preorder α] [CommGroup α] [MulLeftMono α] (s t : NonemptyInterval α) :

(s / t).toProd.1 = s.toProd.1 / t.toProd.2

@[simp]

theorem NonemptyInterval.snd_div {α : Type u_2} [Preorder α] [CommGroup α] [MulLeftMono α] (s t : NonemptyInterval α) :

(s / t).toProd.2 = s.toProd.2 / t.toProd.1

@[simp]

theorem NonemptyInterval.coe_div_interval {α : Type u_2} [Preorder α] [CommGroup α] [MulLeftMono α] (s t : NonemptyInterval α) :

↑(s / t) = ↑s / ↑t

theorem NonemptyInterval.div_mem_div {α : Type u_2} [Preorder α] [CommGroup α] [MulLeftMono α] (s t : NonemptyInterval α) (a b : α) (ha : a ∈ s) (hb : b ∈ t) :

a / b ∈ s / t

@[simp]

theorem NonemptyInterval.pure_div_pure {α : Type u_2} [Preorder α] [CommGroup α] [MulLeftMono α] (a b : α) :

pure a / pure b = pure (a / b)

@[simp]

theorem Interval.bot_div {α : Type u_2} [Preorder α] [CommGroup α] [MulLeftMono α] (t : Interval α) :

⊥ / t = ⊥

@[simp]

theorem Interval.div_bot {α : Type u_2} [Preorder α] [CommGroup α] [MulLeftMono α] (s : Interval α) :

s / ⊥ = ⊥

Negation/inversion #

@[implicit_reducible]

instance instInvNonemptyInterval {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

Inv (NonemptyInterval α)

@[implicit_reducible]

instance instNegNonemptyInterval {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

Neg (NonemptyInterval α)

@[implicit_reducible]

instance instInvInterval {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

Inv (Interval α)

@[implicit_reducible]

instance instNegInterval {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

Neg (Interval α)

@[simp]

theorem NonemptyInterval.fst_inv {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s : NonemptyInterval α) :

s⁻¹.toProd.1 = s.toProd.2⁻¹

@[simp]

theorem NonemptyInterval.fst_neg {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s : NonemptyInterval α) :

(-s).toProd.1 = -s.toProd.2

@[simp]

theorem NonemptyInterval.snd_inv {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s : NonemptyInterval α) :

s⁻¹.toProd.2 = s.toProd.1⁻¹

@[simp]

theorem NonemptyInterval.snd_neg {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s : NonemptyInterval α) :

(-s).toProd.2 = -s.toProd.1

@[simp]

theorem NonemptyInterval.coe_inv_interval {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s : NonemptyInterval α) :

↑s⁻¹ = (↑s)⁻¹

@[simp]

theorem NonemptyInterval.coe_neg_interval {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s : NonemptyInterval α) :

↑(-s) = -↑s

theorem NonemptyInterval.inv_mem_inv {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (s : NonemptyInterval α) (a : α) (ha : a ∈ s) :

a⁻¹ ∈ s⁻¹

theorem NonemptyInterval.neg_mem_neg {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s : NonemptyInterval α) (a : α) (ha : a ∈ s) :

-a ∈ -s

@[simp]

theorem NonemptyInterval.inv_pure {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] (a : α) :

(pure a)⁻¹ = pure a⁻¹

@[simp]

theorem NonemptyInterval.neg_pure {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (a : α) :

-pure a = pure (-a)

@[simp]

theorem Interval.inv_bot {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

@[simp]

theorem Interval.neg_bot {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

theorem NonemptyInterval.mul_eq_one_iff {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s t : NonemptyInterval α} :

s * t = 1 ↔ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1

theorem NonemptyInterval.add_eq_zero_iff {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s t : NonemptyInterval α} :

s + t = 0 ↔ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a + b = 0

@[implicit_reducible]

instance NonemptyInterval.subtractionCommMonoid {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

SubtractionCommMonoid (NonemptyInterval α)

@[implicit_reducible]

instance NonemptyInterval.divisionCommMonoid {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

DivisionCommMonoid (NonemptyInterval α)

theorem Interval.mul_eq_one_iff {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] {s t : Interval α} :

s * t = 1 ↔ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a * b = 1

theorem Interval.add_eq_zero_iff {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] {s t : Interval α} :

s + t = 0 ↔ ∃ (a : α) (b : α), s = pure a ∧ t = pure b ∧ a + b = 0

@[implicit_reducible]

instance Interval.subtractionCommMonoid {α : Type u} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :

SubtractionCommMonoid (Interval α)

@[implicit_reducible]

instance Interval.divisionCommMonoid {α : Type u_2} [CommGroup α] [PartialOrder α] [IsOrderedMonoid α] :

DivisionCommMonoid (Interval α)

def NonemptyInterval.length {α : Type u_2} [AddCommGroup α] [PartialOrder α] (s : NonemptyInterval α) :

α

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

Instances For

@[simp]

theorem NonemptyInterval.length_nonneg {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s : NonemptyInterval α) :

@[simp]

theorem NonemptyInterval.length_pure {α : Type u_2} [AddCommGroup α] [PartialOrder α] (a : α) :

(pure a).length = 0

@[simp]

theorem NonemptyInterval.length_zero {α : Type u_2} [AddCommGroup α] [PartialOrder α] :

length 0 = 0

@[simp]

theorem NonemptyInterval.length_neg {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s : NonemptyInterval α) :

(-s).length = s.length

@[simp]

theorem NonemptyInterval.length_add {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : NonemptyInterval α) :

(s + t).length = s.length + t.length

@[simp]

theorem NonemptyInterval.length_sub {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : NonemptyInterval α) :

(s - t).length = s.length + t.length

@[simp]

theorem NonemptyInterval.length_sum {ι : Type u_1} {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (f : ι → NonemptyInterval α) (s : Finset ι) :

(∑ i ∈ s, f i).length = ∑ i ∈ s, (f i).length

def Interval.length {α : Type u_2} [AddCommGroup α] [PartialOrder α] :

Interval α → α

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

Instances For

@[simp]

theorem Interval.length_nonneg {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s : Interval α) :

@[simp]

theorem Interval.length_pure {α : Type u_2} [AddCommGroup α] [PartialOrder α] (a : α) :

(pure a).length = 0

@[simp]

theorem Interval.length_zero {α : Type u_2} [AddCommGroup α] [PartialOrder α] :

length 0 = 0

@[simp]

theorem Interval.length_neg {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s : Interval α) :

(-s).length = s.length

theorem Interval.length_add_le {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : Interval α) :

(s + t).length ≤ s.length + t.length

theorem Interval.length_sub_le {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (s t : Interval α) :

(s - t).length ≤ s.length + t.length

theorem Interval.length_sum_le {ι : Type u_1} {α : Type u_2} [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] (f : ι → Interval α) (s : Finset ι) :

(∑ i ∈ s, f i).length ≤ ∑ i ∈ s, (f i).length

def Mathlib.Meta.Positivity.evalNonemptyIntervalLength :

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

Instances For

def Mathlib.Meta.Positivity.evalIntervalLength :

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

Instances For