Quelle Binomial_Plus.thy Sprache: Isabelle

section \<open>More facts about binomial coefficients\<close>

text \<open>
  These facts could have been proven before, but having real numbers
  makes the proofs a lot easier. Thanks to Alexander Maletzky among others.
\<close>

theory Binomial_Plus
imports Real
begin

subsection \<open>More facts about binomial coefficients\<close>

text \<open>
  These facts could have been proven before, but having real numbers
  makes the proofs a lot easier.
\<close>

lemma central_binomial_odd:
  "odd n \ n choose (Suc (n div 2)) = n choose (n div 2)"
proof -
  assume "odd n"
  hence "Suc (n div 2) \ n" by presburger
  hence "n choose (Suc (n div 2)) = n choose (n - Suc (n div 2))"
    by (rule binomial_symmetric)
  also from \<open>odd n\<close> have "n - Suc (n div 2) = n div 2" by presburger
  finally show ?thesis .
qed

lemma binomial_less_binomial_Suc:
  assumes k: "k < n div 2"
  shows   "n choose k < n choose (Suc k)"
proof -
  from k have k': "k \ n" "Suc k \ n" by simp_all
  from k' have "real (n choose k) = fact n / (fact k * fact (n - k))"
    by (simp add: binomial_fact)
  also from k' have "n - k = Suc (n - Suc k)" by simp
  also from k' have "fact \ = (real n - real k) * fact (n - Suc k)"
    by (subst fact_Suc) (simp_all add: of_nat_diff)
  also from k have "fact k = fact (Suc k) / (real k + 1)" by (simp add: field_simps)
  also have "fact n / (fact (Suc k) / (real k + 1) * ((real n - real k) * fact (n - Suc k))) =
               (n choose (Suc k)) * ((real k + 1) / (real n - real k))"
    using k by (simp add: field_split_simps binomial_fact)
  also from assms have "(real k + 1) / (real n - real k) < 1" by simp
  finally show ?thesis using k by (simp add: mult_less_cancel_left)
qed

lemma binomial_strict_mono:
  assumes "k < k'" "2*k' \ n"
  shows   "n choose k < n choose k'"
proof -
  from assms have "k \ k' - 1" by simp
  thus ?thesis
  proof (induction rule: inc_induct)
    case base
    with assms binomial_less_binomial_Suc[of "k' - 1" n]
      show ?case by simp
  next
    case (step k)
    from step.prems step.hyps assms have "n choose k < n choose (Suc k)"
      by (intro binomial_less_binomial_Suc) simp_all
    also have "\ < n choose k'" by (rule step.IH)
    finally show ?case .
  qed
qed

lemma binomial_mono:
  assumes "k \ k'" "2*k' \ n"
  shows   "n choose k \ n choose k'"
  using assms binomial_strict_mono[of k k' n] by (cases "k = k'") simp_all

lemma binomial_strict_antimono:
  assumes "k < k'" "2 * k \ n" "k' \ n"
  shows   "n choose k > n choose k'"
proof -
  from assms have "n choose (n - k) > n choose (n - k')"
    by (intro binomial_strict_mono) (simp_all add: algebra_simps)
  with assms show ?thesis by (simp add: binomial_symmetric [symmetric])
qed

lemma binomial_antimono:
  assumes "k \ k'" "k \ n div 2" "k' \ n"
  shows   "n choose k \ n choose k'"
proof (cases "k = k'")
  case False
  note not_eq = False
  show ?thesis
  proof (cases "k = n div 2 \ odd n")
    case False
    with assms(2) have "2*k \ n" by presburger
    with not_eq assms binomial_strict_antimono[of k k' n]
      show ?thesis by simp
  next
    case True
    have "n choose k' \ n choose (Suc (n div 2))"
    proof (cases "k' = Suc (n div 2)")
      case False
      with assms True not_eq have "Suc (n div 2) < k'" by simp
      with assms binomial_strict_antimono[of "Suc (n div 2)" k' n] True
        show ?thesis by auto
    qed simp_all
    also from True have "\ = n choose k" by (simp add: central_binomial_odd)
    finally show ?thesis .
  qed
qed simp_all

lemma binomial_maximum: "n choose k \ n choose (n div 2)"
proof -
  have "k \ n div 2 \ 2*k \ n" by linarith
  consider "2*k \ n" | "2*k \ n" "k \ n" | "k > n" by linarith
  thus ?thesis
  proof cases
    case 1
    thus ?thesis by (intro binomial_mono) linarith+
  next
    case 2
    thus ?thesis by (intro binomial_antimono) simp_all
  qed (simp_all add: binomial_eq_0)
qed

lemma binomial_maximum': "(2*n) choose k \ (2*n) choose n"
  using binomial_maximum[of "2*n"] by simp

lemma central_binomial_lower_bound:
  assumes "n > 0"
  shows   "4^n / (2*real n) \ real ((2*n) choose n)"
proof -
  from binomial[of 1 1 "2*n"]
    have "4 ^ n = (\k\2*n. (2*n) choose k)"
    by (simp add: power_mult power2_eq_square One_nat_def [symmetric] del: One_nat_def)
  also have "{..2*n} = {0<..<2*n} \ {0,2*n}" by auto
  also have "(\k\\. (2*n) choose k) =
             (\<Sum>k\<in>{0<..<2*n}. (2*n) choose k) + (\<Sum>k\<in>{0,2*n}. (2*n) choose k)"
    by (subst sum.union_disjoint) auto
  also have "(\k\{0,2*n}. (2*n) choose k) \ (\k\1. (n choose k)\<^sup>2)"
    by (cases n) simp_all
  also from assms have "\ \ (\k\n. (n choose k)\<^sup>2)"
    by (intro sum_mono2) auto
  also have "\ = (2*n) choose n" by (rule choose_square_sum)
  also have "(\k\{0<..<2*n}. (2*n) choose k) \ (\k\{0<..<2*n}. (2*n) choose n)"
    by (intro sum_mono binomial_maximum')
  also have "\ = card {0<..<2*n} * ((2*n) choose n)" by simp
  also have "card {0<..<2*n} \ 2*n - 1" by (cases n) simp_all
  also have "(2 * n - 1) * (2 * n choose n) + (2 * n choose n) = ((2*n) choose n) * (2*n)"
    using assms by (simp add: algebra_simps)
  finally have "4 ^ n \ (2 * n choose n) * (2 * n)" by simp_all
  hence "real (4 ^ n) \ real ((2 * n choose n) * (2 * n))"
    by (subst of_nat_le_iff)
  with assms show ?thesis by (simp add: field_simps)
qed

lemma upper_le_binomial:
  assumes "0 < k" and "k < n"
  shows "n \ n choose k"
proof -
  from assms have "1 \ n" by simp
  define k' where "k' = (if n div 2 \<le> k then k else n - k)"
  from assms have 1: "k' \ n - 1" and 2: "n div 2 \ k'" by (auto simp: k'_def)
  from assms(2) have "k \ n" by simp
  have "n choose k = n choose k'" by (simp add: k'_def binomial_symmetric[OF \k \ n\])
  have "n = n choose 1" by (simp only: choose_one)
  also from \<open>1 \<le> n\<close> have "\<dots> = n choose (n - 1)" by (rule binomial_symmetric)
  also from 1 2 have "\ \ n choose k'" by (rule binomial_antimono) simp
  also have "\ = n choose k" by (simp add: k'_def binomial_symmetric[OF \k \ n\])
  finally show ?thesis .
qed

subsection \<open>Results about binomials and integers, thanks to Alexander Maletzky\<close>

text \<open>Restore original sort constraints: semidom rather than field of char 0\<close>
setup \<open>Sign.add_const_constraint (@{const_name gbinomial}, SOME @{typ "'a::{semidom_divide,semiring_char_0} \<Rightarrow> nat \<Rightarrow> 'a"})\<close>

lemma gbinomial_eq_0_int:
  assumes "n < k"
  shows "(int n) gchoose k = 0"
  by (simp add: assms gbinomial_prod_rev prod_zero)

corollary gbinomial_eq_0: "0 \ a \ a < int k \ a gchoose k = 0"
  by (metis nat_eq_iff2 nat_less_iff gbinomial_eq_0_int)

lemma gbinomial_mono:
  fixes k::nat and a::real
  assumes "of_nat k \ a" "a \ b" shows "a gchoose k \ b gchoose k"
  using assms
  by (force simp: gbinomial_prod_rev intro!: divide_right_mono prod_mono)

lemma int_binomial: "int (n choose k) = (int n) gchoose k"
proof (cases "k \ n")
  case True
  from refl have eq: "(\i = 0..i = 0..
  proof (rule prod.cong)
    fix i
    assume "i \ {0..
    with True show "int (n - i) = int n - int i" by simp
  qed
  show ?thesis
    by (simp add: gbinomial_binomial[symmetric] gbinomial_prod_rev zdiv_int eq)
next
  case False
  thus ?thesis by (simp add: gbinomial_eq_0_int)
qed

lemma falling_fact_pochhammer: "prod (\i. a - int i) {0..
proof -
  have eq: "z ^ Suc n * prod f {0..n} = prod (\x. z * f x) {0..n}" for z::int and n f
    by (induct n) (simp_all add: ac_simps)
  show ?thesis
  proof (cases k)
    case 0
    thus ?thesis by (simp add: pochhammer_minus)
  next
    case (Suc n)
    thus ?thesis
      by (simp only: pochhammer_prod atLeastLessThanSuc_atLeastAtMost
          prod.atLeast_Suc_atMost_Suc_shift eq flip: power_mult_distrib) (simp add: of_nat_diff)
  qed
qed

lemma falling_fact_pochhammer': "prod (\i. a - int i) {0..
  by (simp add: falling_fact_pochhammer pochhammer_minus')

lemma gbinomial_int_pochhammer: "(a::int) gchoose k = (- 1) ^ k * pochhammer (- a) k div fact k"
  by (simp only: gbinomial_prod_rev falling_fact_pochhammer)

lemma gbinomial_int_pochhammer': "a gchoose k = pochhammer (a - int k + 1) k div fact k"
  by (simp only: gbinomial_prod_rev falling_fact_pochhammer')

lemma fact_dvd_pochhammer: "fact k dvd pochhammer (a::int) k"
proof -
  have dvd: "y \ 0 \ ((of_int (x div y))::'a::field_char_0) = of_int x / of_int y \ y dvd x"
    for x y :: int
    by (metis dvd_triv_right nonzero_eq_divide_eq of_int_0_eq_iff of_int_eq_iff of_int_mult)
  show ?thesis
  proof (cases "0 < a")
    case True
    moreover define n where "n = nat (a - 1) + k"
    ultimately have a: "a = int n - int k + 1" by simp
    from fact_nonzero show ?thesis unfolding a
    proof (rule dvd)
      have "of_int (pochhammer (int n - int k + 1) k div fact k) = (of_int (int n gchoose k)::rat)"
        by (simp only: gbinomial_int_pochhammer')
      also have "\ = of_nat (n choose k)"
        by (metis int_binomial of_int_of_nat_eq)
      also have "\ = (of_nat n) gchoose k" by (fact binomial_gbinomial)
      also have "\ = pochhammer (of_nat n - of_nat k + 1) k / fact k"
        by (fact gbinomial_pochhammer')
      also have "\ = pochhammer (of_int (int n - int k + 1)) k / fact k" by simp
      also have "\ = (of_int (pochhammer (int n - int k + 1) k)) / (of_int (fact k))"
        by (simp only: of_int_fact pochhammer_of_int)
      finally show "of_int (pochhammer (int n - int k + 1) k div fact k) =
                      of_int (pochhammer (int n - int k + 1) k) / rat_of_int (fact k)" .
    qed
  next
    case False
    moreover define n where "n = nat (- a)"
    ultimately have a: "a = - int n" by simp
    from fact_nonzero have "fact k dvd (-1)^k * pochhammer (- int n) k"
    proof (rule dvd)
      have "of_int ((-1)^k * pochhammer (- int n) k div fact k) = (of_int (int n gchoose k)::rat)"
        by (metis falling_fact_pochhammer gbinomial_prod_rev)
      also have "\ = of_int (int (n choose k))" by (simp only: int_binomial)
      also have "\ = of_nat (n choose k)" by simp
      also have "\ = (of_nat n) gchoose k" by (fact binomial_gbinomial)
      also have "\ = (-1)^k * pochhammer (- of_nat n) k / fact k"
        by (fact gbinomial_pochhammer)
      also have "\ = (-1)^k * pochhammer (of_int (- int n)) k / fact k" by simp
      also have "\ = (-1)^k * (of_int (pochhammer (- int n) k)) / (of_int (fact k))"
        by (simp only: of_int_fact pochhammer_of_int)
      also have "\ = (of_int ((-1)^k * pochhammer (- int n) k)) / (of_int (fact k))" by simp
      finally show "of_int ((- 1) ^ k * pochhammer (- int n) k div fact k) =
                    of_int ((- 1) ^ k * pochhammer (- int n) k) / rat_of_int (fact k)" .
    qed
    thus ?thesis unfolding a by (metis dvdI dvd_mult_unit_iff' minus_one_mult_self)
  qed
qed

lemma gbinomial_int_negated_upper: "(a gchoose k) = (-1) ^ k * ((int k - a - 1) gchoose k)"
  by (simp add: gbinomial_int_pochhammer pochhammer_minus algebra_simps fact_dvd_pochhammer div_mult_swap)

lemma gbinomial_int_mult_fact: "fact k * (a gchoose k) = (\i = 0..
  by (simp only: gbinomial_int_pochhammer' fact_dvd_pochhammer dvd_mult_div_cancel falling_fact_pochhammer')

corollary gbinomial_int_mult_fact': "(a gchoose k) * fact k = (\i = 0..
  using gbinomial_int_mult_fact[of k a] by (simp add: ac_simps)

lemma gbinomial_int_binomial:
  "a gchoose k = (if 0 \ a then int ((nat a) choose k) else (-1::int)^k * int ((k + (nat (- a)) - 1) choose k))"
  by (auto simp: int_binomial gbinomial_int_negated_upper[of a] int_ops(6))

corollary gbinomial_nneg: "0 \ a \ a gchoose k = int ((nat a) choose k)"
  by (simp add: gbinomial_int_binomial)

corollary gbinomial_neg: "a < 0 \ a gchoose k = (-1::int)^k * int ((k + (nat (- a)) - 1) choose k)"
  by (simp add: gbinomial_int_binomial)

lemma of_int_gbinomial: "of_int (a gchoose k) = (of_int a :: 'a::field_char_0) gchoose k"
proof -
  have of_int_div: "y dvd x \ of_int (x div y) = of_int x / (of_int y :: 'a)" for x y :: int by auto
  show ?thesis
    by (simp add: gbinomial_int_pochhammer' gbinomial_pochhammer' of_int_div fact_dvd_pochhammer
        pochhammer_of_int[symmetric])
qed

lemma uminus_one_gbinomial [simp]: "(- 1::int) gchoose k = (- 1) ^ k"
  by (simp add: gbinomial_int_binomial)

lemma gbinomial_int_Suc_Suc: "(x + 1::int) gchoose (Suc k) = (x gchoose k) + (x gchoose (Suc k))"
proof (rule linorder_cases)
  assume 1: "x + 1 < 0"
  hence 2: "x < 0" by simp
  then obtain n where 3: "nat (- x) = Suc n" using not0_implies_Suc by fastforce
  hence 4: "nat (- x - 1) = n" by simp
  show ?thesis
  proof (cases k)
    case 0
    show ?thesis by (simp add: \<open>k = 0\<close>)
  next
    case (Suc k')
    from 1 2 3 4 show ?thesis by (simp add: \<open>k = Suc k'\<close> gbinomial_int_binomial int_distrib(2))
  qed
next
  assume "x + 1 = 0"
  hence "x = - 1" by simp
  thus ?thesis by simp
next
  assume "0 < x + 1"
  hence "0 \ x + 1" and "0 \ x" and "nat (x + 1) = Suc (nat x)" by simp_all
  thus ?thesis by (simp add: gbinomial_int_binomial)
qed

corollary plus_Suc_gbinomial:
  "(x + (1 + int k)) gchoose (Suc k) = ((x + int k) gchoose k) + ((x + int k) gchoose (Suc k))"
    (is "?l = ?r")
proof -
  have "?l = (x + int k + 1) gchoose (Suc k)" by (simp only: ac_simps)
  also have "\ = ?r" by (fact gbinomial_int_Suc_Suc)
  finally show ?thesis .
qed

lemma gbinomial_int_n_n [simp]: "(int n) gchoose n = 1"
proof (induct n)
  case 0
  show ?case by simp
next
  case (Suc n)
  have "int (Suc n) gchoose Suc n = (int n + 1) gchoose Suc n" by (simp add: add.commute)
  also have "\ = (int n gchoose n) + (int n gchoose (Suc n))" by (fact gbinomial_int_Suc_Suc)
  finally show ?case by (simp add: Suc gbinomial_eq_0)
qed

lemma gbinomial_int_Suc_n [simp]: "(1 + int n) gchoose n = 1 + int n"
proof (induct n)
  case 0
  show ?case by simp
next
  case (Suc n)
  have "1 + int (Suc n) gchoose Suc n = (1 + int n) + 1 gchoose Suc n" by simp
  also have "\ = (1 + int n gchoose n) + (1 + int n gchoose (Suc n))" by (fact gbinomial_int_Suc_Suc)
  also have "\ = 1 + int n + (int (Suc n) gchoose (Suc n))" by (simp add: Suc)
  also have "\ = 1 + int (Suc n)" by (simp only: gbinomial_int_n_n)
  finally show ?case .
qed

lemma zbinomial_eq_0_iff [simp]: "a gchoose k = 0 \ (0 \ a \ a < int k)"
proof
  assume a: "a gchoose k = 0"
  have 1: "b < int k" if "b gchoose k = 0" for b
  proof (rule ccontr)
    assume "\ b < int k"
    hence "0 \ b" and "k \ nat b" by simp_all
    from this(1) have "int ((nat b) choose k) = b gchoose k" by (simp add: gbinomial_int_binomial)
    also have "\ = 0" by (fact that)
    finally show False using \<open>k \<le> nat b\<close> by simp
  qed
  show "0 \ a \ a < int k"
  proof
    show "0 \ a"
    proof (rule ccontr)
      assume "\ 0 \ a"
      hence "(-1) ^ k * ((int k - a - 1) gchoose k) = a gchoose k"
        by (simp add: gbinomial_int_negated_upper[of a])
      also have "\ = 0" by (fact a)
      finally have "(int k - a - 1) gchoose k = 0" by simp
      hence "int k - a - 1 < int k" by (rule 1)
      with \<open>\<not> 0 \<le> a\<close> show False by simp
    qed
  next
    from a show "a < int k" by (rule 1)
  qed
qed (auto intro: gbinomial_eq_0)

subsection \<open>Sums\<close>

lemma gchoose_rising_sum_nat: "(\j\n. int j + int k gchoose k) = (int n + int k + 1) gchoose (Suc k)"
proof -
  have "(\j\n. int j + int k gchoose k) = int (\j\n. k + j choose k)"
    by (simp add: int_binomial add.commute)
  also have "(\j\n. k + j choose k) = (k + n + 1) choose (k + 1)" by (fact choose_rising_sum(1))
  also have "int \ = (int n + int k + 1) gchoose (Suc k)"
    by (simp add: int_binomial ac_simps del: binomial_Suc_Suc)
  finally show ?thesis .
qed

lemma gchoose_rising_sum:
  assumes "0 \ n" \\Necessary condition.\
  shows "(\j=0..n. j + int k gchoose k) = (n + int k + 1) gchoose (Suc k)"
proof -
  from _ refl have "(\j=0..n. j + int k gchoose k) = (\j\int ` {0..nat n}. j + int k gchoose k)"
  proof (rule sum.cong)
    from assms show "{0..n} = int ` {0..nat n}" by (simp add: image_int_atLeastAtMost)
  qed
  also have "\ = (\j\nat n. int j + int k gchoose k)" by (simp add: sum.reindex atMost_atLeast0)
  also have "\ = (int (nat n) + int k + 1) gchoose (Suc k)" by (fact gchoose_rising_sum_nat)
  also from assms have "\ = (n + int k + 1) gchoose (Suc k)" by (simp add: add.assoc add.commute)
  finally show ?thesis .
qed

end

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.