Theory Descartes_Roots_Test
section ‹Descartes Roots Test›
theory Descartes_Roots_Test imports Budan_Fourier
begin
text ‹The Descartes roots test is a consequence of Descartes' rule of signs:
through counting sign variations on coefficients of a base-transformed (i.e. Taylor shifted)
polynomial, it can over-approximate the number of real roots (counting multiplicity)
within an interval. Its ability is similar to the Budan--Fourier theorem, but is far more
efficient in practice. Therefore, this test is widely used in modern root isolation procedures.
More information can be found in the wiki page about Vincent's theorem:
@{url "https://en.wikipedia.org/wiki/Vincent%27s_theorem"}
and Collins and Akritas's classic paper of root isolation:
Collins, G.E., Akritas, A.G.: Polynomial real root isolation using Descarte's rule of signs. SYMSACC. 272--275 (1976).
A more modern treatment is available from a recent implementation of isolating real roots:
Kobel, A., Rouillier, F., Sagraloff, M.: Computing Real Roots of Real Polynomials ... and now For Real!
Proceedings of ISSAC '16, New York, New York, USA (2016).
›
lemma bij_betw_pos_interval:
fixes a b::real
assumes "a<b"
shows "bij_betw (λx. (a+b * x) / (1+x)) {x. x>0} {x. a<x ∧ x<b}"
proof (rule bij_betw_imageI)
show "inj_on (λx. (a + b * x) / (1 + x)) {x. 0 < x}"
unfolding inj_on_def
apply (auto simp add:field_simps)
using assms crossproduct_noteq by fastforce
have "x ∈ (λx. (a + b * x) / (1 + x)) ` {x. 0 < x}" when "a < x" "x < b" for x
proof (rule rev_image_eqI[of "(x-a)/(b-x)"])
define bx where "bx=b-x"
have x:"x=b-bx" unfolding bx_def by auto
have "bx≠0" "b>a" unfolding bx_def using that by auto
then show " x = (a + b * ((x - a) / (b - x))) / (1 + (x - a) / (b - x))"
apply (fold bx_def,unfold x)
by (auto simp add:field_simps)
show "(x - a) / (b - x) ∈ {x. 0 < x}" using that by auto
qed
then show "(λx. (a + b * x) / (1 + x)) ` {x. 0 < x} = {x. a < x ∧ x < b}"
using assms by (auto simp add:divide_simps algebra_simps)
qed
lemma proots_sphere_pos_interval:
fixes a b::real
defines "q1≡[:a,b:]" and "q2≡[:1,1:]"
assumes "p≠0" "a<b"
shows "proots_count p {x. a < x ∧ x < b} = proots_count (fcompose p q1 q2) {x. 0 < x}"
apply (rule proots_fcompose_bij_eq[OF _ ‹p≠0›])
unfolding q1_def q2_def using bij_betw_pos_interval[OF ‹a<b›] ‹a<b›
by (auto simp add:algebra_simps infinite_UNIV_char_0)
definition descartes_roots_test::"real ⇒ real ⇒ real poly ⇒ nat" where
"descartes_roots_test a b p = nat (changes (coeffs (fcompose p [:a,b:] [:1,1:])))"
theorem descartes_roots_test:
fixes p::"real poly"
assumes "p≠0" "a<b"
shows "proots_count p {x. a < x ∧ x <b} ≤ descartes_roots_test a b p ∧
even (descartes_roots_test a b p - proots_count p {x. a < x ∧ x < b})"
proof -
define q where "q=fcompose p [:a,b:] [:1,1:]"
have "q≠0"
unfolding q_def
apply (rule fcompose_nzero[OF ‹p≠0›])
using ‹a<b› infinite_UNIV_char_0 by auto
have "proots_count p {x. a < x ∧ x <b} = proots_count q {x. 0 < x}"
using proots_sphere_pos_interval[OF ‹p≠0› ‹a<b›,folded q_def] .
moreover have "int (proots_count q {x. 0 < x}) ≤ changes (coeffs q) ∧
even (changes (coeffs q) - int (proots_count q {x. 0 < x}))"
by (rule descartes_sign[OF ‹q≠0›])
then have "proots_count q {x. 0 < x} ≤ nat (changes (coeffs q)) ∧
even (nat (changes (coeffs q)) - proots_count q {x. 0 < x})"
using even_nat_iff by auto
ultimately show ?thesis
unfolding descartes_roots_test_def
apply (fold q_def)
by auto
qed
text ‹The roots test @{term descartes_roots_test} is exact if its result is 0 or 1.›
corollary descartes_roots_test_zero:
fixes p::"real poly"
assumes "p≠0" "a<b" "descartes_roots_test a b p = 0"
shows "∀x. a<x ∧ x<b ⟶ poly p x≠0"
proof -
have "proots_count p {x. a < x ∧ x <b} = 0"
using descartes_roots_test[OF assms(1,2)] assms(3) by auto
from proots_count_0_imp_empty[OF this ‹p≠0›]
show ?thesis by auto
qed
corollary descartes_roots_test_one:
fixes p::"real poly"
assumes "p≠0" "a<b" "descartes_roots_test a b p = 1"
shows "proots_count p {x. a < x ∧ x <b} = 1"
using descartes_roots_test[OF ‹p≠0› ‹a<b›] ‹descartes_roots_test a b p = 1›
by (metis dvd_diffD even_zero le_neq_implies_less less_one odd_one)
text ‹Similar to the Budan--Fourier theorem, the Descartes roots test result is exact when all roots
are real.›
corollary descartes_roots_test_real:
fixes p::"real poly"
assumes "p≠0" "a<b"
assumes "all_roots_real p"
shows "proots_count p {x. a < x ∧ x <b} = descartes_roots_test a b p"
proof -
define q where "q=fcompose p [:a,b:] [:1,1:]"
have "q≠0"
unfolding q_def
apply (rule fcompose_nzero[OF ‹p≠0›])
using ‹a<b› infinite_UNIV_char_0 by auto
have "proots_count p {x. a < x ∧ x <b} = proots_count q {x. 0 < x}"
using proots_sphere_pos_interval[OF ‹p≠0› ‹a<b›,folded q_def] .
moreover have "int (proots_count q {x. 0 < x}) = changes (coeffs q)"
apply (rule descartes_sign_real[OF ‹q≠0›])
unfolding q_def by (rule all_real_roots_mobius[OF ‹all_roots_real p› ‹a<b›])
then have "proots_count q {x. 0 < x} = nat (changes (coeffs q))"
by simp
ultimately show ?thesis unfolding descartes_roots_test_def
apply (fold q_def)
by auto
qed
end