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

instance instZeroNonemptyIntervalToLE {α : Type u_2} [Preorder α] [Zero α] : Zero (NonemptyInterval α)

Equations

• instZeroNonemptyIntervalToLE = { zero := NonemptyInterval.pure 0 }

instance instOneNonemptyIntervalToLE {α : Type u_2} [Preorder α] [One α] : One (NonemptyInterval α)

Equations

• instOneNonemptyIntervalToLE = { one := NonemptyInterval.pure 1 }

@[simp]

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

@[simp]

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

theorem NonemptyInterval.fst_zero {α : Type u_2} [Preorder α] [Zero α] : 0.toProd.1 = 0

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

theorem NonemptyInterval.snd_zero {α : Type u_2} [Preorder α] [Zero α] : 0.toProd.2 = 0

theorem NonemptyInterval.snd_one {α : Type u_2} [Preorder α] [One α] : 1.toProd.2 = 1

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

Addition/multiplication

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

instance instAddNonemptyIntervalToLE {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : Add (NonemptyInterval α)

Equations

• instAddNonemptyIntervalToLE = { add := fun (s t : NonemptyInterval α) => { toProd := s.toProd + t.toProd, fst_le_snd := ⋯ } }

theorem instAddNonemptyIntervalToLE.proof_1 {α : Type u_1} [Preorder α] [Add α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : s.toProd.1 + t.toProd.1 ≤ s.toProd.2 + t.toProd.2

instance instMulNonemptyIntervalToLE {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : Mul (NonemptyInterval α)

Equations

• instMulNonemptyIntervalToLE = { mul := fun (s t : NonemptyInterval α) => { toProd := s.toProd * t.toProd, fst_le_snd := ⋯ } }

instance instAddIntervalToLE {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : Add (Interval α)

Equations

• instAddIntervalToLE = { add := Option.map₂ fun (x x_1 : NonemptyInterval α) => x + x_1 }

instance instMulIntervalToLE {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : Mul (Interval α)

Equations

• instMulIntervalToLE = { mul := Option.map₂ fun (x x_1 : NonemptyInterval α) => x * x_1 }

@[simp]

theorem NonemptyInterval.toProd_add {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : (s + t).toProd = s.toProd + t.toProd

@[simp]

theorem NonemptyInterval.toProd_mul {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : (s * t).toProd = s.toProd * t.toProd

theorem NonemptyInterval.fst_add {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : (s + t).toProd.1 = s.toProd.1 + t.toProd.1

theorem NonemptyInterval.fst_mul {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : (s * t).toProd.1 = s.toProd.1 * t.toProd.1

theorem NonemptyInterval.snd_add {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : (s + t).toProd.2 = s.toProd.2 + t.toProd.2

theorem NonemptyInterval.snd_mul {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : (s * t).toProd.2 = s.toProd.2 * t.toProd.2

@[simp]

theorem NonemptyInterval.coe_add_interval {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : ↑(s + t) = ↑s + ↑t

@[simp]

theorem NonemptyInterval.coe_mul_interval {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : ↑(s * t) = ↑s * ↑t

@[simp]

theorem NonemptyInterval.pure_add_pure {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : NonemptyInterval.pure a + NonemptyInterval.pure b = NonemptyInterval.pure (a + b)

@[simp]

theorem NonemptyInterval.pure_mul_pure {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : NonemptyInterval.pure a * NonemptyInterval.pure b = NonemptyInterval.pure (a * b)

@[simp]

theorem Interval.bot_add {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (t : Interval α) : ⊥ + t = ⊥

@[simp]

theorem Interval.bot_mul {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (t : Interval α) : ⊥ * t = ⊥

theorem Interval.add_bot {α : Type u_2} [Preorder α] [Add α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : Interval α) : s + ⊥ = ⊥

@[simp]

theorem Interval.mul_bot {α : Type u_2} [Preorder α] [Mul α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : Interval α) : s * ⊥ = ⊥

Powers

instance NonemptyInterval.hasNSMul {α : Type u_2} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : SMul ℕ (NonemptyInterval α)

Equations

• NonemptyInterval.hasNSMul = { smul := fun (n : ℕ) (s : NonemptyInterval α) => { toProd := (n • s.toProd.1, n • s.toProd.2), fst_le_snd := ⋯ } }

instance NonemptyInterval.hasPow {α : Type u_2} [Monoid α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : Pow (NonemptyInterval α) ℕ

Equations

• NonemptyInterval.hasPow = { pow := fun (s : NonemptyInterval α) (n : ℕ) => { toProd := s.toProd ^ n, fst_le_snd := ⋯ } }

@[simp]

theorem NonemptyInterval.toProd_nsmul {α : Type u_2} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (n : ℕ) : (n • s).toProd = n • s.toProd

@[simp]

theorem NonemptyInterval.toProd_pow {α : Type u_2} [Monoid α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (n : ℕ) : (s ^ n).toProd = s.toProd ^ n

theorem NonemptyInterval.fst_nsmul {α : Type u_2} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (n : ℕ) : (n • s).toProd.1 = n • s.toProd.1

theorem NonemptyInterval.fst_pow {α : Type u_2} [Monoid α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (n : ℕ) : (s ^ n).toProd.1 = s.toProd.1 ^ n

theorem NonemptyInterval.snd_nsmul {α : Type u_2} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (n : ℕ) : (n • s).toProd.2 = n • s.toProd.2

theorem NonemptyInterval.snd_pow {α : Type u_2} [Monoid α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (n : ℕ) : (s ^ n).toProd.2 = s.toProd.2 ^ n

@[simp]

theorem NonemptyInterval.pure_nsmul {α : Type u_2} [AddMonoid α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (n : ℕ) : n • NonemptyInterval.pure a = NonemptyInterval.pure (n • a)

@[simp]

theorem NonemptyInterval.pure_pow {α : Type u_2} [Monoid α] [Preorder α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] [CovariantClass α α (Function.swap fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (n : ℕ) : NonemptyInterval.pure a ^ n = NonemptyInterval.pure (a ^ n)

theorem NonemptyInterval.addCommMonoid.proof_2 {α : Type u_1} [OrderedAddCommMonoid α] : 0.toProd = 0

theorem NonemptyInterval.addCommMonoid.proof_4 {α : Type u_1} [OrderedAddCommMonoid α] (s : NonemptyInterval α) (n : ℕ) : (n • s).toProd = n • s.toProd

theorem NonemptyInterval.addCommMonoid.proof_1 {α : Type u_1} [OrderedAddCommMonoid α] : Function.Injective NonemptyInterval.toProd

theorem NonemptyInterval.addCommMonoid.proof_3 {α : Type u_1} [OrderedAddCommMonoid α] (s : NonemptyInterval α) (t : NonemptyInterval α) : (s + t).toProd = s.toProd + t.toProd

instance NonemptyInterval.addCommMonoid {α : Type u_2} [OrderedAddCommMonoid α] : AddCommMonoid (NonemptyInterval α)

Equations

• NonemptyInterval.addCommMonoid = Function.Injective.addCommMonoid NonemptyInterval.toProd ⋯ ⋯ ⋯ ⋯

instance NonemptyInterval.commMonoid {α : Type u_2} [OrderedCommMonoid α] : CommMonoid (NonemptyInterval α)

Equations

• NonemptyInterval.commMonoid = Function.Injective.commMonoid NonemptyInterval.toProd ⋯ ⋯ ⋯ ⋯

instance Interval.addZeroClass {α : Type u_2} [OrderedAddCommMonoid α] : AddZeroClass (Interval α)

Equations

• Interval.addZeroClass = AddZeroClass.mk ⋯ ⋯

theorem Interval.addZeroClass.proof_2 {α : Type u_1} [OrderedAddCommMonoid α] (s : Interval α) : Option.map₂ (fun (x x_1 : NonemptyInterval α) => x + x_1) s (some 0) = s

theorem Interval.addZeroClass.proof_1 {α : Type u_1} [OrderedAddCommMonoid α] (s : Interval α) : Option.map₂ (fun (x x_1 : NonemptyInterval α) => x + x_1) (some 0) s = s

instance Interval.mulOneClass {α : Type u_2} [OrderedCommMonoid α] : MulOneClass (Interval α)

Equations

• Interval.mulOneClass = MulOneClass.mk ⋯ ⋯

theorem Interval.addCommMonoid.proof_3 {α : Type u_1} [OrderedAddCommMonoid α] (a : Interval α) : a + 0 = a

theorem Interval.addCommMonoid.proof_2 {α : Type u_1} [OrderedAddCommMonoid α] (a : Interval α) : 0 + a = a

theorem Interval.addCommMonoid.proof_4 {α : Type u_1} [OrderedAddCommMonoid α] : ∀ (x : Interval α), nsmulRec 0 x = nsmulRec 0 x

theorem Interval.addCommMonoid.proof_1 {α : Type u_1} [OrderedAddCommMonoid α] : ∀ (x x_1 x_2 : Interval α), Option.map₂ (fun (x x_3 : NonemptyInterval α) => x + x_3) (Option.map₂ (fun (x x_3 : NonemptyInterval α) => x + x_3) x x_1) x_2 = Option.map₂ (fun (x x_3 : NonemptyInterval α) => x + x_3) x (Option.map₂ (fun (x x_3 : NonemptyInterval α) => x + x_3) x_1 x_2)

theorem Interval.addCommMonoid.proof_6 {α : Type u_1} [OrderedAddCommMonoid α] : ∀ (x x_1 : Interval α), Option.map₂ (fun (x x_2 : NonemptyInterval α) => x + x_2) x x_1 = Option.map₂ (fun (x x_2 : NonemptyInterval α) => x + x_2) x_1 x

theorem Interval.addCommMonoid.proof_5 {α : Type u_1} [OrderedAddCommMonoid α] : ∀ (n : ℕ) (x : Interval α), nsmulRec (n + 1) x = nsmulRec (n + 1) x

instance Interval.addCommMonoid {α : Type u_2} [OrderedAddCommMonoid α] : AddCommMonoid (Interval α)

Equations

• Interval.addCommMonoid = let __src := Interval.addZeroClass; AddCommMonoid.mk ⋯

instance Interval.commMonoid {α : Type u_2} [OrderedCommMonoid α] : CommMonoid (Interval α)

Equations

• Interval.commMonoid = let __src := Interval.mulOneClass; CommMonoid.mk ⋯

theorem NonemptyInterval.coe_nsmul_interval {α : Type u_2} [OrderedAddCommMonoid α] (s : NonemptyInterval α) (n : ℕ) : ↑(n • s) = n • ↑s

@[simp]

theorem NonemptyInterval.coe_pow_interval {α : Type u_2} [OrderedCommMonoid α] (s : NonemptyInterval α) (n : ℕ) : ↑(s ^ n) = ↑s ^ n

theorem Interval.bot_nsmul {α : Type u_2} [OrderedAddCommMonoid α] {n : ℕ} : n ≠ 0 → n • ⊥ = ⊥

abbrev Interval.bot_nsmul.match_1 (motive : (x : ℕ) → x ≠ 0 → Prop) : ∀ (x : ℕ) (x_1 : x ≠ 0), (∀ (h : 0 ≠ 0), motive 0 h) → (∀ (n : ℕ) (x : Nat.succ n ≠ 0), motive (Nat.succ n) x) → motive x x_1

Equations

• ⋯ = ⋯

theorem Interval.bot_pow {α : Type u_2} [OrderedCommMonoid α] {n : ℕ} : n ≠ 0 → ⊥ ^ n = ⊥

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

instance instSubNonemptyIntervalToLE {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : Sub (NonemptyInterval α)

Equations

• instSubNonemptyIntervalToLE = { sub := fun (s t : NonemptyInterval α) => { toProd := (s.toProd.1 - t.toProd.2, s.toProd.2 - t.toProd.1), fst_le_snd := ⋯ } }

instance instSubIntervalToLE {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] : Sub (Interval α)

Equations

• instSubIntervalToLE = { sub := Option.map₂ Sub.sub }

@[simp]

theorem NonemptyInterval.fst_sub {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : (s - t).toProd.1 = s.toProd.1 - t.toProd.2

@[simp]

theorem NonemptyInterval.snd_sub {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (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 α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : ↑(s - t) = ↑s - ↑t

theorem NonemptyInterval.sub_mem_sub {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (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 α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : NonemptyInterval.pure a - NonemptyInterval.pure b = NonemptyInterval.pure (a - b)

@[simp]

theorem Interval.bot_sub {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (t : Interval α) : ⊥ - t = ⊥

@[simp]

theorem Interval.sub_bot {α : Type u_2} [Preorder α] [AddCommSemigroup α] [Sub α] [OrderedSub α] [CovariantClass α α (fun (x x_1 : α) => x + x_1) fun (x x_1 : α) => x ≤ x_1] (s : Interval α) : s - ⊥ = ⊥

Division in ordered groups

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

instance instDivNonemptyIntervalToLE {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : Div (NonemptyInterval α)

Equations

• instDivNonemptyIntervalToLE = { div := fun (s t : NonemptyInterval α) => { toProd := (s.toProd.1 / t.toProd.2, s.toProd.2 / t.toProd.1), fst_le_snd := ⋯ } }

instance instDivIntervalToLE {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] : Div (Interval α)

Equations

• instDivIntervalToLE = { div := Option.map₂ fun (x x_1 : NonemptyInterval α) => x / x_1 }

@[simp]

theorem NonemptyInterval.fst_div {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : (s / t).toProd.1 = s.toProd.1 / t.toProd.2

@[simp]

theorem NonemptyInterval.snd_div {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : (s / t).toProd.2 = s.toProd.2 / t.toProd.1

@[simp]

theorem NonemptyInterval.coe_div_interval {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (t : NonemptyInterval α) : ↑(s / t) = ↑s / ↑t

theorem NonemptyInterval.div_mem_div {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : NonemptyInterval α) (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 α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (a : α) (b : α) : NonemptyInterval.pure a / NonemptyInterval.pure b = NonemptyInterval.pure (a / b)

@[simp]

theorem Interval.bot_div {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (t : Interval α) : ⊥ / t = ⊥

@[simp]

theorem Interval.div_bot {α : Type u_2} [Preorder α] [CommGroup α] [CovariantClass α α (fun (x x_1 : α) => x * x_1) fun (x x_1 : α) => x ≤ x_1] (s : Interval α) : s / ⊥ = ⊥

Negation/inversion

instance instNegNonemptyIntervalToLEToPreorderToPartialOrder {α : Type u_2} [OrderedAddCommGroup α] : Neg (NonemptyInterval α)

Equations

• instNegNonemptyIntervalToLEToPreorderToPartialOrder = { neg := fun (s : NonemptyInterval α) => { toProd := (-s.toProd.2, -s.toProd.1), fst_le_snd := ⋯ } }

theorem instNegNonemptyIntervalToLEToPreorderToPartialOrder.proof_1 {α : Type u_1} [OrderedAddCommGroup α] (s : NonemptyInterval α) : -s.toProd.2 ≤ -s.toProd.1

instance instInvNonemptyIntervalToLEToPreorderToPartialOrder {α : Type u_2} [OrderedCommGroup α] : Inv (NonemptyInterval α)

Equations

• instInvNonemptyIntervalToLEToPreorderToPartialOrder = { inv := fun (s : NonemptyInterval α) => { toProd := (s.toProd.2⁻¹, s.toProd.1⁻¹), fst_le_snd := ⋯ } }

instance instNegIntervalToLEToPreorderToPartialOrder {α : Type u_2} [OrderedAddCommGroup α] : Neg (Interval α)

Equations

• instNegIntervalToLEToPreorderToPartialOrder = { neg := Option.map Neg.neg }

instance instInvIntervalToLEToPreorderToPartialOrder {α : Type u_2} [OrderedCommGroup α] : Inv (Interval α)

Equations

• instInvIntervalToLEToPreorderToPartialOrder = { inv := Option.map Inv.inv }

@[simp]

theorem NonemptyInterval.fst_neg {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) : (-s).toProd.1 = -s.toProd.2

@[simp]

theorem NonemptyInterval.fst_inv {α : Type u_2} [OrderedCommGroup α] (s : NonemptyInterval α) : s⁻¹.toProd.1 = s.toProd.2⁻¹

@[simp]

theorem NonemptyInterval.snd_neg {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) : (-s).toProd.2 = -s.toProd.1

@[simp]

theorem NonemptyInterval.snd_inv {α : Type u_2} [OrderedCommGroup α] (s : NonemptyInterval α) : s⁻¹.toProd.2 = s.toProd.1⁻¹

@[simp]

theorem NonemptyInterval.coe_neg_interval {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) : ↑(-s) = -↑s

@[simp]

theorem NonemptyInterval.coe_inv_interval {α : Type u_2} [OrderedCommGroup α] (s : NonemptyInterval α) : ↑s⁻¹ = (↑s)⁻¹

theorem NonemptyInterval.neg_mem_neg {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) (a : α) (ha : a ∈ s) : -a ∈ -s

theorem NonemptyInterval.inv_mem_inv {α : Type u_2} [OrderedCommGroup α] (s : NonemptyInterval α) (a : α) (ha : a ∈ s) : a⁻¹ ∈ s⁻¹

@[simp]

theorem NonemptyInterval.neg_pure {α : Type u_2} [OrderedAddCommGroup α] (a : α) : -NonemptyInterval.pure a = NonemptyInterval.pure (-a)

@[simp]

theorem NonemptyInterval.inv_pure {α : Type u_2} [OrderedCommGroup α] (a : α) : (NonemptyInterval.pure a)⁻¹ = NonemptyInterval.pure a⁻¹

@[simp]

theorem Interval.neg_bot {α : Type u_2} [OrderedAddCommGroup α] : -⊥ = ⊥

@[simp]

theorem Interval.inv_bot {α : Type u_2} [OrderedCommGroup α] : ⊥⁻¹ = ⊥

theorem NonemptyInterval.add_eq_zero_iff {α : Type u_2} [OrderedAddCommGroup α] {s : NonemptyInterval α} {t : NonemptyInterval α} : s + t = 0 ↔ ∃ (a : α) (b : α), s = NonemptyInterval.pure a ∧ t = NonemptyInterval.pure b ∧ a + b = 0

theorem NonemptyInterval.mul_eq_one_iff {α : Type u_2} [OrderedCommGroup α] {s : NonemptyInterval α} {t : NonemptyInterval α} : s * t = 1 ↔ ∃ (a : α) (b : α), s = NonemptyInterval.pure a ∧ t = NonemptyInterval.pure b ∧ a * b = 1

instance NonemptyInterval.subtractionCommMonoid {α : Type u} [OrderedAddCommGroup α] : SubtractionCommMonoid (NonemptyInterval α)

Equations

• NonemptyInterval.subtractionCommMonoid = let __src := NonemptyInterval.addCommMonoid; SubtractionCommMonoid.mk ⋯

instance NonemptyInterval.divisionCommMonoid {α : Type u_2} [OrderedCommGroup α] : DivisionCommMonoid (NonemptyInterval α)

Equations

• NonemptyInterval.divisionCommMonoid = let __src := NonemptyInterval.commMonoid; DivisionCommMonoid.mk ⋯

theorem Interval.add_eq_zero_iff {α : Type u_2} [OrderedAddCommGroup α] {s : Interval α} {t : Interval α} : s + t = 0 ↔ ∃ (a : α) (b : α), s = Interval.pure a ∧ t = Interval.pure b ∧ a + b = 0

theorem Interval.mul_eq_one_iff {α : Type u_2} [OrderedCommGroup α] {s : Interval α} {t : Interval α} : s * t = 1 ↔ ∃ (a : α) (b : α), s = Interval.pure a ∧ t = Interval.pure b ∧ a * b = 1

instance Interval.subtractionCommMonoid {α : Type u} [OrderedAddCommGroup α] : SubtractionCommMonoid (Interval α)

Equations

• Interval.subtractionCommMonoid = let __src := Interval.addCommMonoid; SubtractionCommMonoid.mk ⋯

instance Interval.divisionCommMonoid {α : Type u_2} [OrderedCommGroup α] : DivisionCommMonoid (Interval α)

Equations

• Interval.divisionCommMonoid = let __src := Interval.commMonoid; DivisionCommMonoid.mk ⋯

def NonemptyInterval.length {α : Type u_2} [OrderedAddCommGroup α] (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.

Equations

• NonemptyInterval.length s = s.toProd.2 - s.toProd.1

@[simp]

theorem NonemptyInterval.length_nonneg {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) : 0 ≤ NonemptyInterval.length s

@[simp]

theorem NonemptyInterval.length_pure {α : Type u_2} [OrderedAddCommGroup α] (a : α) : NonemptyInterval.length (NonemptyInterval.pure a) = 0

@[simp]

theorem NonemptyInterval.length_zero {α : Type u_2} [OrderedAddCommGroup α] : NonemptyInterval.length 0 = 0

@[simp]

theorem NonemptyInterval.length_neg {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) : NonemptyInterval.length (-s) = NonemptyInterval.length s

@[simp]

theorem NonemptyInterval.length_add {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) (t : NonemptyInterval α) : NonemptyInterval.length (s + t) = NonemptyInterval.length s + NonemptyInterval.length t

@[simp]

theorem NonemptyInterval.length_sub {α : Type u_2} [OrderedAddCommGroup α] (s : NonemptyInterval α) (t : NonemptyInterval α) : NonemptyInterval.length (s - t) = NonemptyInterval.length s + NonemptyInterval.length t

@[simp]

theorem NonemptyInterval.length_sum {ι : Type u_1} {α : Type u_2} [OrderedAddCommGroup α] (f : ι → NonemptyInterval α) (s : Finset ι) : NonemptyInterval.length (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => NonemptyInterval.length (f i)

def Interval.length {α : Type u_2} [OrderedAddCommGroup α] : Interval α → α

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

Equations

• Interval.length x = match x with | none => 0 | some s => NonemptyInterval.length s

@[simp]

theorem Interval.length_nonneg {α : Type u_2} [OrderedAddCommGroup α] (s : Interval α) : 0 ≤ Interval.length s

@[simp]

theorem Interval.length_pure {α : Type u_2} [OrderedAddCommGroup α] (a : α) : Interval.length (Interval.pure a) = 0

@[simp]

theorem Interval.length_zero {α : Type u_2} [OrderedAddCommGroup α] : Interval.length 0 = 0

@[simp]

theorem Interval.length_neg {α : Type u_2} [OrderedAddCommGroup α] (s : Interval α) : Interval.length (-s) = Interval.length s

theorem Interval.length_add_le {α : Type u_2} [OrderedAddCommGroup α] (s : Interval α) (t : Interval α) : Interval.length (s + t) ≤ Interval.length s + Interval.length t

theorem Interval.length_sub_le {α : Type u_2} [OrderedAddCommGroup α] (s : Interval α) (t : Interval α) : Interval.length (s - t) ≤ Interval.length s + Interval.length t

theorem Interval.length_sum_le {ι : Type u_1} {α : Type u_2} [OrderedAddCommGroup α] (f : ι → Interval α) (s : Finset ι) : Interval.length (Finset.sum s fun (i : ι) => f i) ≤ Finset.sum s fun (i : ι) => Interval.length (f i)

def Mathlib.Meta.Positivity.evalNonemptyIntervalLength : Mathlib.Meta.Positivity.PositivityExt

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

def Mathlib.Meta.Positivity.evalIntervalLength : Mathlib.Meta.Positivity.PositivityExt

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