Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
authoreberlm
Mon Nov 02 16:17:09 2015 +0100 (2015-11-02)
changeset 61552980dd46a03fb
parent 61532 e3984606b4b6
child 61553 933eb9e6a1cc
Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer
CONTRIBUTORS
src/HOL/Binomial.thy
src/HOL/Complex.thy
src/HOL/Deriv.thy
src/HOL/Int.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Uniform_Limit.thy
src/HOL/Transcendental.thy
     1.1 --- a/CONTRIBUTORS	Mon Nov 02 11:56:38 2015 +0100
     1.2 +++ b/CONTRIBUTORS	Mon Nov 02 16:17:09 2015 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl
     1.8 +  A large number of additional binomial identities.
     1.9 +
    1.10  * Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel
    1.11    Isar subgoal command for proof structure within unstructured proof
    1.12    scripts.
     2.1 --- a/src/HOL/Binomial.thy	Mon Nov 02 11:56:38 2015 +0100
     2.2 +++ b/src/HOL/Binomial.thy	Mon Nov 02 16:17:09 2015 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4  
     2.5  subsection \<open>Factorial\<close>
     2.6  
     2.7 -fun fact :: "nat \<Rightarrow> ('a::semiring_char_0)"
     2.8 +fun (in semiring_char_0) fact :: "nat \<Rightarrow> 'a"
     2.9    where "fact 0 = 1" | "fact (Suc n) = of_nat (Suc n) * fact n"
    2.10  
    2.11  lemmas fact_Suc = fact.simps(2)
    2.12 @@ -442,7 +442,7 @@
    2.13  
    2.14  text \<open>See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\<close>
    2.15  
    2.16 -definition "pochhammer (a::'a::comm_semiring_1) n =
    2.17 +definition (in comm_semiring_1) "pochhammer (a :: 'a) n =
    2.18    (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
    2.19  
    2.20  lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
    2.21 @@ -621,6 +621,40 @@
    2.22    "m \<le> n \<Longrightarrow> pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n - m)"
    2.23    using pochhammer_product'[of z m "n - m"] by simp
    2.24  
    2.25 +lemma pochhammer_times_pochhammer_half:
    2.26 +  fixes z :: "'a :: field_char_0"
    2.27 +  shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\<Prod>k=0..2*n+1. z + of_nat k / 2)"
    2.28 +proof (induction n)
    2.29 +  case (Suc n)
    2.30 +  def n' \<equiv> "Suc n"
    2.31 +  have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') =
    2.32 +          (pochhammer z n' * pochhammer (z + 1 / 2) n') * 
    2.33 +          ((z + of_nat n') * (z + 1/2 + of_nat n'))" (is "_ = _ * ?A")
    2.34 +     by (simp_all add: pochhammer_rec' mult_ac)
    2.35 +  also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)"
    2.36 +    (is "_ = ?A") by (simp add: field_simps n'_def of_nat_mult)
    2.37 +  also note Suc[folded n'_def]
    2.38 +  also have "(\<Prod>k = 0..2 * n + 1. z + of_nat k / 2) * ?A = (\<Prod>k = 0..2 * Suc n + 1. z + of_nat k / 2)"
    2.39 +    by (simp add: setprod_nat_ivl_Suc)
    2.40 +  finally show ?case by (simp add: n'_def)
    2.41 +qed (simp add: setprod_nat_ivl_Suc)
    2.42 +
    2.43 +lemma pochhammer_double:
    2.44 +  fixes z :: "'a :: field_char_0"
    2.45 +  shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n"
    2.46 +proof (induction n)
    2.47 +  case (Suc n)
    2.48 +  have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) * 
    2.49 +          (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)"
    2.50 +    by (simp add: pochhammer_rec' ac_simps of_nat_mult)
    2.51 +  also note Suc
    2.52 +  also have "of_nat (2 ^ (2 * n)) * pochhammer z n * pochhammer (z + 1/2) n *
    2.53 +                 (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) =
    2.54 +             of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)"
    2.55 +    by (simp add: of_nat_mult field_simps pochhammer_rec')
    2.56 +  finally show ?case .
    2.57 +qed simp
    2.58 +
    2.59  lemma pochhammer_absorb_comp:
    2.60    "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k" 
    2.61    (is "?lhs = ?rhs")
    2.62 @@ -633,7 +667,7 @@
    2.63  
    2.64  subsection\<open>Generalized binomial coefficients\<close>
    2.65  
    2.66 -definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
    2.67 +definition (in field_char_0) gbinomial :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
    2.68    where "a gchoose n =
    2.69      (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / (fact n))"
    2.70  
    2.71 @@ -654,6 +688,15 @@
    2.72        eq setprod.distrib[symmetric])
    2.73  qed
    2.74  
    2.75 +lemma gbinomial_pochhammer':
    2.76 +  "(s :: 'a :: field_char_0) gchoose n = pochhammer (s - of_nat n + 1) n / fact n"
    2.77 +proof -
    2.78 +  have "s gchoose n = ((-1)^n * (-1)^n) * pochhammer (s - of_nat n + 1) n / fact n"
    2.79 +    by (simp add: gbinomial_pochhammer pochhammer_minus mult_ac)
    2.80 +  also have "(-1 :: 'a)^n * (-1)^n = 1" by (subst power_add [symmetric]) simp
    2.81 +  finally show ?thesis by simp
    2.82 +qed
    2.83 +
    2.84  lemma binomial_gbinomial: 
    2.85      "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)"
    2.86  proof -
     3.1 --- a/src/HOL/Complex.thy	Mon Nov 02 11:56:38 2015 +0100
     3.2 +++ b/src/HOL/Complex.thy	Mon Nov 02 16:17:09 2015 +0100
     3.3 @@ -166,6 +166,12 @@
     3.4  
     3.5  lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
     3.6    by (simp add: Im_divide sqr_conv_mult)
     3.7 +  
     3.8 +lemma Re_divide_of_nat: "Re (z / of_nat n) = Re z / of_nat n"
     3.9 +  by (cases n) (simp_all add: Re_divide divide_simps power2_eq_square del: of_nat_Suc)
    3.10 +
    3.11 +lemma Im_divide_of_nat: "Im (z / of_nat n) = Im z / of_nat n"
    3.12 +  by (cases n) (simp_all add: Im_divide divide_simps power2_eq_square del: of_nat_Suc)
    3.13  
    3.14  lemma of_real_Re [simp]:
    3.15      "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
     4.1 --- a/src/HOL/Deriv.thy	Mon Nov 02 11:56:38 2015 +0100
     4.2 +++ b/src/HOL/Deriv.thy	Mon Nov 02 16:17:09 2015 +0100
     4.3 @@ -745,7 +745,7 @@
     4.4    by (rule DERIV_continuous)
     4.5  
     4.6  lemma DERIV_continuous_on:
     4.7 -  "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative D) (at x)) \<Longrightarrow> continuous_on s f"
     4.8 +  "(\<And>x. x \<in> s \<Longrightarrow> (f has_field_derivative (D x)) (at x)) \<Longrightarrow> continuous_on s f"
     4.9    by (metis DERIV_continuous continuous_at_imp_continuous_on)
    4.10  
    4.11  lemma DERIV_mult':
     5.1 --- a/src/HOL/Int.thy	Mon Nov 02 11:56:38 2015 +0100
     5.2 +++ b/src/HOL/Int.thy	Mon Nov 02 16:17:09 2015 +0100
     5.3 @@ -686,6 +686,9 @@
     5.4  lemma Ints_1 [simp]: "1 \<in> \<int>"
     5.5    using Ints_of_int [of "1"] by simp
     5.6  
     5.7 +lemma Ints_numeral [simp]: "numeral n \<in> \<int>"
     5.8 +  by (subst of_nat_numeral [symmetric], rule Ints_of_nat)
     5.9 +
    5.10  lemma Ints_add [simp]: "a \<in> \<int> \<Longrightarrow> b \<in> \<int> \<Longrightarrow> a + b \<in> \<int>"
    5.11  apply (auto simp add: Ints_def)
    5.12  apply (rule range_eqI)
     6.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Mon Nov 02 11:56:38 2015 +0100
     6.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Nov 02 16:17:09 2015 +0100
     6.3 @@ -3115,7 +3115,7 @@
     6.4    then show ?thesis by simp
     6.5  qed
     6.6  
     6.7 -lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
     6.8 +lemma fps_binomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)"
     6.9    (is "?l = inverse ?r")
    6.10  proof-
    6.11    have th: "?r$0 \<noteq> 0" by simp
     7.1 --- a/src/HOL/Limits.thy	Mon Nov 02 11:56:38 2015 +0100
     7.2 +++ b/src/HOL/Limits.thy	Mon Nov 02 16:17:09 2015 +0100
     7.3 @@ -1148,6 +1148,32 @@
     7.4    qed
     7.5  qed
     7.6  
     7.7 +lemma tendsto_add_filterlim_at_infinity:
     7.8 +  assumes "(f ---> (c :: 'b :: real_normed_vector)) (F :: 'a filter)"
     7.9 +  assumes "filterlim g at_infinity F"
    7.10 +  shows   "filterlim (\<lambda>x. f x + g x) at_infinity F"
    7.11 +proof (subst filterlim_at_infinity[OF order_refl], safe)
    7.12 +  fix r :: real assume r: "r > 0"
    7.13 +  from assms(1) have "((\<lambda>x. norm (f x)) ---> norm c) F" by (rule tendsto_norm)
    7.14 +  hence "eventually (\<lambda>x. norm (f x) < norm c + 1) F" by (rule order_tendstoD) simp_all
    7.15 +  moreover from r have "r + norm c + 1 > 0" by (intro add_pos_nonneg) simp_all 
    7.16 +  with assms(2) have "eventually (\<lambda>x. norm (g x) \<ge> r + norm c + 1) F"
    7.17 +    unfolding filterlim_at_infinity[OF order_refl] by (elim allE[of _ "r + norm c + 1"]) simp_all
    7.18 +  ultimately show "eventually (\<lambda>x. norm (f x + g x) \<ge> r) F"
    7.19 +  proof eventually_elim
    7.20 +    fix x :: 'a assume A: "norm (f x) < norm c + 1" and B: "r + norm c + 1 \<le> norm (g x)"
    7.21 +    from A B have "r \<le> norm (g x) - norm (f x)" by simp
    7.22 +    also have "norm (g x) - norm (f x) \<le> norm (g x + f x)" by (rule norm_diff_ineq)
    7.23 +    finally show "r \<le> norm (f x + g x)" by (simp add: add_ac)
    7.24 +  qed
    7.25 +qed
    7.26 +
    7.27 +lemma tendsto_add_filterlim_at_infinity':
    7.28 +  assumes "filterlim f at_infinity F"
    7.29 +  assumes "(g ---> (c :: 'b :: real_normed_vector)) (F :: 'a filter)"
    7.30 +  shows   "filterlim (\<lambda>x. f x + g x) at_infinity F"
    7.31 +  by (subst add.commute) (rule tendsto_add_filterlim_at_infinity assms)+
    7.32 +
    7.33  lemma filterlim_inverse_at_right_top: "LIM x at_top. inverse x :> at_right (0::real)"
    7.34    unfolding filterlim_at
    7.35    by (auto simp: eventually_at_top_dense)
     8.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Nov 02 11:56:38 2015 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Nov 02 16:17:09 2015 +0100
     8.3 @@ -3164,6 +3164,9 @@
     8.4    unfolding bounded_any_center [where a=0]
     8.5    by (simp add: dist_norm)
     8.6  
     8.7 +lemma bdd_above_norm: "bdd_above (norm ` X) \<longleftrightarrow> bounded X"
     8.8 +  by (simp add: bounded_iff bdd_above_def)
     8.9 +
    8.10  lemma bounded_realI:
    8.11    assumes "\<forall>x\<in>s. abs (x::real) \<le> B"
    8.12    shows "bounded s"
     9.1 --- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Mon Nov 02 11:56:38 2015 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Mon Nov 02 16:17:09 2015 +0100
     9.3 @@ -479,4 +479,22 @@
     9.4    "uniform_limit J f g F \<Longrightarrow> I \<subseteq> J \<Longrightarrow> uniform_limit I f g F"
     9.5    by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_rev_mono)
     9.6  
     9.7 +
     9.8 +
     9.9 +lemma uniformly_convergent_add:
    9.10 +  "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
    9.11 +      uniformly_convergent_on A (\<lambda>k x. f k x + g k x :: 'a :: {real_normed_algebra})"
    9.12 +  unfolding uniformly_convergent_on_def by (blast dest: uniform_limit_add)
    9.13 +
    9.14 +lemma uniformly_convergent_minus:
    9.15 +  "uniformly_convergent_on A f \<Longrightarrow> uniformly_convergent_on A g\<Longrightarrow>
    9.16 +      uniformly_convergent_on A (\<lambda>k x. f k x - g k x :: 'a :: {real_normed_algebra})"
    9.17 +  unfolding uniformly_convergent_on_def by (blast dest: uniform_limit_minus)
    9.18 +
    9.19 +lemma uniformly_convergent_mult:
    9.20 +  "uniformly_convergent_on A f \<Longrightarrow> 
    9.21 +      uniformly_convergent_on A (\<lambda>k x. c * f k x :: 'a :: {real_normed_algebra})"
    9.22 +  unfolding uniformly_convergent_on_def
    9.23 +  by (blast dest: bounded_linear_uniform_limit_intros(13))
    9.24 +
    9.25  end
    9.26 \ No newline at end of file
    10.1 --- a/src/HOL/Transcendental.thy	Mon Nov 02 11:56:38 2015 +0100
    10.2 +++ b/src/HOL/Transcendental.thy	Mon Nov 02 16:17:09 2015 +0100
    10.3 @@ -792,6 +792,29 @@
    10.4      done
    10.5  qed
    10.6  
    10.7 +lemma termdiffs_strong_converges_everywhere:
    10.8 +    fixes K x :: "'a::{real_normed_field,banach}"
    10.9 +  assumes "\<And>y. summable (\<lambda>n. c n * y ^ n)"
   10.10 +  shows   "((\<lambda>x. \<Sum>n. c n * x^n) has_field_derivative (\<Sum>n. diffs c n * x^n)) (at x)"
   10.11 +  using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
   10.12 +  by (force simp del: of_real_add)
   10.13 +  
   10.14 +lemma isCont_powser:
   10.15 +  fixes K x :: "'a::{real_normed_field,banach}"
   10.16 +  assumes "summable (\<lambda>n. c n * K ^ n)"
   10.17 +  assumes "norm x < norm K"
   10.18 +  shows   "isCont (\<lambda>x. \<Sum>n. c n * x^n) x"
   10.19 +  using termdiffs_strong[OF assms] by (blast intro!: DERIV_isCont)
   10.20 +  
   10.21 +lemmas isCont_powser' = isCont_o2[OF _ isCont_powser]
   10.22 +
   10.23 +lemma isCont_powser_converges_everywhere:
   10.24 +  fixes K x :: "'a::{real_normed_field,banach}"
   10.25 +  assumes "\<And>y. summable (\<lambda>n. c n * y ^ n)"
   10.26 +  shows   "isCont (\<lambda>x. \<Sum>n. c n * x^n) x"
   10.27 +  using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
   10.28 +  by (force intro!: DERIV_isCont simp del: of_real_add)
   10.29 +
   10.30  lemma powser_limit_0: 
   10.31    fixes a :: "nat \<Rightarrow> 'a::{real_normed_field,banach}"
   10.32    assumes s: "0 < s"