Theory Binomial_Int

(* Author: Alexander Maletzky *)

section ‹Integer Binomial Coefficients›

theory Binomial_Int
  imports Complex_Main
begin

text ‹Restore original sort constraints:›
setup ‹Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::{semidom_divide,semiring_char_0} ⇒ nat ⇒ 'a"})›

subsection ‹Inequalities›

lemma binomial_mono:
  assumes "m ≤ n"
  shows "m choose k ≤ n choose k"
  by (simp add: assms binomial_right_mono)

lemma binomial_plus_le:
  assumes "0 < k"
  shows "(m choose k) + (n choose k) ≤ (m + n) choose k"
proof -
  define k0 where "k0 = k - 1"
  with assms have k: "k = Suc k0" by simp
  show ?thesis unfolding k
  proof (induct n)
    case 0
    show ?case by simp
  next
    case (Suc n)
    then show ?case
      by (simp add: add.left_commute add_le_mono binomial_right_mono)
  qed
qed

lemma binomial_ineq_1: "2 * ((n + i) choose k) ≤ (n choose k) + ((n + 2 * i) choose k)"
proof (cases k)
  case 0
  thus ?thesis by simp
next
  case k: (Suc k0)
  show ?thesis unfolding k
  proof (induct i)
    case 0
    thus ?case by simp
  next
    case (Suc i)
    have "2 * (n + Suc i choose Suc k0) = 2 * (n + i choose k0) + 2 * (n + i choose Suc k0)"
      by simp
    also have "… ≤ ((n + 2 * i choose k0) + (Suc (n + 2 * i) choose k0)) + ((n choose Suc k0) + (n + 2 * i choose Suc k0))"
    proof (rule add_mono)
      have "n + i choose k0 ≤ n + 2 * i choose k0" 
        by (rule binomial_mono) simp
      moreover have "n + 2 * i choose k0 ≤ Suc (n + 2 * i) choose k0" 
        by (rule binomial_mono) simp
      ultimately show "2 * (n + i choose k0) ≤ (n + 2 * i choose k0) + (Suc (n + 2 * i) choose k0)"
        by simp
    qed (fact Suc)
    also have "… = (n choose Suc k0) + (n + 2 * Suc i choose Suc k0)" by simp
    finally show ?case .
  qed
qed

lemma gbinomial_int_mono:
  assumes "0 ≤ x" and "x ≤ (y::int)"
  shows "x gchoose k ≤ y gchoose k"
proof -
  from assms have "nat x ≤ nat y" by simp
  hence "nat x choose k ≤ nat y choose k" by (rule binomial_mono)
  hence "int (nat x choose k) ≤ int (nat y choose k)" by (simp only: zle_int)
  hence "int (nat x) gchoose k ≤ int (nat y) gchoose k" by (simp only: int_binomial)
  with assms show ?thesis by simp
qed

lemma gbinomial_int_plus_le:
  assumes "0 < k" and "0 ≤ x" and "0 ≤ (y::int)"
  shows "(x gchoose k) + (y gchoose k) ≤ (x + y) gchoose k"
proof -
  from assms(1) have "(nat x choose k) + (nat y choose k) ≤ nat x + nat y choose k"
    by (rule binomial_plus_le)
  hence "int ((nat x choose k) + (nat y choose k)) ≤ int (nat x + nat y choose k)"
    by (simp only: zle_int)
  hence "(int (nat x) gchoose k) + (int (nat y) gchoose k) ≤ int (nat x) + int (nat y) gchoose k"
    by (simp only: int_plus int_binomial)
  with assms(2, 3) show ?thesis by simp
qed

lemma binomial_int_ineq_1:
  assumes "0 ≤ x" and "0 ≤ (y::int)"
  shows "2 * (x + y gchoose k) ≤ (x gchoose k) + ((x + 2 * y) gchoose k)"
proof -
  from binomial_ineq_1[of "nat x" "nat y" k]
  have "int (2 * (nat x + nat y choose k)) ≤ int ((nat x choose k) + (nat x + 2 * nat y choose k))"
    by (simp only: zle_int)
  hence "2 * (int (nat x) + int (nat y) gchoose k) ≤ (int (nat x) gchoose k) + (int (nat x) + 2 * int (nat y) gchoose k)"
    by (simp only: int_binomial int_plus int_ops(7)) simp
  with assms show ?thesis by simp
qed

corollary binomial_int_ineq_2:
  assumes "0 ≤ y" and "y ≤ (x::int)"
  shows "2 * (x gchoose k) ≤ (x - y gchoose k) + (x + y gchoose k)"
proof -
  from assms(2) have "0 ≤ x - y" by simp
  hence "2 * ((x - y) + y gchoose k) ≤ (x - y gchoose k) + ((x - y + 2 * y) gchoose k)"
    using assms(1) by (rule binomial_int_ineq_1)
  thus ?thesis by smt
qed

corollary binomial_int_ineq_3:
  assumes "0 ≤ y" and "y ≤ 2 * (x::int)"
  shows "2 * (x gchoose k) ≤ (y gchoose k) + (2 * x - y gchoose k)"
proof (cases "y ≤ x")
  case True
  hence "0 ≤ x - y" by simp
  moreover from assms(1) have "x - y ≤ x" by simp
  ultimately have "2 * (x gchoose k) ≤ (x - (x - y) gchoose k) + (x + (x - y) gchoose k)"
    by (rule binomial_int_ineq_2)
  thus ?thesis by simp
next
  case False
  hence "0 ≤ y - x" by simp
  moreover from assms(2) have "y - x ≤ x" by simp
  ultimately have "2 * (x gchoose k) ≤ (x - (y - x) gchoose k) + (x + (y - x) gchoose k)"
    by (rule binomial_int_ineq_2)
  thus ?thesis by simp
qed

subsection ‹Backward Difference Operator›

definition bw_diff :: "('a ⇒ 'a) ⇒ 'a ⇒ 'a::{ab_group_add,one}"
  where "bw_diff f x = f x - f (x - 1)"

lemma bw_diff_const [simp]: "bw_diff (λ_. c) = (λ_. 0)"
  by (rule ext) (simp add: bw_diff_def)

lemma bw_diff_id [simp]: "bw_diff (λx. x) = (λ_. 1)"
  by (rule ext) (simp add: bw_diff_def)

lemma bw_diff_plus [simp]: "bw_diff (λx. f x + g x) = (λx. bw_diff f x + bw_diff g x)"
  by (rule ext) (simp add: bw_diff_def)

lemma bw_diff_uminus [simp]: "bw_diff (λx. - f x) = (λx. - bw_diff f x)"
  by (rule ext) (simp add: bw_diff_def)

lemma bw_diff_minus [simp]: "bw_diff (λx. f x - g x) = (λx. bw_diff f x - bw_diff g x)"
  by (rule ext) (simp add: bw_diff_def)

lemma bw_diff_const_pow: "(bw_diff ^^ k) (λ_. c) = (if k = 0 then λ_. c else (λ_. 0))"
  by (induct k, simp_all)

lemma bw_diff_id_pow:
  "(bw_diff ^^ k) (λx. x) = (if k = 0 then (λx. x) else if k = 1 then (λ_. 1) else (λ_. 0))"
  by (induct k, simp_all)

lemma bw_diff_plus_pow [simp]:
  "(bw_diff ^^ k) (λx. f x + g x) = (λx. (bw_diff ^^ k) f x + (bw_diff ^^ k) g x)"
  by (induct k, simp_all)

lemma bw_diff_uminus_pow [simp]: "(bw_diff ^^ k) (λx. - f x) = (λx. - (bw_diff ^^ k) f x)"
  by (induct k, simp_all)

lemma bw_diff_minus_pow [simp]:
  "(bw_diff ^^ k) (λx. f x - g x) = (λx. (bw_diff ^^ k) f x - (bw_diff ^^ k) g x)"
  by (induct k, simp_all)

lemma bw_diff_sum_pow [simp]:
  "(bw_diff ^^ k) (λx. (∑i∈I. f i x)) = (λx. (∑i∈I. (bw_diff ^^ k) (f i) x))"
  by (induct I rule: infinite_finite_induct, simp_all add: bw_diff_const_pow)

lemma bw_diff_gbinomial:
  assumes "0 < k"
  shows "bw_diff (λx::int. (x + n) gchoose k) = (λx. (x + n - 1) gchoose (k - 1))"
proof (rule ext)
  fix x::int
  from assms have eq: "Suc (k - Suc 0) = k" by simp
  have "x + n gchoose k = (x + n - 1) + 1 gchoose (Suc (k - 1))" by (simp add: eq)
  also have "… = (x + n - 1 gchoose k - 1) + ((x + n - 1) gchoose (Suc (k - 1)))"
    by (fact gbinomial_int_Suc_Suc)
  finally show "bw_diff (λx. x + n gchoose k) x = x + n - 1 gchoose (k - 1)"
    by (simp add: eq bw_diff_def algebra_simps)
qed

lemma bw_diff_gbinomial_pow:
  "(bw_diff ^^ l) (λx::int. (x + n) gchoose k) =
      (if l ≤ k then (λx. (x + n - int l) gchoose (k - l)) else (λ_. 0))"
proof -
  have *: "l0 ≤ k ⟹ (bw_diff ^^ l0) (λx::int. (x + n) gchoose k) = (λx. (x + n - int l0) gchoose (k - l0))"
    for l0
  proof (induct l0)
    case 0
    show ?case by simp
  next
    case (Suc l0)
    from Suc.prems have "0 < k - l0" and "l0 ≤ k" by simp_all
    from this(2) have eq: "(bw_diff ^^ l0) (λx. x + n gchoose k) = (λx. x + n - int l0 gchoose (k - l0))"
      by (rule Suc.hyps)
    have "(bw_diff ^^ Suc l0) (λx. x + n gchoose k) = bw_diff (λx. x + (n - int l0) gchoose (k - l0))"
      by (simp add: eq algebra_simps)
    also from ‹0 < k - l0› have "… = (λx. (x + (n - int l0) - 1) gchoose (k - l0 - 1))"
      by (rule bw_diff_gbinomial)
    also have "… = (λx. x + n - int (Suc l0) gchoose (k - Suc l0))" by (simp add: algebra_simps)
    finally show ?case .
  qed
  show ?thesis
  proof (simp add: * split: if_split, intro impI)
    assume "¬ l ≤ k"
    hence "(l - k) + k = l" and "l - k ≠ 0" by simp_all
    hence "(bw_diff ^^ l) (λx. x + n gchoose k) = (bw_diff ^^ ((l - k) + k)) (λx. x + n gchoose k)"
      by (simp only:)
    also have "… = (bw_diff ^^ (l - k)) (λ_. 1)" by (simp add: * funpow_add)
    also from ‹l - k ≠ 0› have "… = (λ_. 0)" by (simp add: bw_diff_const_pow)
    finally show "(bw_diff ^^ l) (λx. x + n gchoose k) = (λ_. 0)" .
  qed
qed

end (* theory *)