Theory Preliminaries

section ‹Preliminaries›
theory Preliminaries
  imports 
    Main
    HOL.Real
    "HOL-Library.FuncSet"
begin

lemma fact_approx_add: "fact (l + n) ≤ fact l * (real l + real n) ^ n" 
proof (induct n arbitrary: l)
  case (Suc n l)
  have "fact (l + Suc n) = (real l + Suc n) * fact (l + n)" by simp
  also have "… ≤ (real l + Suc n) * (fact l * (real l + real n) ^ n)" 
    by (intro mult_left_mono[OF Suc], auto)
  also have "… = fact l * ((real l + Suc n) * (real l + real n) ^ n)" by simp
  also have "… ≤ fact l * ((real l + Suc n) * (real l + real (Suc n)) ^ n)" 
    by (rule mult_left_mono, rule mult_left_mono, rule power_mono, auto)
  finally show ?case by simp
qed simp

lemma fact_approx_minus: assumes "k ≥ n"
  shows "fact k ≤ fact (k - n) * (real k ^ n)"
proof -
  define l where "l = k - n" 
  from assms have k: "k = l + n" unfolding l_def by auto
  show ?thesis unfolding k using fact_approx_add[of l n] by simp
qed

lemma fact_approx_upper_add: assumes al: "a ≤ Suc l" shows "fact l * real a ^ n ≤ fact (l + n)" 
proof (induct n)
  case (Suc n)
  have "fact l * real a ^ (Suc n) = (fact l * real a ^ n) * real a" by simp
  also have "… ≤ fact (l + n) * real a" 
    by (rule mult_right_mono[OF Suc], auto)
  also have "… ≤ fact (l + n) * real (Suc (l + n))" 
    by (intro mult_left_mono, insert al, auto)
  also have "… = fact (Suc (l + n))" by simp
  finally show ?case by simp
qed simp

lemma fact_approx_upper_minus: assumes "n ≤ k" and "n + a ≤ Suc k" 
  shows "fact (k - n) * real a ^ n ≤ fact k" 
proof -
  define l where "l = k - n" 
  from assms have k: "k = l + n" unfolding l_def by auto
  show ?thesis using assms unfolding k 
    apply simp
    apply (rule fact_approx_upper_add, insert assms, auto simp: l_def)
    done
qed

lemma choose_mono: "n ≤ m ⟹ n choose k ≤ m choose k" 
  unfolding binomial_def
  by (rule card_mono, auto)

lemma div_mult_le: "(a div b) * c ≤ (a * c) div (b :: nat)"
  by (metis div_mult2_eq div_mult_mult2 mult.commute mult_0_right times_div_less_eq_dividend)

lemma div_mult_pow_le: "(a div b)^n ≤ a^n div (b :: nat)^n"  
proof (cases "b = 0")
  case True
  thus ?thesis by (cases n, auto)
next
  case b: False  
  then obtain c d where a: "a = b * c + d" and id: "c = a div b" "d = a mod b" by auto
  have "(a div b)^n = c^n" unfolding id by simp
  also have "… = (b * c)^n div b^n" using b
    by (metis div_power dvd_triv_left nonzero_mult_div_cancel_left)
  also have "… ≤ (b * c + d)^n div b^n" 
    by (rule div_le_mono, rule power_mono, auto)
  also have "… = a^n div b^n " unfolding a by simp
  finally show ?thesis .
qed

lemma choose_inj_right:
  assumes id: "(n choose l) = (k choose l)" 
    and n0: "n choose l ≠ 0" 
    and l0:  "l ≠ 0" 
  shows "n = k"
proof (rule ccontr)
  assume nk: "n ≠ k" 
  define m where "m = min n k" 
  define M where "M = max n k" 
  from nk have mM: "m < M" unfolding m_def M_def by auto
  let ?new = "insert (M - 1) {0..< l - 1}" 
  let ?m = "{K ∈ Pow {0..<m}. card K = l}" 
  let ?M = "{K ∈ Pow {0..<M}. card K = l}" 
  from id n0 have lM :"l ≤ M" unfolding m_def M_def by auto
  from id have id: "(m choose l) = (M choose l)" 
    unfolding m_def M_def by auto
  from this[unfolded binomial_def]
  have "card ?M < Suc (card ?m)" 
    by auto
  also have "… = card (insert ?new ?m)" 
    by (rule sym, rule card_insert_disjoint, force, insert mM, auto)
  also have "… ≤ card (insert ?new ?M)" 
    by (rule card_mono, insert mM, auto)
  also have "insert ?new ?M = ?M" 
    by (insert mM lM l0, auto)
  finally show False by simp
qed


end