# HG changeset patch # User eberlm # Date 1446477429 -3600 # Node ID 980dd46a03fb538ff9d0846fed3e0ac2e5a9498d # Parent e3984606b4b6f20ffa074005157f5879699528f4 Added binomial identities to CONTRIBUTORS; small lemmas on of_int/pochhammer diff -r e3984606b4b6 -r 980dd46a03fb CONTRIBUTORS --- a/CONTRIBUTORS Mon Nov 02 11:56:38 2015 +0100 +++ b/CONTRIBUTORS Mon Nov 02 16:17:09 2015 +0100 @@ -6,6 +6,9 @@ Contributions to this Isabelle version -------------------------------------- +* Autumn 2015: Chaitanya Mangla, Lawrence C Paulson, and Manuel Eberl + A large number of additional binomial identities. + * Summer 2015: Daniel Matichuk, NICTA and Makarius Wenzel Isar subgoal command for proof structure within unstructured proof scripts. diff -r e3984606b4b6 -r 980dd46a03fb src/HOL/Binomial.thy --- a/src/HOL/Binomial.thy Mon Nov 02 11:56:38 2015 +0100 +++ b/src/HOL/Binomial.thy Mon Nov 02 16:17:09 2015 +0100 @@ -13,7 +13,7 @@ subsection \Factorial\ -fun fact :: "nat \ ('a::semiring_char_0)" +fun (in semiring_char_0) fact :: "nat \ 'a" where "fact 0 = 1" | "fact (Suc n) = of_nat (Suc n) * fact n" lemmas fact_Suc = fact.simps(2) @@ -442,7 +442,7 @@ text \See @{url "http://en.wikipedia.org/wiki/Pochhammer_symbol"}\ -definition "pochhammer (a::'a::comm_semiring_1) n = +definition (in comm_semiring_1) "pochhammer (a :: 'a) n = (if n = 0 then 1 else setprod (\n. a + of_nat n) {0 .. n - 1})" lemma pochhammer_0 [simp]: "pochhammer a 0 = 1" @@ -621,6 +621,40 @@ "m \ n \ pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n - m)" using pochhammer_product'[of z m "n - m"] by simp +lemma pochhammer_times_pochhammer_half: + fixes z :: "'a :: field_char_0" + shows "pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n) = (\k=0..2*n+1. z + of_nat k / 2)" +proof (induction n) + case (Suc n) + def n' \ "Suc n" + have "pochhammer z (Suc n') * pochhammer (z + 1 / 2) (Suc n') = + (pochhammer z n' * pochhammer (z + 1 / 2) n') * + ((z + of_nat n') * (z + 1/2 + of_nat n'))" (is "_ = _ * ?A") + by (simp_all add: pochhammer_rec' mult_ac) + also have "?A = (z + of_nat (Suc (2 * n + 1)) / 2) * (z + of_nat (Suc (Suc (2 * n + 1))) / 2)" + (is "_ = ?A") by (simp add: field_simps n'_def of_nat_mult) + also note Suc[folded n'_def] + also have "(\k = 0..2 * n + 1. z + of_nat k / 2) * ?A = (\k = 0..2 * Suc n + 1. z + of_nat k / 2)" + by (simp add: setprod_nat_ivl_Suc) + finally show ?case by (simp add: n'_def) +qed (simp add: setprod_nat_ivl_Suc) + +lemma pochhammer_double: + fixes z :: "'a :: field_char_0" + shows "pochhammer (2 * z) (2 * n) = of_nat (2^(2*n)) * pochhammer z n * pochhammer (z+1/2) n" +proof (induction n) + case (Suc n) + have "pochhammer (2 * z) (2 * (Suc n)) = pochhammer (2 * z) (2 * n) * + (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1)" + by (simp add: pochhammer_rec' ac_simps of_nat_mult) + also note Suc + also have "of_nat (2 ^ (2 * n)) * pochhammer z n * pochhammer (z + 1/2) n * + (2 * (z + of_nat n)) * (2 * (z + of_nat n) + 1) = + of_nat (2 ^ (2 * (Suc n))) * pochhammer z (Suc n) * pochhammer (z + 1/2) (Suc n)" + by (simp add: of_nat_mult field_simps pochhammer_rec') + finally show ?case . +qed simp + lemma pochhammer_absorb_comp: "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k" (is "?lhs = ?rhs") @@ -633,7 +667,7 @@ subsection\Generalized binomial coefficients\ -definition gbinomial :: "'a::field_char_0 \ nat \ 'a" (infixl "gchoose" 65) +definition (in field_char_0) gbinomial :: "'a \ nat \ 'a" (infixl "gchoose" 65) where "a gchoose n = (if n = 0 then 1 else (setprod (\i. a - of_nat i) {0 .. n - 1}) / (fact n))" @@ -654,6 +688,15 @@ eq setprod.distrib[symmetric]) qed +lemma gbinomial_pochhammer': + "(s :: 'a :: field_char_0) gchoose n = pochhammer (s - of_nat n + 1) n / fact n" +proof - + have "s gchoose n = ((-1)^n * (-1)^n) * pochhammer (s - of_nat n + 1) n / fact n" + by (simp add: gbinomial_pochhammer pochhammer_minus mult_ac) + also have "(-1 :: 'a)^n * (-1)^n = 1" by (subst power_add [symmetric]) simp + finally show ?thesis by simp +qed + lemma binomial_gbinomial: "of_nat (n choose k) = (of_nat n gchoose k :: 'a::field_char_0)" proof - diff -r e3984606b4b6 -r 980dd46a03fb src/HOL/Complex.thy --- a/src/HOL/Complex.thy Mon Nov 02 11:56:38 2015 +0100 +++ b/src/HOL/Complex.thy Mon Nov 02 16:17:09 2015 +0100 @@ -166,6 +166,12 @@ lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w" by (simp add: Im_divide sqr_conv_mult) + +lemma Re_divide_of_nat: "Re (z / of_nat n) = Re z / of_nat n" + by (cases n) (simp_all add: Re_divide divide_simps power2_eq_square del: of_nat_Suc) + +lemma Im_divide_of_nat: "Im (z / of_nat n) = Im z / of_nat n" + by (cases n) (simp_all add: Im_divide divide_simps power2_eq_square del: of_nat_Suc) lemma of_real_Re [simp]: "z \ \ \ of_real (Re z) = z" diff -r e3984606b4b6 -r 980dd46a03fb src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Mon Nov 02 11:56:38 2015 +0100 +++ b/src/HOL/Deriv.thy Mon Nov 02 16:17:09 2015 +0100 @@ -745,7 +745,7 @@ by (rule DERIV_continuous) lemma DERIV_continuous_on: - "(\x. x \ s \ (f has_field_derivative D) (at x)) \ continuous_on s f" + "(\x. x \ s \ (f has_field_derivative (D x)) (at x)) \ continuous_on s f" by (metis DERIV_continuous continuous_at_imp_continuous_on) lemma DERIV_mult': diff -r e3984606b4b6 -r 980dd46a03fb src/HOL/Int.thy --- a/src/HOL/Int.thy Mon Nov 02 11:56:38 2015 +0100 +++ b/src/HOL/Int.thy Mon Nov 02 16:17:09 2015 +0100 @@ -686,6 +686,9 @@ lemma Ints_1 [simp]: "1 \ \" using Ints_of_int [of "1"] by simp +lemma Ints_numeral [simp]: "numeral n \ \" + by (subst of_nat_numeral [symmetric], rule Ints_of_nat) + lemma Ints_add [simp]: "a \ \ \ b \ \ \ a + b \ \" apply (auto simp add: Ints_def) apply (rule range_eqI) diff -r e3984606b4b6 -r 980dd46a03fb src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Mon Nov 02 11:56:38 2015 +0100 +++ b/src/HOL/Library/Formal_Power_Series.thy Mon Nov 02 16:17:09 2015 +0100 @@ -3115,7 +3115,7 @@ then show ?thesis by simp qed -lemma fps_minomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)" +lemma fps_binomial_minus_one: "fps_binomial (- 1) = inverse (1 + X)" (is "?l = inverse ?r") proof- have th: "?r$0 \ 0" by simp diff -r e3984606b4b6 -r 980dd46a03fb src/HOL/Limits.thy --- a/src/HOL/Limits.thy Mon Nov 02 11:56:38 2015 +0100 +++ b/src/HOL/Limits.thy Mon Nov 02 16:17:09 2015 +0100 @@ -1148,6 +1148,32 @@ qed qed +lemma tendsto_add_filterlim_at_infinity: + assumes "(f ---> (c :: 'b :: real_normed_vector)) (F :: 'a filter)" + assumes "filterlim g at_infinity F" + shows "filterlim (\x. f x + g x) at_infinity F" +proof (subst filterlim_at_infinity[OF order_refl], safe) + fix r :: real assume r: "r > 0" + from assms(1) have "((\x. norm (f x)) ---> norm c) F" by (rule tendsto_norm) + hence "eventually (\x. norm (f x) < norm c + 1) F" by (rule order_tendstoD) simp_all + moreover from r have "r + norm c + 1 > 0" by (intro add_pos_nonneg) simp_all + with assms(2) have "eventually (\x. norm (g x) \ r + norm c + 1) F" + unfolding filterlim_at_infinity[OF order_refl] by (elim allE[of _ "r + norm c + 1"]) simp_all + ultimately show "eventually (\x. norm (f x + g x) \ r) F" + proof eventually_elim + fix x :: 'a assume A: "norm (f x) < norm c + 1" and B: "r + norm c + 1 \ norm (g x)" + from A B have "r \ norm (g x) - norm (f x)" by simp + also have "norm (g x) - norm (f x) \ norm (g x + f x)" by (rule norm_diff_ineq) + finally show "r \ norm (f x + g x)" by (simp add: add_ac) + qed +qed + +lemma tendsto_add_filterlim_at_infinity': + assumes "filterlim f at_infinity F" + assumes "(g ---> (c :: 'b :: real_normed_vector)) (F :: 'a filter)" + shows "filterlim (\x. f x + g x) at_infinity F" + by (subst add.commute) (rule tendsto_add_filterlim_at_infinity assms)+ + lemma filterlim_inverse_at_right_top: "LIM x at_top. inverse x :> at_right (0::real)" unfolding filterlim_at by (auto simp: eventually_at_top_dense) diff -r e3984606b4b6 -r 980dd46a03fb src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Nov 02 11:56:38 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Nov 02 16:17:09 2015 +0100 @@ -3164,6 +3164,9 @@ unfolding bounded_any_center [where a=0] by (simp add: dist_norm) +lemma bdd_above_norm: "bdd_above (norm ` X) \ bounded X" + by (simp add: bounded_iff bdd_above_def) + lemma bounded_realI: assumes "\x\s. abs (x::real) \ B" shows "bounded s" diff -r e3984606b4b6 -r 980dd46a03fb src/HOL/Multivariate_Analysis/Uniform_Limit.thy --- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Nov 02 11:56:38 2015 +0100 +++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy Mon Nov 02 16:17:09 2015 +0100 @@ -479,4 +479,22 @@ "uniform_limit J f g F \ I \ J \ uniform_limit I f g F" by (auto intro!: uniform_limitI dest!: uniform_limitD intro: eventually_rev_mono) + + +lemma uniformly_convergent_add: + "uniformly_convergent_on A f \ uniformly_convergent_on A g\ + uniformly_convergent_on A (\k x. f k x + g k x :: 'a :: {real_normed_algebra})" + unfolding uniformly_convergent_on_def by (blast dest: uniform_limit_add) + +lemma uniformly_convergent_minus: + "uniformly_convergent_on A f \ uniformly_convergent_on A g\ + uniformly_convergent_on A (\k x. f k x - g k x :: 'a :: {real_normed_algebra})" + unfolding uniformly_convergent_on_def by (blast dest: uniform_limit_minus) + +lemma uniformly_convergent_mult: + "uniformly_convergent_on A f \ + uniformly_convergent_on A (\k x. c * f k x :: 'a :: {real_normed_algebra})" + unfolding uniformly_convergent_on_def + by (blast dest: bounded_linear_uniform_limit_intros(13)) + end \ No newline at end of file diff -r e3984606b4b6 -r 980dd46a03fb src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Mon Nov 02 11:56:38 2015 +0100 +++ b/src/HOL/Transcendental.thy Mon Nov 02 16:17:09 2015 +0100 @@ -792,6 +792,29 @@ done qed +lemma termdiffs_strong_converges_everywhere: + fixes K x :: "'a::{real_normed_field,banach}" + assumes "\y. summable (\n. c n * y ^ n)" + shows "((\x. \n. c n * x^n) has_field_derivative (\n. diffs c n * x^n)) (at x)" + using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x] + by (force simp del: of_real_add) + +lemma isCont_powser: + fixes K x :: "'a::{real_normed_field,banach}" + assumes "summable (\n. c n * K ^ n)" + assumes "norm x < norm K" + shows "isCont (\x. \n. c n * x^n) x" + using termdiffs_strong[OF assms] by (blast intro!: DERIV_isCont) + +lemmas isCont_powser' = isCont_o2[OF _ isCont_powser] + +lemma isCont_powser_converges_everywhere: + fixes K x :: "'a::{real_normed_field,banach}" + assumes "\y. summable (\n. c n * y ^ n)" + shows "isCont (\x. \n. c n * x^n) x" + using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x] + by (force intro!: DERIV_isCont simp del: of_real_add) + lemma powser_limit_0: fixes a :: "nat \ 'a::{real_normed_field,banach}" assumes s: "0 < s"