The Sturm step keeps every point #
Assuming Sturm's theorem (Ratpoints.SturmTheorem), the intervals that the Sturm step
(Ratpoints.Sturm.computeSturm) leaves hold every value x with |x| ≤ 2 ^ 63 and f(x) ≥ 0
of the caller's intervals (Ratpoints.Sturm.covers_computeSturm); the bisection keeps at most
1 + ⌊d / 2⌋ intervals, the room of the array ivlocal of the C code
(Ratpoints.Sturm.size_run_iterate_le_of_chain_eq_some), and the intersection with the caller's
intervals has at most ⌊d / 2⌋ intervals more than they, within the room that the caller's array
must have (Ratpoints.Sturm.size_run_computeSturm_le).
The bisection (Ratpoints.Sturm.iterate) keeps the invariant Ratpoints.Sturm.IterateInvariant:
its intervals are intervals of the bisection (Ratpoints.Sturm.EndsWF), and the counts and signs it
hands on are those of the real polynomial f at their ends, since the rows of the chain are, over
ℝ, positive multiples of the entries of the Sturm sequence of f and f'
(Ratpoints.Sturm.IsChain.signsOf, Ratpoints.Sturm.IsChain.run_countsAtInfinity_eq). An interval
that it drops holds no x with f(x) ≥ 0 (Ratpoints.Sturm.IterateInvariant.not_kept, from
Ratpoints.eval_neg_of_vLeft_eq_vRight); one that it keeps holds every value between the doubles of
its ends (Ratpoints.Sturm.covers_addInterval) and a point where f is positive
(Ratpoints.Sturm.IterateInvariant.exists_pos, from Ratpoints.exists_inside_eval_pos); and a
value x with f(x) ≥ 0 that an interval it splits would keep is kept by one of its halves
(Ratpoints.Sturm.kept_halves), where at a simple root m the signs of f'(m) that the halves get
decide which. Between two intervals it keeps, f is negative, so that their positive points and the
negative points between them alternate in sign, and a polynomial of degree d changes its sign at
most d times (Ratpoints.Sturm.length_le_of_witnessed).
Main definitions #
Ratpoints.Sturm.lowerEnd,Ratpoints.Sturm.upperEnd: the real ends of an interval of the bisection, none at infinity.Ratpoints.Sturm.IterateInvariant: the invariant of the bisection for a real polynomial.Ratpoints.Sturm.Kept: the values that the bisection of an interval keeps.Ratpoints.Sturm.SignsOf: the signs and counts thatRatpoints.Sturm.signsAtcomputes are those of a real polynomial.Ratpoints.Sturm.Witnessed: an interval kept with a point where the polynomial is positive.
Main statements #
Ratpoints.Sturm.covers_iterate: the bisection keeps every value withf ≥ 0that it should keep.Ratpoints.Sturm.covers_computeSturm: the Sturm step keeps every value withf ≥ 0of the caller's intervals.Ratpoints.Sturm.size_run_iterate_le_of_chain_eq_some,Ratpoints.Sturm.size_run_computeSturm_le: the bisection keeps at most1 + ⌊d / 2⌋intervals, and the intersection adds at most⌊d / 2⌋to the intervals of the caller.
The lower end nl / 2 ^ del of an interval of the bisection over ℝ, none for the end
-LONG_MAX at -∞.
Equations
- Ratpoints.Sturm.lowerEnd nl del = if nl = -Ratpoints.Sturm.longMax then none else some ↑(Ratpoints.Sturm.endValue nl del)
Instances For
The upper end nr / 2 ^ der of an interval of the bisection over ℝ, none for the end
LONG_MAX at +∞.
Equations
- Ratpoints.Sturm.upperEnd nr der = if nr = Ratpoints.Sturm.longMax then none else some ↑(Ratpoints.Sturm.endValue nr der)
Instances For
The invariant of the bisection Ratpoints.Sturm.iterate on the interval from nl / 2 ^ del
to nr / 2 ^ der at the depth depth, for the real polynomial F whose chain it evaluates: an
interval of the bisection (Ratpoints.Sturm.EndsWF) whose counts cl, cr and signs sl, sr
are those of F at its ends (Ratpoints.vLeft, Ratpoints.vRight, Ratpoints.sgnLeftEnd,
Ratpoints.sgnRightEnd).
- ends : EndsWF depth nl nr del der
An interval of the bisection at the depth.
The count at the lower end.
The count at the upper end.
The sign just inside the lower end.
The sign just inside the upper end.
Instances For
The values x that the bisection of an interval keeps: between the values of the doubles of
its ends, at a finite end only when F is positive just inside it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A value that the bisection of an interval keeps lies between its real ends, or at a finite
end where F is positive just inside.
By Sturm's theorem, an interval that the bisection drops, with equal counts at its ends and F
negative just inside its lower end, holds no value x with F(x) ≥ 0 that it would keep.
The halves at the midpoint m = nm / 2 ^ dem of an interval of the bisection keep the
invariant with the counts and signs that Ratpoints.Sturm.iterate hands them, when s0, s1 and
cmid are the signs of F(m) and F'(m) and the count V(m).
A value x with F(x) ≥ 0 that the bisection of an interval keeps is kept by one of its
halves at the midpoint m, with the signs that Ratpoints.Sturm.iterate hands them: at m itself
by the left half when F(m) > 0 or F'(m) < 0, and by the right half when F'(m) > 0.
The intervals kept hold what they held, and every value between the ends of an interval of the bisection, after the bisection keeps that interval.
The signs and the count that Ratpoints.Sturm.signsAt computes for the chain rows at the
finite points nm / 2 ^ dem with 0 ≤ dem ≤ 55 are those of the real polynomial F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The signs and the count at the midpoint of an interval of the bisection, below the depth
55.
By Sturm's theorem, the bisection Ratpoints.Sturm.iterate of an interval with the invariant
Ratpoints.Sturm.IterateInvariant of a squarefree F, up to the depth iter ≤ 55, keeps what the
intervals kept so far hold, and every value with F ≥ 0 that it keeps
(Ratpoints.Sturm.Kept).
The real polynomial of the chain of c and d is squarefree when the chain succeeds: over ℚ
by Ratpoints.Sturm.run_chain_eq_none_iff, and a separable polynomial stays separable over
ℝ.
The invariant of the bisection on the whole line, with the counts and signs of F at ∓∞.
For a chain whose last row is constant, of a polynomial of degree d < 2 ^ 57 that is
squarefree over ℝ, Ratpoints.Sturm.signsAt computes the signs and the count of the real
polynomial (Ratpoints.Sturm.IsChain.run_signsAt_eq).
By Sturm's theorem, the Sturm step at a depth of at most 55 on a polynomial of degree
1 ≤ d < 2 ^ 57 with c_d ≠ 0, for well-formed intervals of the caller, leaves intervals that hold
every value x with |x| ≤ 2 ^ 63 and f(x) ≥ 0 in the caller's intervals.
The size of the intervals kept #
The ends of an interval of the bisection up to the depth 55 have values in
[-2 ^ 63, 2 ^ 63].
The ends of an interval of doubles have rational values L and U in [-2 ^ 63, 2 ^ 63], and
the real polynomial F is positive at a point p above L and below U, where an end of the
value ∓2 ^ 63, the value of an end at infinity of the bisection, does not bound p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The interval from lo to u that joins the interval up to u with the value U to the last
interval (lo, up) kept, where up has the value L of the new lower end, is witnessed by the
witness of the new interval.
The intervals kept stay witnessed when the bisection adds one from l to u with a positive
point after them: a join extends the last interval with the witness of the new one.
By Sturm's theorem, an interval that the bisection keeps, without equal counts at its ends and
F negative just inside its lower end, holds a point where F is positive: next to a root
between its ends, or just inside its lower end.
By Sturm's theorem, the bisection of an interval with the invariant of a squarefree F, up to
the depth iter ≤ 55, after witnessed intervals, keeps witnessed intervals
(Ratpoints.Sturm.Witnessed).
Between two neighbouring intervals of intervals increasing and strictly apart that hold every
value x ≥ A up to 2 ^ 63 with F(x) ≥ 0, F is negative.
The values x ≥ L_j with F(x) ≥ 0 held by intervals i :: j :: l increasing and strictly
apart are held by j :: l, when the first interval begins at A ≤ x at the earliest.
The step of Ratpoints.Sturm.exists_isChain_of_witnessed: points of alternating signs for
j :: l, the first positive and above the lower end of j, are preceded by the positive point
of i and a negative point between i and j.
Witnessed intervals, increasing and strictly apart, that hold every value x ≥ A up to
2 ^ 63 with F(x) ≥ 0, the first beginning at A at the earliest, give increasing points at
which the signs of F alternate: a positive point in each interval, the first one above the lower
end of the first interval unless that is -2 ^ 63, and a negative point between each two.
Witnessed intervals, increasing and strictly apart, that hold every value in [-2 ^ 63, 2 ^ 63]
with F ≥ 0, are at most 1 + n / 2 for a nonzero F of degree n: their positive points and the
negative points between them are 2 m - 1 points of alternating signs
(Polynomial.length_le_natDegree_add_one_of_isChain).
By Sturm's theorem, the bisection of the Sturm step at a depth of at most 55, for a polynomial
of degree 1 ≤ d < 2 ^ 57 with c_d ≠ 0 whose chain succeeds, keeps at most 1 + ⌊d / 2⌋
intervals: each holds a point where f is positive, and f is negative between two of them.
By Sturm's theorem, the intersection of the intervals of the Sturm step at a depth of at most
55, for a polynomial of degree 1 ≤ d < 2 ^ 57 with c_d ≠ 0, with the intervals iv of the
caller has at most iv.size + ⌊d / 2⌋ intervals (from
Ratpoints.Sturm.size_run_iterate_le_of_chain_eq_some): within both the room num_inter + degree
that the manual asks of the caller's array and the room of 1 + ⌊degree / 2⌋ intervals more than
it holds that the C code relies on (sturm.c:52-53), the latter from the degree 3 on only by
the bound with ⌊d / 2⌋.
The value of the real polynomial of the chain of c and its degree at a rational point.
The real polynomial of the chain of c and its degree is not negative at a / b, b > 0,
when the binary form is not negative at (a, b).