The intervals of the Sturm step #
The structure of the intervals that the Sturm step (Ratpoints.Sturm.computeSturm) leaves, over the
values of the ends of their doubles: the bisection (Ratpoints.Sturm.iterate) at a depth of at most
55, where the search clamps it, meets only intervals of four shapes (Ratpoints.Sturm.EndsWF):
the ends at infinity ∓LONG_MAX with the exponent 0, finite ends n / 2 ^ e with |n| ≤ 2 ^ 53
and 0 ≤ e ≤ 55, increasing, whose midpoints (Ratpoints.Sturm.midpoint) the longs compute
without overflow strictly between the ends (Ratpoints.Sturm.EndsWF.halves); the doubles
ldexp((double)n, -e) of the ends are exact, ±2 ^ 63 at infinity
(Ratpoints.Sturm.EndsWF.hasValue_left), so that the intervals it keeps, joined where one ends at
the beginning of the next (Ratpoints.Sturm.AreIntervals.addInterval), are closed, increasing and
strictly apart (Ratpoints.Sturm.AreIntervals, Ratpoints.Sturm.iterate_wf). Their intersection
with well-formed intervals of the caller (Ratpoints.Sturm.intersectList, the loop of
Ratpoints.Sturm.intersect) is well formed, inside both, and holds every value that lies in both
(Ratpoints.Sturm.intervalsWF_intersectList,
Ratpoints.Sturm.inIntervals_of_inIntervals_intersectList,
Ratpoints.Sturm.inIntervals_intersectList); hence the Sturm step leaves well-formed intervals
inside the caller's (Ratpoints.Sturm.computeSturm_wf).
Main definitions #
Ratpoints.Sturm.HasValue: a double that is not a NaN, with its value.Ratpoints.Sturm.endValue: the value of the double of an end of the bisection.Ratpoints.Sturm.EndsWF: the intervals that the bisection meets at a depth.Ratpoints.Sturm.IsInterval,Ratpoints.Sturm.EndsBefore: an interval of doubles without a NaN whose ends are in order, and one interval ending strictly before another begins.Ratpoints.Sturm.AreIntervals: intervals of doubles without a NaN, increasing and strictly apart, equivalently well formed (Ratpoints.Sturm.intervalsWF_domainBits_iff).
Main statements #
Ratpoints.Sturm.EndsWF.halves: the halves of an interval of the bisection at its midpoint are intervals of the bisection at the next depth.Ratpoints.Sturm.EndsWF.hasValue_left,Ratpoints.Sturm.EndsWF.hasValue_right: the doubles of the ends are exact.Ratpoints.Sturm.iterate_wf: the intervals that the bisection keeps are well formed.Ratpoints.Sturm.intervalsWF_intersectList,Ratpoints.Sturm.inIntervals_of_inIntervals_intersectList,Ratpoints.Sturm.inIntervals_intersectList,Ratpoints.Sturm.length_intersectList_le: the intersection is well formed, inside both lists, holds what lies in both, and has fewer intervals than the two lists together.Ratpoints.Sturm.computeSturm_wf: the Sturm step leaves well-formed intervals inside the caller's.
The value of an end n / 2 ^ e of the bisection, ±2 ^ 63 for the ends ±LONG_MAX at
infinity, as their doubles have it.
Equations
Instances For
The double x is not a NaN and has the value q.
Equations
- Ratpoints.Sturm.HasValue x q = (x.isNaN = false ∧ Ratpoints.doubleValue x.bits = WithBotTop.coe q)
Instances For
The end LONG_MAX at +∞ of the bisection has the double 2 ^ 63.
The end -LONG_MAX at -∞ of the bisection has the double -2 ^ 63.
The interval from nl / 2 ^ del to nr / 2 ^ der of the bisection at the depth depth, as
Ratpoints.Sturm.iterate meets it when the depth is at most 55: one of the four shapes of the
intervals of the bisection (the whole line, the ends at infinity ∓LONG_MAX with the exponent 0,
an infinite interval with the finite end 0 or on its side of 0, two finite ends with the
exponent 0 when they have the same exponent), the exponents from 0 to the depth, the finite
ends, scaled to the larger exponent, at most 2 ^ depth / 4 in absolute value (from the depth 1
on), and the ends increasing.
- shape : nl = -longMax ∧ nr = longMax ∧ del = 0 ∧ der = 0 ∨ nl = -longMax ∧ nr ≠ longMax ∧ del = 0 ∧ der = 0 ∧ nr.toInt ≤ 0 ∨ nl ≠ -longMax ∧ nr = longMax ∧ del = 0 ∧ der = 0 ∧ 0 ≤ nl.toInt ∨ nl ≠ -longMax ∧ nr ≠ longMax ∧ (del = der → del = 0)
The four shapes: the whole line; the end at
-∞with a finite upper end≤ 0; a finite lower end≥ 0with the end at+∞, the exponents0in these three; two finite ends, with the exponent0when they have the same exponent. The lower end is not at
+∞.The upper end is not at
-∞.The exponent of the lower end is not negative.
The exponent of the upper end is not negative.
The exponent of the lower end is at most the depth.
The exponent of the upper end is at most the depth.
- bound_left : nl ≠ -longMax → 1 ≤ depth ∧ 4 * |nl.toInt| * 2 ^ (der.toInt - del.toInt).toNat ≤ 2 ^ depth
A finite lower end, scaled to the larger exponent, is at most
2 ^ depth / 4in absolute value, from the depth1on. - bound_right : nr ≠ longMax → 1 ≤ depth ∧ 4 * |nr.toInt| * 2 ^ (del.toInt - der.toInt).toNat ≤ 2 ^ depth
A finite upper end, scaled to the larger exponent, is at most
2 ^ depth / 4in absolute value, from the depth1on. The ends increase.
Instances For
The midpoint #
The halves of a finite interval [a, b] with the exponents 0 at its midpoint m,
2 m = a + b, when a + b is even.
The halves of a finite interval [a, b] with the exponents 0 at its midpoint (a + b) / 2
with the exponent 1, when a + b is odd.
The halves of a finite interval [a / 2 ^ p, b / 2 ^ q] with q < p at its midpoint
m / 2 ^ (p + 1), m = a + b 2 ^ (p - q).
The midpoint a + b 2 ^ (p - q) of the interval from a / 2 ^ p to b / 2 ^ q, q < p,
computed in longs, without overflow for |a| and |b| 2 ^ (p - q) at most 2 ^ 52.
The halves of a finite interval [a / 2 ^ p, b / 2 ^ q] with p < q at its midpoint
m / 2 ^ (q + 1), m = a 2 ^ (q - p) + b.
The midpoint a 2 ^ (q - p) + b of the interval from a / 2 ^ p to b / 2 ^ q, p < q,
computed in longs, without overflow for |a| 2 ^ (q - p) and |b| at most 2 ^ 52.
An interval of doubles whose ends are not NaNs and whose lower end is at most its upper end, by their values.
Equations
- Ratpoints.Sturm.IsInterval i = (i.1.isNaN = false ∧ i.2.isNaN = false ∧ Ratpoints.doubleValue i.1.bits ≤ Ratpoints.doubleValue i.2.bits)
Instances For
The relation of two intervals of doubles of which the first ends strictly before the second begins, by the values of their ends.
Equations
- Ratpoints.Sturm.EndsBefore i j = (Ratpoints.doubleValue i.2.bits < Ratpoints.doubleValue j.1.bits)
Instances For
Intervals of doubles without a NaN, each with its ends in order, increasing and strictly apart, by the values of their ends.
Equations
- Ratpoints.Sturm.AreIntervals l = ((∀ i ∈ l, Ratpoints.Sturm.IsInterval i) ∧ List.Pairwise Ratpoints.Sturm.EndsBefore l)
Instances For
Every interval of increasing intervals strictly apart ends at the end of the last at the latest.
The join of the interval up to u to the last interval kept, from lo to up, keeps the
intervals increasing and strictly apart when u lies above up.
A new last interval x after increasing intervals strictly apart that end before x begins
keeps them so.
The last interval kept after the bisection adds the interval up to u ends at u, whether
it is the new interval or the join of it to the last interval before.
The intervals kept stay increasing and strictly apart when the bisection adds the interval from
l to u (their values L < U) after kept intervals that end at L at the latest, joining it
to the last of them when that ends at L.
What the intervals kept hold stays held when the bisection adds an interval up to u after
them, with the value U above L, the last of them ending at L at the latest: the join extends
the last interval.
The intervals kept hold every value from L to U after the bisection adds the interval from
l to u with these values.
The intervals that the bisection keeps from the interval from nl / 2 ^ del to nr / 2 ^ der
at the depth depth ≤ iter ≤ 55, after kept intervals that end at its lower end at the latest, are
increasing and strictly apart and end at its upper end at the latest.
An interval of the intersection is that of an interval of each list, which it meets.
An interval of the intersection begins at the beginning of an interval of each list at the earliest.
A value in two intervals lies in the interval that Ratpoints.Sturm.meet notes for them.
A value in an interval a and an interval of b :: bs lies in the interval that
Ratpoints.Sturm.meet notes for a and b when the step goes on with the next interval after a:
an interval after b begins after the end of a.
A value in an interval of a :: as and an interval b lies in the interval that
Ratpoints.Sturm.meet notes for a and b when the step goes on with the next interval after b:
an interval after a begins after the end of b.
A value in an interval of each list lies in an interval of their intersection: the step at the two intervals notes their intersection, and every other step moves past an interval that ends before one of them begins.
The Sturm step after a successful chain: no interval at the exit when f has no real root and
f(0) < 0, and otherwise the intersection of the intervals that the bisection keeps from
[-∞, +∞] with the caller's.
The intervals of the Sturm step at a depth of at most 55 for well-formed intervals of the
caller are well formed and inside the caller's intervals.