# Theory Liouville_Numbers_Misc

section ‹Liouville Numbers›
subsection ‹Preliminary lemmas›
theory Liouville_Numbers_Misc
imports
Complex_Main
"HOL-Computational_Algebra.Polynomial"
begin
text ‹
We will require these inequalities on factorials to show properties of the standard
construction later.
›
lemma fact_ineq: "n ≥ 1 ⟹ fact n + k ≤ fact (n + k)"
proof (induction k)
case (Suc k)
from Suc have "fact n + Suc k ≤ fact (n + k) + 1" by simp
also from Suc have "… ≤ fact (n + Suc k)" by simp
finally show ?case .
qed simp_all
lemma Ints_sum:
assumes "⋀x. x ∈ A ⟹ f x ∈ ℤ"
shows "sum f A ∈ ℤ"
by (cases "finite A", insert assms, induction A rule: finite_induct)
(auto intro!: Ints_add)
lemma suminf_split_initial_segment':
"summable (f :: nat ⇒ 'a::real_normed_vector) ⟹
suminf f = (∑n. f (n + k + 1)) + sum f {..k}"
by (subst suminf_split_initial_segment[of _ "Suc k"], assumption, subst lessThan_Suc_atMost)
simp_all
lemma Rats_eq_int_div_int': "(ℚ :: real set) = {of_int p / of_int q |p q. q > 0}"
proof safe
fix x :: real assume "x ∈ ℚ"
then obtain p q where pq: "x = of_int p / of_int q" "q ≠ 0"
by (subst (asm) Rats_eq_int_div_int) auto
show "∃p q. x = real_of_int p / real_of_int q ∧ 0 < q"
proof (cases "q > 0")
case False
show ?thesis by (rule exI[of _ "-p"], rule exI[of _ "-q"]) (insert False pq, auto)
qed (insert pq, force)
qed auto
lemma Rats_cases':
assumes "(x :: real) ∈ ℚ"
obtains p q where "q > 0" "x = of_int p / of_int q"
using assms by (subst (asm) Rats_eq_int_div_int') auto
text ‹
The following inequality gives a lower bound for the absolute value of an
integer polynomial at a rational point that is not a root.
›
lemma int_poly_rat_no_root_ge:
fixes p :: "real poly" and a b :: int
assumes "⋀n. coeff p n ∈ ℤ"
assumes "b > 0" "poly p (a / b) ≠ 0"
defines "n ≡ degree p"
shows "abs (poly p (a / b)) ≥ 1 / of_int b ^ n"
proof -
let ?S = "(∑i≤n. coeff p i * of_int a ^ i * (of_int b ^ (n - i)))"
from ‹b > 0› have eq: "?S = of_int b ^ n * poly p (a / b)"
by (simp add: poly_altdef power_divide mult_ac n_def sum_distrib_left power_diff)
have "?S ∈ ℤ" by (intro Ints_sum Ints_mult assms Ints_power) simp_all
moreover from assms have "?S ≠ 0" by (subst eq) auto
ultimately have "abs ?S ≥ 1" by (elim Ints_cases) simp
with eq ‹b > 0› show ?thesis by (simp add: field_simps abs_mult)
qed
end