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 #
Equations
- instZeroNonemptyInterval = { zero := NonemptyInterval.pure 0 }
Equations
- instOneNonemptyInterval = { one := NonemptyInterval.pure 1 }
Addition/multiplication #
Note that this multiplication does not apply to ℚ
or ℝ
.
Equations
- instAddNonemptyInterval = { add := fun (s t : NonemptyInterval α) => { toProd := s.toProd + t.toProd, fst_le_snd := ⋯ } }
Equations
- instMulNonemptyInterval = { mul := fun (s t : NonemptyInterval α) => { toProd := s.toProd * t.toProd, fst_le_snd := ⋯ } }
Equations
- instAddInterval = { add := Option.map₂ fun (x1 x2 : NonemptyInterval α) => x1 + x2 }
Equations
- instMulInterval = { mul := Option.map₂ fun (x1 x2 : NonemptyInterval α) => x1 * x2 }
Powers #
Equations
- NonemptyInterval.hasNSMul = { smul := fun (n : ℕ) (s : NonemptyInterval α) => { toProd := (n • s.toProd.1, n • s.toProd.2), fst_le_snd := ⋯ } }
Equations
- NonemptyInterval.hasPow = { pow := fun (s : NonemptyInterval α) (n : ℕ) => { toProd := s.toProd ^ n, fst_le_snd := ⋯ } }
Equations
- NonemptyInterval.addCommMonoid = Function.Injective.addCommMonoid NonemptyInterval.toProd ⋯ ⋯ ⋯ ⋯
Equations
- NonemptyInterval.commMonoid = Function.Injective.commMonoid NonemptyInterval.toProd ⋯ ⋯ ⋯ ⋯
Equations
- Interval.addZeroClass = AddZeroClass.mk ⋯ ⋯
Equations
- Interval.mulOneClass = MulOneClass.mk ⋯ ⋯
Equations
- Interval.addCommMonoid = AddCommMonoid.mk ⋯
Equations
- Interval.commMonoid = CommMonoid.mk ⋯
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).
Equations
- instSubNonemptyInterval = { sub := fun (s t : NonemptyInterval α) => { toProd := (s.toProd.1 - t.toProd.2, s.toProd.2 - t.toProd.1), fst_le_snd := ⋯ } }
Equations
- instSubInterval = { sub := Option.map₂ Sub.sub }
Division in ordered groups #
Note that this division does not apply to ℚ
or ℝ
.
Equations
- instDivNonemptyInterval = { div := fun (s t : NonemptyInterval α) => { toProd := (s.toProd.1 / t.toProd.2, s.toProd.2 / t.toProd.1), fst_le_snd := ⋯ } }
Equations
- instDivInterval = { div := Option.map₂ fun (x1 x2 : NonemptyInterval α) => x1 / x2 }
Negation/inversion #
Equations
- instNegNonemptyInterval = { neg := fun (s : NonemptyInterval α) => { toProd := (-s.toProd.2, -s.toProd.1), fst_le_snd := ⋯ } }
Equations
- instInvNonemptyInterval = { inv := fun (s : NonemptyInterval α) => { toProd := (s.toProd.2⁻¹, s.toProd.1⁻¹), fst_le_snd := ⋯ } }
Equations
- instNegInterval = { neg := Option.map Neg.neg }
Equations
- instInvInterval = { inv := Option.map Inv.inv }
Equations
- NonemptyInterval.subtractionCommMonoid = SubtractionCommMonoid.mk ⋯
Equations
- NonemptyInterval.divisionCommMonoid = DivisionCommMonoid.mk ⋯
Equations
- Interval.subtractionCommMonoid = SubtractionCommMonoid.mk ⋯
Equations
- Interval.divisionCommMonoid = DivisionCommMonoid.mk ⋯
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
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 none = 0
- Interval.length (some s) = s.length
Instances For
Extension for the positivity
tactic: The length of an interval is always nonnegative.
Instances For
Extension for the positivity
tactic: The length of an interval is always nonnegative.