Theory Liouville_Numbers_Misc

(* 
  File:    Liouville_Numbers_Misc.thy
  Author:  Manuel Eberl <manuel@pruvisto.org>

*)

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