Theory Misc_Polynomial
theory Misc_Polynomial
imports "HOL-Computational_Algebra.Polynomial" "HOL-Computational_Algebra.Polynomial_Factorial" "Pure-ex.Guess"
begin
subsection ‹Analysis›
lemma fun_eq_in_ivl:
assumes "a ≤ b" "∀x::real. a ≤ x ∧ x ≤ b ⟶ eventually (λξ. f ξ = f x) (at x)"
shows "f a = f b"
proof (rule connected_local_const)
show "connected {a..b}" "a ∈ {a..b}" "b ∈ {a..b}" using ‹a ≤ b› by (auto intro: connected_Icc)
show "∀aa∈{a..b}. eventually (λb. f aa = f b) (at aa within {a..b})"
proof
fix x assume "x ∈ {a..b}"
with assms(2)[rule_format, of x]
show "eventually (λb. f x = f b) (at x within {a..b})"
by (auto simp: eventually_at_filter elim: eventually_mono)
qed
qed
subsection ‹Polynomials›
subsubsection ‹General simplification lemmas›
lemma pderiv_div:
assumes [simp]: "q dvd p" "q ≠ 0"
shows "pderiv (p div q) = (q * pderiv p - p * pderiv q) div (q * q)"
"q*q dvd (q * pderiv p - p * pderiv q)"
proof-
from assms obtain r where "p = q * r" unfolding dvd_def by blast
hence "q * pderiv p - p * pderiv q = (q * q) * pderiv r"
by (simp add: algebra_simps pderiv_mult)
thus "q*q dvd (q * pderiv p - p * pderiv q)" by simp
note 0 = pderiv_mult[of q "p div q"]
have 1: "q * (p div q) = p"
by (metis assms(1) assms(2) dvd_def nonzero_mult_div_cancel_left)
have f1: "pderiv (p div q) * (q * q) div (q * q) = pderiv (p div q)"
by simp
have f2: "pderiv p = q * pderiv (p div q) + p div q * pderiv q"
by (metis 0 1)
have "p * pderiv q = pderiv q * (q * (p div q))"
by (metis 1 mult.commute)
then have "p * pderiv q = q * (p div q * pderiv q)"
by fastforce
then have "q * pderiv p - p * pderiv q = q * (q * pderiv (p div q))"
using f2 by (metis add_diff_cancel_right' distrib_left)
then show "pderiv (p div q) = (q * pderiv p - p * pderiv q) div (q * q)"
using f1 by (metis mult.commute mult.left_commute)
qed
subsubsection ‹Divisibility of polynomials›
text ‹
Two polynomials that are coprime have no common roots.
›
lemma coprime_imp_no_common_roots:
"¬ (poly p x = 0 ∧ poly q x = 0)" if "coprime p q"
for x :: "'a :: field"
proof clarify
assume "poly p x = 0" "poly q x = 0"
then have "[:-x, 1:] dvd p" "[:-x, 1:] dvd q"
by (simp_all add: poly_eq_0_iff_dvd)
with that have "is_unit [:-x, 1:]"
by (rule coprime_common_divisor)
then show False
by (auto simp add: is_unit_pCons_iff)
qed
lemma poly_div:
assumes "poly q x ≠ 0" and "(q::'a :: field poly) dvd p"
shows "poly (p div q) x = poly p x / poly q x"
proof-
from assms have [simp]: "q ≠ 0" by force
have "poly q x * poly (p div q) x = poly (q * (p div q)) x" by simp
also have "q * (p div q) = p"
using assms by (simp add: div_mult_swap)
finally show "poly (p div q) x = poly p x / poly q x"
using assms by (simp add: field_simps)
qed
lemma poly_div_gcd_squarefree_aux:
assumes "pderiv (p::('a::{field_char_0,field_gcd}) poly) ≠ 0"
defines "d ≡ gcd p (pderiv p)"
shows "coprime (p div d) (pderiv (p div d))" and
"⋀x. poly (p div d) x = 0 ⟷ poly p x = 0"
proof -
obtain r s where "bezout_coefficients p (pderiv p) = (r, s)"
by (auto simp add: prod_eq_iff)
then have "r * p + s * pderiv p = gcd p (pderiv p)"
by (rule bezout_coefficients)
then have rs: "d = r * p + s * pderiv p"
by (simp add: d_def)
define t where "t = p div d"
define p' where [simp]: "p' = pderiv p"
define d' where [simp]: "d' = pderiv d"
define u where "u = p' div d"
have A: "p = t * d" and B: "p' = u * d"
by (simp_all add: t_def u_def d_def algebra_simps)
from poly_squarefree_decomp[OF assms(1) A B[unfolded p'_def] rs]
show "⋀x. poly (p div d) x = 0 ⟷ poly p x = 0" by (auto simp: t_def)
from rs have C: "s*t*d' = d * (1 - r*t - s*pderiv t)"
by (simp add: A B algebra_simps pderiv_mult)
from assms have [simp]: "p ≠ 0" "d ≠ 0" "t ≠ 0"
by (force, force, subst (asm) A, force)
have "⋀x. ⟦x dvd t; x dvd (pderiv t)⟧ ⟹ x dvd 1"
proof -
fix x assume "x dvd t" "x dvd (pderiv t)"
then obtain v w where vw:
"t = x*v" "pderiv t = x*w" unfolding dvd_def by blast
define x' v' where [simp]: "x' = pderiv x" and [simp]: "v' = pderiv v"
from vw have "x*v' + v*x' = x*w" by (simp add: pderiv_mult)
hence "v*x' = x*(w - v')" by (simp add: algebra_simps)
hence "x dvd v*pderiv x" by simp
then obtain y where y: "v*x' = x*y" unfolding dvd_def by force
from ‹t ≠ 0› and vw have "x ≠ 0" by simp
have x_pow_n_dvd_d: "⋀n. x^n dvd d"
proof-
fix n show "x ^ n dvd d"
proof (induction n, simp, rename_tac n, case_tac n)
fix n assume "n = (0::nat)"
from vw and C have "d = x*(d*r*v + d*s*w + s*v*d')"
by (simp add: algebra_simps)
with ‹n = 0› show "x^Suc n dvd d" by (force intro: dvdI)
next
fix n n' assume IH: "x^n dvd d" and "n = Suc n'"
hence [simp]: "Suc n' = n" "x * x^n' = x^n" by simp_all
define c :: "'a poly" where "c = [:of_nat n:]"
from pderiv_power_Suc[of x n']
have [simp]: "pderiv (x^n) = c*x^n' * x'" unfolding c_def
by simp
from IH obtain z where d: "d = x^n * z" unfolding dvd_def by blast
define z' where [simp]: "z' = pderiv z"
from d ‹d ≠ 0› have "x^n ≠ 0" "z ≠ 0" by force+
from C d have "x^n*z = z*r*v*x^Suc n + z*s*c*x^n*(v*x') +
s*v*z'*x^Suc n + s*z*(v*x')*x^n + s*z*v'*x^Suc n"
by (simp add: algebra_simps vw pderiv_mult)
also have "... = x^n*x * (z*r*v + z*s*c*y + s*v*z' + s*z*y + s*z*v')"
by (simp only: y, simp add: algebra_simps)
finally have "z = x*(z*r*v+z*s*c*y+s*v*z'+s*z*y+s*z*v')"
using ‹x^n ≠ 0› by force
hence "x dvd z" by (metis dvd_triv_left)
with d show "x^Suc n dvd d" by simp
qed
qed
have "degree x = 0"
proof (cases "degree x", simp)
case (Suc n)
hence "x ≠ 0" by auto
with Suc have "degree (x ^ (Suc (degree d))) > degree d"
by (subst degree_power_eq, simp_all)
moreover from x_pow_n_dvd_d[of "Suc (degree d)"] and ‹d ≠ 0›
have "degree (x^Suc (degree d)) ≤ degree d"
by (simp add: dvd_imp_degree_le)
ultimately show ?thesis by simp
qed
then obtain c where [simp]: "x = [:c:]" by (cases x, simp split: if_split_asm)
moreover from ‹x ≠ 0› have "c ≠ 0" by simp
ultimately show "x dvd 1" using dvdI[of 1 x "[:inverse c:]"]
by simp
qed
then show "coprime t (pderiv t)"
by (rule coprimeI)
qed
lemma normalize_field:
"normalize (x :: 'a :: {field,normalization_semidom}) = (if x = 0 then 0 else 1)"
by (auto simp: is_unit_normalize dvd_field_iff)
lemma normalize_field_eq_1 [simp]:
"x ≠ 0 ⟹ normalize (x :: 'a :: {field,normalization_semidom}) = 1"
by (simp add: normalize_field)
lemma unit_factor_field [simp]:
"unit_factor (x :: 'a :: {field,normalization_semidom}) = x"
by (cases "x = 0") (auto simp: is_unit_unit_factor dvd_field_iff)
text ‹
Dividing a polynomial by its gcd with its derivative yields
a squarefree polynomial with the same roots.
›
lemma poly_div_gcd_squarefree:
assumes "(p :: ('a::{field_char_0,field_gcd}) poly) ≠ 0"
defines "d ≡ gcd p (pderiv p)"
shows "coprime (p div d) (pderiv (p div d))" (is ?A) and
"⋀x. poly (p div d) x = 0 ⟷ poly p x = 0" (is "⋀x. ?B x")
proof-
have "?A ∧ (∀x. ?B x)"
proof (cases "pderiv p = 0")
case False
from poly_div_gcd_squarefree_aux[OF this] show ?thesis
unfolding d_def by auto
next
case True
then obtain c where [simp]: "p = [:c:]" using pderiv_iszero by blast
from assms(1) have "c ≠ 0" by simp
from True have "d = smult (inverse c) p"
by (simp add: d_def normalize_poly_def map_poly_pCons field_simps)
with ‹p ≠ 0› ‹c ≠ 0› have "p div d = [:c:]"
by (simp add: pCons_one)
with ‹c ≠ 0› show ?thesis
by (simp add: normalize_const_poly is_unit_triv)
qed
thus ?A and "⋀x. ?B x" by simp_all
qed
subsubsection ‹Sign changes of a polynomial›
text ‹
If a polynomial has different signs at two points, it has a root inbetween.
›
lemma poly_different_sign_imp_root:
assumes "a < b" and "sgn (poly p a) ≠ sgn (poly p (b::real))"
shows "∃x. a ≤ x ∧ x ≤ b ∧ poly p x = 0"
proof (cases "poly p a = 0 ∨ poly p b = 0")
case True
thus ?thesis using assms(1)
by (elim disjE, rule_tac exI[of _ a], simp,
rule_tac exI[of _ b], simp)
next
case False
hence [simp]: "poly p a ≠ 0" "poly p b ≠ 0" by simp_all
show ?thesis
proof (cases "poly p a < 0")
case True
hence "sgn (poly p a) = -1" by simp
with assms True have "poly p b > 0"
by (auto simp: sgn_real_def split: if_split_asm)
from poly_IVT_pos[OF ‹a < b› True this] guess x ..
thus ?thesis by (intro exI[of _ x], simp)
next
case False
hence "poly p a > 0" by (simp add: not_less less_eq_real_def)
hence "sgn (poly p a) = 1" by simp
with assms False have "poly p b < 0"
by (auto simp: sgn_real_def not_less
less_eq_real_def split: if_split_asm)
from poly_IVT_neg[OF ‹a < b› ‹poly p a > 0› this] guess x ..
thus ?thesis by (intro exI[of _ x], simp)
qed
qed
lemma poly_different_sign_imp_root':
assumes "sgn (poly p a) ≠ sgn (poly p (b::real))"
shows "∃x. poly p x = 0"
using assms by (cases "a < b", auto dest!: poly_different_sign_imp_root
simp: less_eq_real_def not_less)
lemma no_roots_inbetween_imp_same_sign:
assumes "a < b" "∀x. a ≤ x ∧ x ≤ b ⟶ poly p x ≠ (0::real)"
shows "sgn (poly p a) = sgn (poly p b)"
using poly_different_sign_imp_root assms by auto
subsubsection ‹Limits of polynomials›
lemma poly_neighbourhood_without_roots:
assumes "(p :: real poly) ≠ 0"
shows "eventually (λx. poly p x ≠ 0) (at x⇩0)"
proof-
{
fix ε :: real assume "ε > 0"
have fin: "finite {x. ¦x-x⇩0¦ < ε ∧ x ≠ x⇩0 ∧ poly p x = 0}"
using poly_roots_finite[OF assms] by simp
with ‹ε > 0›have "∃δ>0. δ≤ε ∧ (∀x. ¦x-x⇩0¦ < δ ∧ x ≠ x⇩0 ⟶ poly p x ≠ 0)"
proof (induction "card {x. ¦x-x⇩0¦ < ε ∧ x ≠ x⇩0 ∧ poly p x = 0}"
arbitrary: ε rule: less_induct)
case (less ε)
let ?A = "{x. ¦x - x⇩0¦ < ε ∧ x ≠ x⇩0 ∧ poly p x = 0}"
show ?case
proof (cases "card ?A")
case 0
hence "?A = {}" using less by auto
thus ?thesis using less(2) by (rule_tac exI[of _ ε], auto)
next
case (Suc _)
with less(3) have "{x. ¦x - x⇩0¦ < ε ∧ x ≠ x⇩0 ∧ poly p x = 0} ≠ {}" by force
then obtain x where x_props: "¦x - x⇩0¦ < ε" "x ≠ x⇩0" "poly p x = 0" by blast
define ε' where "ε' = ¦x - x⇩0¦ / 2"
have "ε' > 0" "ε' < ε" unfolding ε'_def using x_props by simp_all
from x_props(1,2) and ‹ε > 0›
have "x ∉ {x'. ¦x' - x⇩0¦ < ε' ∧ x' ≠ x⇩0 ∧ poly p x' = 0}" (is "_ ∉ ?B")
by (auto simp: ε'_def)
moreover from x_props
have "x ∈ {x. ¦x - x⇩0¦ < ε ∧ x ≠ x⇩0 ∧ poly p x = 0}" by blast
ultimately have "?B ⊂ ?A" by auto
hence "card ?B < card ?A" "finite ?B"
by (rule psubset_card_mono[OF less(3)],
blast intro: finite_subset[OF _ less(3)])
from less(1)[OF this(1) ‹ε' > 0› this(2)]
show ?thesis using ‹ε' < ε› by force
qed
qed
}
from this[of "1"]
show ?thesis by (auto simp: eventually_at dist_real_def)
qed
lemma poly_neighbourhood_same_sign:
assumes "poly p (x⇩0 :: real) ≠ 0"
shows "eventually (λx. sgn (poly p x) = sgn (poly p x⇩0)) (at x⇩0)"
proof -
have cont: "isCont (λx. sgn (poly p x)) x⇩0"
by (rule isCont_sgn, rule poly_isCont, rule assms)
then have "eventually (λx. ¦sgn (poly p x) - sgn (poly p x⇩0)¦ < 1) (at x⇩0)"
by (auto simp: isCont_def tendsto_iff dist_real_def)
then show ?thesis
by (rule eventually_mono) (simp add: sgn_real_def split: if_split_asm)
qed
lemma poly_lhopital:
assumes "poly p (x::real) = 0" "poly q x = 0" "q ≠ 0"
assumes "(λx. poly (pderiv p) x / poly (pderiv q) x) ─x→ y"
shows "(λx. poly p x / poly q x) ─x→ y"
using assms
proof (rule_tac lhopital)
have "isCont (poly p) x" "isCont (poly q) x" by simp_all
with assms(1,2) show "poly p ─x→ 0" "poly q ─x→ 0"
by (simp_all add: isCont_def)
from ‹q ≠ 0› and ‹poly q x = 0› have "pderiv q ≠ 0"
by (auto dest: pderiv_iszero)
from poly_neighbourhood_without_roots[OF this]
show "eventually (λx. poly (pderiv q) x ≠ 0) (at x)" .
qed (auto intro: poly_DERIV poly_neighbourhood_without_roots)
lemma poly_roots_bounds:
assumes "p ≠ 0"
obtains l u
where "l ≤ (u :: real)"
and "poly p l ≠ 0"
and "poly p u ≠ 0"
and "{x. x > l ∧ x ≤ u ∧ poly p x = 0 } = {x. poly p x = 0}"
and "⋀x. x ≤ l ⟹ sgn (poly p x) = sgn (poly p l)"
and "⋀x. x ≥ u ⟹ sgn (poly p x) = sgn (poly p u)"
proof
from assms have "finite {x. poly p x = 0}" (is "finite ?roots")
using poly_roots_finite by fast
let ?roots' = "insert 0 ?roots"
define l where "l = Min ?roots' - 1"
define u where "u = Max ?roots' + 1"
from ‹finite ?roots› have A: "finite ?roots'" by auto
from Min_le[OF this, of 0] and Max_ge[OF this, of 0]
show "l ≤ u" by (simp add: l_def u_def)
from Min_le[OF A] have l_props: "⋀x. x≤l ⟹ poly p x ≠ 0"
by (fastforce simp: l_def)
from Max_ge[OF A] have u_props: "⋀x. x≥u ⟹ poly p x ≠ 0"
by (fastforce simp: u_def)
from l_props u_props show [simp]: "poly p l ≠ 0" "poly p u ≠ 0" by auto
from l_props have "⋀x. poly p x = 0 ⟹ x > l" by (metis not_le)
moreover from u_props have "⋀x. poly p x = 0 ⟹ x ≤ u" by (metis linear)
ultimately show "{x. x > l ∧ x ≤ u ∧ poly p x = 0} = ?roots" by auto
{
fix x assume A: "x < l" "sgn (poly p x) ≠ sgn (poly p l)"
with poly_IVT_pos[OF A(1), of p] poly_IVT_neg[OF A(1), of p] A(2)
have False by (auto split: if_split_asm
simp: sgn_real_def l_props not_less less_eq_real_def)
}
thus "⋀x. x ≤ l ⟹ sgn (poly p x) = sgn (poly p l)"
by (case_tac "x = l", auto simp: less_eq_real_def)
{
fix x assume A: "x > u" "sgn (poly p x) ≠ sgn (poly p u)"
with u_props poly_IVT_neg[OF A(1), of p] poly_IVT_pos[OF A(1), of p] A(2)
have False by (auto split: if_split_asm
simp: sgn_real_def l_props not_less less_eq_real_def)
}
thus "⋀x. x ≥ u ⟹ sgn (poly p x) = sgn (poly p u)"
by (case_tac "x = u", auto simp: less_eq_real_def)
qed
definition poly_inf :: "('a::real_normed_vector) poly ⇒ 'a" where
"poly_inf p ≡ sgn (coeff p (degree p))"
definition poly_neg_inf :: "('a::real_normed_vector) poly ⇒ 'a" where
"poly_neg_inf p ≡ if even (degree p) then sgn (coeff p (degree p))
else -sgn (coeff p (degree p))"
lemma poly_inf_0_iff[simp]:
"poly_inf p = 0 ⟷ p = 0" "poly_neg_inf p = 0 ⟷ p = 0"
by (auto simp: poly_inf_def poly_neg_inf_def sgn_zero_iff)
lemma poly_inf_mult[simp]:
fixes p :: "('a::real_normed_field) poly"
shows "poly_inf (p*q) = poly_inf p * poly_inf q"
"poly_neg_inf (p*q) = poly_neg_inf p * poly_neg_inf q"
unfolding poly_inf_def poly_neg_inf_def
by ((cases "p = 0 ∨ q = 0",auto simp: sgn_zero_iff
degree_mult_eq[of p q] coeff_mult_degree_sum Real_Vector_Spaces.sgn_mult)[])+
lemma poly_neq_0_at_infinity:
assumes "(p :: real poly) ≠ 0"
shows "eventually (λx. poly p x ≠ 0) at_infinity"
proof-
from poly_roots_bounds[OF assms] guess l u .
note lu_props = this
define b where "b = max (-l) u"
show ?thesis
proof (subst eventually_at_infinity, rule exI[of _ b], clarsimp)
fix x assume A: "¦x¦ ≥ b" and B: "poly p x = 0"
show False
proof (cases "x ≥ 0")
case True
with A have "x ≥ u" unfolding b_def by simp
with lu_props(3, 6) show False by (metis sgn_zero_iff B)
next
case False
with A have "x ≤ l" unfolding b_def by simp
with lu_props(2, 5) show False by (metis sgn_zero_iff B)
qed
qed
qed
lemma poly_limit_aux:
fixes p :: "real poly"
defines "n ≡ degree p"
shows "((λx. poly p x / x ^ n) ⤏ coeff p n) at_infinity"
proof (subst filterlim_cong, rule refl, rule refl)
show "eventually (λx. poly p x / x^n = (∑i≤n. coeff p i / x^(n-i)))
at_infinity"
proof (rule eventually_mono)
show "eventually (λx::real. x ≠ 0) at_infinity"
by (simp add: eventually_at_infinity, rule exI[of _ 1], auto)
fix x :: real assume [simp]: "x ≠ 0"
show "poly p x / x ^ n = (∑i≤n. coeff p i / x ^ (n - i))"
by (simp add: n_def sum_divide_distrib power_diff poly_altdef)
qed
let ?a = "λi. if i = n then coeff p n else 0"
have "∀i∈{..n}. ((λx. coeff p i / x ^ (n - i)) ⤏ ?a i) at_infinity"
proof
fix i assume "i ∈ {..n}"
hence "i ≤ n" by simp
show "((λx. coeff p i / x ^ (n - i)) ⤏ ?a i) at_infinity"
proof (cases "i = n")
case True
thus ?thesis by (intro tendstoI, subst eventually_at_infinity,
intro exI[of _ 1], simp add: dist_real_def)
next
case False
hence "n - i > 0" using ‹i ≤ n› by simp
from tendsto_inverse_0 and divide_real_def[of 1]
have "((λx. 1 / x :: real) ⤏ 0) at_infinity" by simp
from tendsto_power[OF this, of "n - i"]
have "((λx::real. 1 / x ^ (n - i)) ⤏ 0) at_infinity"
using ‹n - i > 0› by (simp add: power_0_left power_one_over)
from tendsto_mult_right_zero[OF this, of "coeff p i"]
have "((λx. coeff p i / x ^ (n - i)) ⤏ 0) at_infinity"
by (simp add: field_simps)
thus ?thesis using False by simp
qed
qed
hence "((λx. ∑i≤n. coeff p i / x^(n-i)) ⤏ (∑i≤n. ?a i)) at_infinity"
by (force intro!: tendsto_sum)
also have "(∑i≤n. ?a i) = coeff p n" by (subst sum.delta, simp_all)
finally show "((λx. ∑i≤n. coeff p i / x^(n-i)) ⤏ coeff p n) at_infinity" .
qed
lemma poly_at_top_at_top:
fixes p :: "real poly"
assumes "degree p ≥ 1" "coeff p (degree p) > 0"
shows "LIM x at_top. poly p x :> at_top"
proof-
let ?n = "degree p"
define f g where "f x = poly p x / x^?n" and "g x = x ^ ?n" for x :: real
from poly_limit_aux have "(f ⤏ coeff p (degree p)) at_top"
using tendsto_mono at_top_le_at_infinity unfolding f_def by blast
moreover from assms
have "LIM x at_top. g x :> at_top"
by (auto simp add: g_def intro!: filterlim_pow_at_top filterlim_ident)
ultimately have "LIM x at_top. f x * g x :> at_top"
using filterlim_tendsto_pos_mult_at_top assms by simp
also have "eventually (λx. f x * g x = poly p x) at_top"
unfolding f_def g_def
by (subst eventually_at_top_linorder, rule exI[of _ 1],
simp add: poly_altdef field_simps sum_distrib_left power_diff)
note filterlim_cong[OF refl refl this]
finally show ?thesis .
qed
lemma poly_at_bot_at_top:
fixes p :: "real poly"
assumes "degree p ≥ 1" "coeff p (degree p) < 0"
shows "LIM x at_top. poly p x :> at_bot"
proof-
from poly_at_top_at_top[of "-p"] and assms
have "LIM x at_top. -poly p x :> at_top" by simp
thus ?thesis by (simp add: filterlim_uminus_at_bot)
qed
lemma poly_lim_inf:
"eventually (λx::real. sgn (poly p x) = poly_inf p) at_top"
proof (cases "degree p ≥ 1")
case False
hence "degree p = 0" by simp
then obtain c where "p = [:c:]" by (cases p, auto split: if_split_asm)
thus ?thesis
by (simp add: eventually_at_top_linorder poly_inf_def)
next
case True
note deg = this
let ?lc = "coeff p (degree p)"
from True have "?lc ≠ 0" by force
show ?thesis
proof (cases "?lc > 0")
case True
from poly_at_top_at_top[OF deg this]
obtain x⇩0 where "⋀x. x ≥ x⇩0 ⟹ poly p x ≥ 1"
by (fastforce simp: filterlim_at_top
eventually_at_top_linorder less_eq_real_def)
hence "⋀x. x ≥ x⇩0 ⟹ sgn (poly p x) = 1" by force
thus ?thesis by (simp only: eventually_at_top_linorder poly_inf_def,
intro exI[of _ x⇩0], simp add: True)
next
case False
hence "?lc < 0" using ‹?lc ≠ 0› by linarith
from poly_at_bot_at_top[OF deg this]
obtain x⇩0 where "⋀x. x ≥ x⇩0 ⟹ poly p x ≤ -1"
by (fastforce simp: filterlim_at_bot
eventually_at_top_linorder less_eq_real_def)
hence "⋀x. x ≥ x⇩0 ⟹ sgn (poly p x) = -1" by force
thus ?thesis by (simp only: eventually_at_top_linorder poly_inf_def,
intro exI[of _ x⇩0], simp add: ‹?lc < 0›)
qed
qed
lemma poly_at_top_or_bot_at_bot:
fixes p :: "real poly"
assumes "degree p ≥ 1" "coeff p (degree p) > 0"
shows "LIM x at_bot. poly p x :> (if even (degree p) then at_top else at_bot)"
proof-
let ?n = "degree p"
define f g where "f x = poly p x / x ^ ?n" and "g x = x ^ ?n" for x :: real
from poly_limit_aux have "(f ⤏ coeff p (degree p)) at_bot"
using tendsto_mono at_bot_le_at_infinity by (force simp: f_def [abs_def])
moreover from assms
have "LIM x at_bot. g x :> (if even (degree p) then at_top else at_bot)"
by (auto simp add: g_def split: if_split_asm intro: filterlim_pow_at_bot_even filterlim_pow_at_bot_odd filterlim_ident)
ultimately have "LIM x at_bot. f x * g x :>
(if even ?n then at_top else at_bot)"
by (auto simp: assms intro: filterlim_tendsto_pos_mult_at_top
filterlim_tendsto_pos_mult_at_bot)
also have "eventually (λx. f x * g x = poly p x) at_bot"
unfolding f_def g_def
by (subst eventually_at_bot_linorder, rule exI[of _ "-1"],
simp add: poly_altdef field_simps sum_distrib_left power_diff)
note filterlim_cong[OF refl refl this]
finally show ?thesis .
qed
lemma poly_at_bot_or_top_at_bot:
fixes p :: "real poly"
assumes "degree p ≥ 1" "coeff p (degree p) < 0"
shows "LIM x at_bot. poly p x :> (if even (degree p) then at_bot else at_top)"
proof-
from poly_at_top_or_bot_at_bot[of "-p"] and assms
have "LIM x at_bot. -poly p x :>
(if even (degree p) then at_top else at_bot)" by simp
thus ?thesis by (auto simp: filterlim_uminus_at_bot)
qed
lemma poly_lim_neg_inf:
"eventually (λx::real. sgn (poly p x) = poly_neg_inf p) at_bot"
proof (cases "degree p ≥ 1")
case False
hence "degree p = 0" by simp
then obtain c where "p = [:c:]" by (cases p, auto split: if_split_asm)
thus ?thesis
by (simp add: eventually_at_bot_linorder poly_neg_inf_def)
next
case True
note deg = this
let ?lc = "coeff p (degree p)"
from True have "?lc ≠ 0" by force
show ?thesis
proof (cases "?lc > 0")
case True
note lc_pos = this
show ?thesis
proof (cases "even (degree p)")
case True
from poly_at_top_or_bot_at_bot[OF deg lc_pos] and True
obtain x⇩0 where "⋀x. x ≤ x⇩0 ⟹ poly p x ≥ 1"
by (fastforce simp add: filterlim_at_top filterlim_at_bot
eventually_at_bot_linorder less_eq_real_def)
hence "⋀x. x ≤ x⇩0 ⟹ sgn (poly p x) = 1" by force
thus ?thesis
by (simp add: True eventually_at_bot_linorder poly_neg_inf_def,
intro exI[of _ x⇩0], simp add: lc_pos)
next
case False
from poly_at_top_or_bot_at_bot[OF deg lc_pos] and False
obtain x⇩0 where "⋀x. x ≤ x⇩0 ⟹ poly p x ≤ -1"
by (fastforce simp add: filterlim_at_bot
eventually_at_bot_linorder less_eq_real_def)
hence "⋀x. x ≤ x⇩0 ⟹ sgn (poly p x) = -1" by force
thus ?thesis
by (simp add: False eventually_at_bot_linorder poly_neg_inf_def,
intro exI[of _ x⇩0], simp add: lc_pos)
qed
next
case False
hence lc_neg: "?lc < 0" using ‹?lc ≠ 0› by linarith
show ?thesis
proof (cases "even (degree p)")
case True
with poly_at_bot_or_top_at_bot[OF deg lc_neg]
obtain x⇩0 where "⋀x. x ≤ x⇩0 ⟹ poly p x ≤ -1"
by (fastforce simp: filterlim_at_bot
eventually_at_bot_linorder less_eq_real_def)
hence "⋀x. x ≤ x⇩0 ⟹ sgn (poly p x) = -1" by force
thus ?thesis
by (simp only: True eventually_at_bot_linorder poly_neg_inf_def,
intro exI[of _ x⇩0], simp add: lc_neg)
next
case False
with poly_at_bot_or_top_at_bot[OF deg lc_neg]
obtain x⇩0 where "⋀x. x ≤ x⇩0 ⟹ poly p x ≥ 1"
by (fastforce simp: filterlim_at_top
eventually_at_bot_linorder less_eq_real_def)
hence "⋀x. x ≤ x⇩0 ⟹ sgn (poly p x) = 1" by force
thus ?thesis
by (simp only: False eventually_at_bot_linorder poly_neg_inf_def,
intro exI[of _ x⇩0], simp add: lc_neg)
qed
qed
qed
subsubsection ‹Signs of polynomials for sufficiently large values›
lemma polys_inf_sign_thresholds:
assumes "finite (ps :: real poly set)"
obtains l u
where "l ≤ u"
and "⋀p. ⟦p ∈ ps; p ≠ 0⟧ ⟹
{x. l < x ∧ x ≤ u ∧ poly p x = 0} = {x. poly p x = 0}"
and "⋀p x. ⟦p ∈ ps; x ≥ u⟧ ⟹ sgn (poly p x) = poly_inf p"
and "⋀p x. ⟦p ∈ ps; x ≤ l⟧ ⟹ sgn (poly p x) = poly_neg_inf p"
proof goal_cases
case prems: 1
have "∃l u. l ≤ u ∧ (∀p x. p ∈ ps ∧ x ≥ u ⟶ sgn (poly p x) = poly_inf p) ∧
(∀p x. p ∈ ps ∧ x ≤ l ⟶ sgn (poly p x) = poly_neg_inf p)"
(is "∃l u. ?P ps l u")
proof (induction rule: finite_subset_induct[OF assms(1), where A = UNIV])
case 1
show ?case by simp
next
case 2
show ?case by (intro exI[of _ 42], simp)
next
case prems: (3 p ps)
from prems(4) obtain l u where lu_props: "?P ps l u" by blast
from poly_lim_inf obtain u'
where u'_props: "∀x≥u'. sgn (poly p x) = poly_inf p"
by (force simp add: eventually_at_top_linorder)
from poly_lim_neg_inf obtain l'
where l'_props: "∀x≤l'. sgn (poly p x) = poly_neg_inf p"
by (force simp add: eventually_at_bot_linorder)
show ?case
by (rule exI[of _ "min l l'"], rule exI[of _ "max u u'"],
insert lu_props l'_props u'_props, auto)
qed
then obtain l u where lu_props: "l ≤ u"
"⋀p x. p ∈ ps ⟹ u ≤ x ⟹ sgn (poly p x) = poly_inf p"
"⋀p x. p ∈ ps ⟹ x ≤ l ⟹ sgn (poly p x) = poly_neg_inf p" by blast
moreover {
fix p x assume A: "p ∈ ps" "p ≠ 0" "poly p x = 0"
from A have "l < x" "x < u"
by (auto simp: not_le[symmetric] dest: lu_props(2,3))
}
note A = this
have "⋀p. p ∈ ps ⟹ p ≠ 0 ⟹
{x. l < x ∧ x ≤ u ∧ poly p x = 0} = {x. poly p x = 0}"
by (auto dest: A)
from prems[OF lu_props(1) this lu_props(2,3)] show thesis .
qed
subsubsection ‹Positivity of polynomials›
lemma poly_pos:
"(∀x::real. poly p x > 0) ⟷ poly_inf p = 1 ∧ (∀x. poly p x ≠ 0)"
proof (intro iffI conjI)
assume A: "∀x::real. poly p x > 0"
have "⋀x. poly p (x::real) > 0 ⟹ poly p x ≠ 0" by simp
with A show "∀x::real. poly p x ≠ 0" by simp
from poly_lim_inf obtain x where "sgn (poly p x) = poly_inf p"
by (auto simp: eventually_at_top_linorder)
with A show "poly_inf p = 1"
by (simp add: sgn_real_def split: if_split_asm)
next
assume "poly_inf p = 1 ∧ (∀x. poly p x ≠ 0)"
hence A: "poly_inf p = 1" and B: "(∀x. poly p x ≠ 0)" by simp_all
from poly_lim_inf obtain x where C: "sgn (poly p x) = poly_inf p"
by (auto simp: eventually_at_top_linorder)
show "∀x. poly p x > 0"
proof (rule ccontr)
assume "¬(∀x. poly p x > 0)"
then obtain x' where "poly p x' ≤ 0" by (auto simp: not_less)
with A and C have "sgn (poly p x') ≠ sgn (poly p x)"
by (auto simp: sgn_real_def split: if_split_asm)
from poly_different_sign_imp_root'[OF this] and B
show False by blast
qed
qed
lemma poly_pos_greater:
"(∀x::real. x > a ⟶ poly p x > 0) ⟷
poly_inf p = 1 ∧ (∀x. x > a ⟶ poly p x ≠ 0)"
proof (intro iffI conjI)
assume A: "∀x::real. x > a ⟶ poly p x > 0"
have "⋀x. poly p (x::real) > 0 ⟹ poly p x ≠ 0" by simp
with A show "∀x::real. x > a ⟶ poly p x ≠ 0" by auto
from poly_lim_inf obtain x⇩0 where
"∀x≥x⇩0. sgn (poly p x) = poly_inf p"
by (auto simp: eventually_at_top_linorder)
hence "poly_inf p = sgn (poly p (max x⇩0 (a + 1)))" by simp
also from A have "... = 1" by force
finally show "poly_inf p = 1" .
next
assume "poly_inf p = 1 ∧ (∀x. x > a ⟶ poly p x ≠ 0)"
hence A: "poly_inf p = 1" and
B: "(∀x. x > a ⟶ poly p x ≠ 0)" by simp_all
from poly_lim_inf obtain x⇩0 where
C: "∀x≥x⇩0. sgn (poly p x) = poly_inf p"
by (auto simp: eventually_at_top_linorder)
hence "sgn (poly p (max x⇩0 (a+1))) = poly_inf p" by simp
with A have D: "sgn (poly p (max x⇩0 (a+1))) = 1" by simp
show "∀x. x > a ⟶ poly p x > 0"
proof (rule ccontr)
assume "¬(∀x. x > a ⟶ poly p x > 0)"
then obtain x' where "x' > a" "poly p x' ≤ 0" by (auto simp: not_less)
with A and D have E: "sgn (poly p x') ≠ sgn (poly p (max x⇩0(a+1)))"
by (auto simp: sgn_real_def split: if_split_asm)
show False
apply (cases x' "max x⇩0 (a+1)" rule: linorder_cases)
using B E ‹x' > a›
apply (force dest!: poly_different_sign_imp_root[of _ _ p])+
done
qed
qed
lemma poly_pos_geq:
"(∀x::real. x ≥ a ⟶ poly p x > 0) ⟷
poly_inf p = 1 ∧ (∀x. x ≥ a ⟶ poly p x ≠ 0)"
proof (intro iffI conjI)
assume A: "∀x::real. x ≥ a ⟶ poly p x > 0"
hence "∀x::real. x > a ⟶ poly p x > 0" by simp
also note poly_pos_greater
finally have "poly_inf p = 1" "(∀x>a. poly p x ≠ 0)" by simp_all
moreover from A have "poly p a > 0" by simp
ultimately show "poly_inf p = 1" "∀x≥a. poly p x ≠ 0"
by (auto simp: less_eq_real_def)
next
assume "poly_inf p = 1 ∧ (∀x. x ≥ a ⟶ poly p x ≠ 0)"
hence A: "poly_inf p = 1" and
B: "poly p a ≠ 0" and C: "∀x>a. poly p x ≠ 0" by simp_all
from A and C and poly_pos_greater have "∀x>a. poly p x > 0" by simp
moreover with B C poly_IVT_pos[of a "a+1" p] have "poly p a > 0" by force
ultimately show "∀x≥a. poly p x > 0" by (auto simp: less_eq_real_def)
qed
lemma poly_pos_less:
"(∀x::real. x < a ⟶ poly p x > 0) ⟷
poly_neg_inf p = 1 ∧ (∀x. x < a ⟶ poly p x ≠ 0)"
proof (intro iffI conjI)
assume A: "∀x::real. x < a ⟶ poly p x > 0"
have "⋀x. poly p (x::real) > 0 ⟹ poly p x ≠ 0" by simp
with A show "∀x::real. x < a ⟶ poly p x ≠ 0" by auto
from poly_lim_neg_inf obtain x⇩0 where
"∀x≤x⇩0. sgn (poly p x) = poly_neg_inf p"
by (auto simp: eventually_at_bot_linorder)
hence "poly_neg_inf p = sgn (poly p (min x⇩0 (a - 1)))" by simp
also from A have "... = 1" by force
finally show "poly_neg_inf p = 1" .
next
assume "poly_neg_inf p = 1 ∧ (∀x. x < a ⟶ poly p x ≠ 0)"
hence A: "poly_neg_inf p = 1" and
B: "(∀x. x < a ⟶ poly p x ≠ 0)" by simp_all
from poly_lim_neg_inf obtain x⇩0 where
C: "∀x≤x⇩0. sgn (poly p x) = poly_neg_inf p"
by (auto simp: eventually_at_bot_linorder)
hence "sgn (poly p (min x⇩0 (a - 1))) = poly_neg_inf p" by simp
with A have D: "sgn (poly p (min x⇩0 (a - 1))) = 1" by simp
show "∀x. x < a ⟶ poly p x > 0"
proof (rule ccontr)
assume "¬(∀x. x < a ⟶ poly p x > 0)"
then obtain x' where "x' < a" "poly p x' ≤ 0" by (auto simp: not_less)
with A and D have E: "sgn (poly p x') ≠ sgn (poly p (min x⇩0 (a - 1)))"
by (auto simp: sgn_real_def split: if_split_asm)
show False
apply (cases x' "min x⇩0 (a - 1)" rule: linorder_cases)
using B E ‹x' < a›
apply (auto dest!: poly_different_sign_imp_root[of _ _ p])+
done
qed
qed
lemma poly_pos_leq:
"(∀x::real. x ≤ a ⟶ poly p x > 0) ⟷
poly_neg_inf p = 1 ∧ (∀x. x ≤ a ⟶ poly p x ≠ 0)"
proof (intro iffI conjI)
assume A: "∀x::real. x ≤ a ⟶ poly p x > 0"
hence "∀x::real. x < a ⟶ poly p x > 0" by simp
also note poly_pos_less
finally have "poly_neg_inf p = 1" "(∀x<a. poly p x ≠ 0)" by simp_all
moreover from A have "poly p a > 0" by simp
ultimately show "poly_neg_inf p = 1" "∀x≤a. poly p x ≠ 0"
by (auto simp: less_eq_real_def)
next
assume "poly_neg_inf p = 1 ∧ (∀x. x ≤ a ⟶ poly p x ≠ 0)"
hence A: "poly_neg_inf p = 1" and
B: "poly p a ≠ 0" and C: "∀x<a. poly p x ≠ 0" by simp_all
from A and C and poly_pos_less have "∀x<a. poly p x > 0" by simp
moreover with B C poly_IVT_neg[of "a - 1" a p] have "poly p a > 0" by force
ultimately show "∀x≤a. poly p x > 0" by (auto simp: less_eq_real_def)
qed
lemma poly_pos_between_less_less:
"(∀x::real. a < x ∧ x < b ⟶ poly p x > 0) ⟷
(a ≥ b ∨ poly p ((a+b)/2) > 0) ∧ (∀x. a < x ∧ x < b ⟶ poly p x ≠ 0)"
proof (intro iffI conjI)
assume A: "∀x. a < x ∧ x < b ⟶ poly p x > 0"
have "⋀x. poly p (x::real) > 0 ⟹ poly p x ≠ 0" by simp
with A show "∀x::real. a < x ∧ x < b ⟶ poly p x ≠ 0" by auto
from A show "a ≥ b ∨ poly p ((a+b)/2) > 0" by (cases "a < b", auto)
next
assume "(b ≤ a ∨ 0 < poly p ((a+b)/2)) ∧ (∀x. a<x ∧ x<b ⟶ poly p x ≠ 0)"
hence A: "b ≤ a ∨ 0 < poly p ((a+b)/2)" and
B: "∀x. a<x ∧ x<b ⟶ poly p x ≠ 0" by simp_all
show "∀x. a < x ∧ x < b ⟶ poly p x > 0"
proof (cases "a ≥ b", simp, clarify, rule_tac ccontr,
simp only: not_le not_less)
fix x assume "a < b" "a < x" "x < b" "poly p x ≤ 0"
with B have "poly p x < 0" by (simp add: less_eq_real_def)
moreover from A and ‹a < b› have "poly p ((a+b)/2) > 0" by simp
ultimately have "sgn (poly p x) ≠ sgn (poly p ((a+b)/2))" by simp
thus False using B
apply (cases x "(a+b)/2" rule: linorder_cases)
apply (drule poly_different_sign_imp_root[of _ _ p], assumption,
insert ‹a < b› ‹a < x› ‹x < b› , force) []
apply simp
apply (drule poly_different_sign_imp_root[of _ _ p], simp,
insert ‹a < b› ‹a < x› ‹x < b› , force)
done
qed
qed
lemma poly_pos_between_less_leq:
"(∀x::real. a < x ∧ x ≤ b ⟶ poly p x > 0) ⟷
(a ≥ b ∨ poly p b > 0) ∧ (∀x. a < x ∧ x ≤ b ⟶ poly p x ≠ 0)"
proof (intro iffI conjI)
assume A: "∀x. a < x ∧ x ≤ b ⟶ poly p x > 0"
have "⋀x. poly p (x::real) > 0 ⟹ poly p x ≠ 0" by simp
with A show "∀x::real. a < x ∧ x ≤ b ⟶ poly p x ≠ 0" by auto
from A show "a ≥ b ∨ poly p b > 0" by (cases "a < b", auto)
next
assume "(b ≤ a ∨ 0 < poly p b) ∧ (∀x. a<x ∧ x≤b ⟶ poly p x ≠ 0)"
hence A: "b ≤ a ∨ 0 < poly p b" and B: "∀x. a<x ∧ x≤b ⟶ poly p x ≠ 0"
by simp_all
show "∀x. a < x ∧ x ≤ b ⟶ poly p x > 0"
proof (cases "a ≥ b", simp, clarify, rule_tac ccontr,
simp only: not_le not_less)
fix x assume "a < b" "a < x" "x ≤ b" "poly p x ≤ 0"
with B have "poly p x < 0" by (simp add: less_eq_real_def)
moreover from A and ‹a < b› have "poly p b > 0" by simp
ultimately have "x < b" using ‹x ≤ b› by (auto simp: less_eq_real_def)
from ‹poly p x < 0› and ‹poly p b > 0›
have "sgn (poly p x) ≠ sgn (poly p b)" by simp
from poly_different_sign_imp_root[OF ‹x < b› this] and B and ‹x > a›
show False by auto
qed
qed
lemma poly_pos_between_leq_less:
"(∀x::real. a ≤ x ∧ x < b ⟶ poly p x > 0) ⟷
(a ≥ b ∨ poly p a > 0) ∧ (∀x. a ≤ x ∧ x < b ⟶ poly p x ≠ 0)"
proof (intro iffI conjI)
assume A: "∀x. a ≤ x ∧ x < b ⟶ poly p x > 0"
have "⋀x. poly p (x::real) > 0 ⟹ poly p x ≠ 0" by simp
with A show "∀x::real. a ≤ x ∧ x < b ⟶ poly p x ≠ 0" by auto
from A show "a ≥ b ∨ poly p a > 0" by (cases "a < b", auto)
next
assume "(b ≤ a ∨ 0 < poly p a) ∧ (∀x. a≤x ∧ x<b ⟶ poly p x ≠ 0)"
hence A: "b ≤ a ∨ 0 < poly p a" and B: "∀x. a≤x ∧ x<b ⟶ poly p x ≠ 0"
by simp_all
show "∀x. a ≤ x ∧ x < b ⟶ poly p x > 0"
proof (cases "a ≥ b", simp, clarify, rule_tac ccontr,
simp only: not_le not_less)
fix x assume "a < b" "a ≤ x" "x < b" "poly p x ≤ 0"
with B have "poly p x < 0" by (simp add: less_eq_real_def)
moreover from A and ‹a < b› have "poly p a > 0" by simp
ultimately have "x > a" using ‹x ≥ a› by (auto simp: less_eq_real_def)
from ‹poly p x < 0› and ‹poly p a > 0›
have "sgn (poly p a) ≠ sgn (poly p x)" by simp
from poly_different_sign_imp_root[OF ‹x > a› this] and B and ‹x < b›
show False by auto
qed
qed
lemma poly_pos_between_leq_leq:
"(∀x::real. a ≤ x ∧ x ≤ b ⟶ poly p x > 0) ⟷
(a > b ∨ poly p a > 0) ∧ (∀x. a ≤ x ∧ x ≤ b ⟶ poly p x ≠ 0)"
proof (intro iffI conjI)
assume A: "∀x. a ≤ x ∧ x ≤ b ⟶ poly p x > 0"
have "⋀x. poly p (x::real) > 0 ⟹ poly p x ≠ 0" by simp
with A show "∀x::real. a ≤ x ∧ x ≤ b ⟶ poly p x ≠ 0" by auto
from A show "a > b ∨ poly p a > 0" by (cases "a ≤ b", auto)
next
assume "(b < a ∨ 0 < poly p a) ∧ (∀x. a≤x ∧ x≤b ⟶ poly p x ≠ 0)"
hence A: "b < a ∨ 0 < poly p a" and B: "∀x. a≤x ∧ x≤b ⟶ poly p x ≠ 0"
by simp_all
show "∀x. a ≤ x ∧ x ≤ b ⟶ poly p x > 0"
proof (cases "a > b", simp, clarify, rule_tac ccontr,
simp only: not_le not_less)
fix x assume "a ≤ b" "a ≤ x" "x ≤ b" "poly p x ≤ 0"
with B have "poly p x < 0" by (simp add: less_eq_real_def)
moreover from A and ‹a ≤ b› have "poly p a > 0" by simp
ultimately have "x > a" using ‹x ≥ a› by (auto simp: less_eq_real_def)
from ‹poly p x < 0› and ‹poly p a > 0›
have "sgn (poly p a) ≠ sgn (poly p x)" by simp
from poly_different_sign_imp_root[OF ‹x > a› this] and B and ‹x ≤ b›
show False by auto
qed
qed
end