Theory Liouville_Numbers_Misc

  File:    Liouville_Numbers_Misc.thy
  Author:  Manuel Eberl <>


section ‹Liouville Numbers›
subsection ‹Preliminary lemmas›
theory Liouville_Numbers_Misc

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) 

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 = "(in. 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)