# HG changeset patch
# User eberlm
# Date 1446461788 -3600
# Node ID ab2e862263e72484dd964bd873bb1bb741e6fda5
# Parent  f2e51e704a962fbdb3f62b28a11c73eabc62d97f
Rounding function, uniform limits, cotangent, binomial identities

diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Archimedean_Field.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -486,6 +486,11 @@
   "- numeral v < ceiling x \<longleftrightarrow> - numeral v < x"
   by (simp add: less_ceiling_iff)
 
+lemma ceiling_altdef: "ceiling x = (if x = of_int (floor x) then floor x else floor x + 1)"
+  by (intro ceiling_unique, (simp, linarith?)+)
+
+lemma floor_le_ceiling [simp]: "floor x \<le> ceiling x" by (simp add: ceiling_altdef)
+
 text \<open>Addition and subtraction of integers\<close>
 
 lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z"
@@ -592,4 +597,79 @@
   apply (simp add: frac_def)
   by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
 
+
+subsection \<open>Rounding to the nearest integer\<close>
+
+definition round where "round x = \<lfloor>x + 1/2\<rfloor>"
+
+lemma of_int_round_ge:     "of_int (round x) \<ge> x - 1/2"
+  and of_int_round_le:     "of_int (round x) \<le> x + 1/2"
+  and of_int_round_abs_le: "\<bar>of_int (round x) - x\<bar> \<le> 1/2"
+  and of_int_round_gt:     "of_int (round x) > x - 1/2"
+proof -
+  from floor_correct[of "x + 1/2"] have "x + 1/2 < of_int (round x) + 1" by (simp add: round_def)
+  from add_strict_right_mono[OF this, of "-1"] show A: "of_int (round x) > x - 1/2" by simp
+  thus "of_int (round x) \<ge> x - 1/2" by simp
+  from floor_correct[of "x + 1/2"] show "of_int (round x) \<le> x + 1/2" by (simp add: round_def)
+  with A show "\<bar>of_int (round x) - x\<bar> \<le> 1/2" by linarith
+qed
+
+lemma round_of_int [simp]: "round (of_int n) = n"
+  unfolding round_def by (subst floor_unique_iff) force
+
+lemma round_0 [simp]: "round 0 = 0"
+  using round_of_int[of 0] by simp
+
+lemma round_1 [simp]: "round 1 = 1"
+  using round_of_int[of 1] by simp
+
+lemma round_numeral [simp]: "round (numeral n) = numeral n"
+  using round_of_int[of "numeral n"] by simp
+
+lemma round_neg_numeral [simp]: "round (-numeral n) = -numeral n"
+  using round_of_int[of "-numeral n"] by simp
+
+lemma round_of_nat [simp]: "round (of_nat n) = of_nat n"
+  using round_of_int[of "int n"] by simp
+
+lemma round_mono: "x \<le> y \<Longrightarrow> round x \<le> round y"
+  unfolding round_def by (intro floor_mono) simp
+
+lemma round_unique: "of_int y > x - 1/2 \<Longrightarrow> of_int y \<le> x + 1/2 \<Longrightarrow> round x = y"
+unfolding round_def
+proof (rule floor_unique)
+  assume "x - 1 / 2 < of_int y"
+  from add_strict_left_mono[OF this, of 1] show "x + 1 / 2 < of_int y + 1" by simp
+qed
+
+lemma round_altdef: "round x = (if frac x \<ge> 1/2 then ceiling x else floor x)"
+  by (cases "frac x \<ge> 1/2")
+     (rule round_unique, ((simp add: frac_def field_simps ceiling_altdef, linarith?)+)[2])+
+
+lemma floor_le_round: "\<lfloor>x\<rfloor> \<le> round x"
+  unfolding round_def by (intro floor_mono) simp
+
+lemma ceiling_ge_round: "\<lceil>x\<rceil> \<ge> round x" unfolding round_altdef by simp
+     
+lemma round_diff_minimal: 
+  fixes z :: "'a :: floor_ceiling"
+  shows "abs (z - of_int (round z)) \<le> abs (z - of_int m)"
+proof (cases "of_int m \<ge> z")
+  case True
+  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (ceiling z) - z\<bar>"
+    unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith?
+  also have "of_int \<lceil>z\<rceil> - z \<ge> 0" by linarith
+  with True have "\<bar>of_int (ceiling z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
+    by (simp add: ceiling_le_iff)
+  finally show ?thesis .
+next
+  case False
+  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (floor z) - z\<bar>"
+    unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith?
+  also have "z - of_int \<lfloor>z\<rfloor> \<ge> 0" by linarith
+  with False have "\<bar>of_int (floor z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
+    by (simp add: le_floor_iff)
+  finally show ?thesis .
+qed
+
 end
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Binomial.thy
--- a/src/HOL/Binomial.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Binomial.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -38,6 +38,10 @@
 lemma fact_mono_nat: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: nat)"
   by (induct n) (auto simp: le_Suc_eq)
 
+lemma fact_in_Nats: "fact n \<in> \<nat>" by (induction n) auto
+
+lemma fact_in_Ints: "fact n \<in> \<int>" by (induction n) auto
+
 context
   assumes "SORT_CONSTRAINT('a::linordered_semidom)"
 begin
@@ -381,6 +385,41 @@
 lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
   by (induct n) auto
 
+lemma choose_alternating_sum: 
+  "n > 0 \<Longrightarrow> (\<Sum>i\<le>n. (-1)^i * of_nat (n choose i)) = (0 :: 'a :: comm_ring_1)"
+  using binomial_ring[of "-1 :: 'a" 1 n] by (simp add: atLeast0AtMost mult_of_nat_commute zero_power)
+
+lemma choose_even_sum:
+  assumes "n > 0"
+  shows   "2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"
+proof - 
+  have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) + (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"
+    using choose_row_sum[of n]
+    by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)
+  also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) + (-1) ^ i * of_nat (n choose i))"
+    by (simp add: setsum.distrib)
+  also have "\<dots> = 2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0)" 
+    by (subst setsum_right_distrib, intro setsum.cong) simp_all
+  finally show ?thesis ..
+qed
+
+lemma choose_odd_sum:
+  assumes "n > 0"
+  shows   "2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"
+proof - 
+  have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) - (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"
+    using choose_row_sum[of n]
+    by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)
+  also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) - (-1) ^ i * of_nat (n choose i))"
+    by (simp add: setsum_subtractf)
+  also have "\<dots> = 2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0)" 
+    by (subst setsum_right_distrib, intro setsum.cong) simp_all
+  finally show ?thesis ..
+qed
+
+lemma choose_row_sum': "(\<Sum>k\<le>n. (n choose k)) = 2 ^ n"
+  using choose_row_sum[of n] by (simp add: atLeast0AtMost)
+
 lemma natsum_reverse_index:
   fixes m::nat
   shows "(\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n - k)) \<Longrightarrow> (\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)"
@@ -417,6 +456,12 @@
 
 lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"
   by (simp add: pochhammer_def)
+  
+lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
+  by (simp add: pochhammer_def of_nat_setprod)
+
+lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"
+  by (simp add: pochhammer_def of_int_setprod)
 
 lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"
 proof -
@@ -460,6 +505,18 @@
     done
 qed
 
+lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"
+proof (induction n arbitrary: z)
+  case (Suc n z)
+  have "pochhammer z (Suc (Suc n)) = z * pochhammer (z + 1) (Suc n)" 
+    by (simp add: pochhammer_rec)
+  also note Suc
+  also have "z * ((z + 1 + of_nat n) * pochhammer (z + 1) n) = 
+               (z + of_nat (Suc n)) * pochhammer z (Suc n)"
+    by (simp_all add: pochhammer_rec algebra_simps)
+  finally show ?case .
+qed simp_all
+
 lemma pochhammer_fact: "fact n = pochhammer 1 n"
   unfolding fact_altdef
   apply (cases n)
@@ -547,6 +604,32 @@
   unfolding pochhammer_minus
   by (simp add: of_nat_diff pochhammer_fact)
 
+lemma pochhammer_product': 
+  "pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m"
+proof (induction n arbitrary: z)
+  case (Suc n z)
+  have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m = 
+            z * (pochhammer (z + 1) n * pochhammer (z + 1 + of_nat n) m)"
+    by (simp add: pochhammer_rec ac_simps)
+  also note Suc[symmetric]
+  also have "z * pochhammer (z + 1) (n + m) = pochhammer z (Suc (n + m))"
+    by (subst pochhammer_rec) simp
+  finally show ?case by simp
+qed simp
+
+lemma pochhammer_product: 
+  "m \<le> n \<Longrightarrow> 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_absorb_comp:
+  "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k" 
+  (is "?lhs = ?rhs")
+proof -
+  have "?lhs = -pochhammer (-r) (Suc k)" by (subst pochhammer_rec') (simp add: algebra_simps)
+  also have "\<dots> = ?rhs" by (subst pochhammer_rec) simp
+  finally show ?thesis .
+qed
+
 
 subsection\<open>Generalized binomial coefficients\<close>
 
@@ -729,6 +812,89 @@
   then show ?thesis using kn by simp
 qed
 
+lemma choose_rising_sum:
+  "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))"
+  "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose m)"
+proof -
+  show "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))" by (induction m) simp_all
+  also have "... = ((n + m + 1) choose m)" by (subst binomial_symmetric) simp_all
+  finally show "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose m)" .
+qed
+
+lemma choose_linear_sum:
+  "(\<Sum>i\<le>n. i * (n choose i)) = n * 2 ^ (n - 1)"
+proof (cases n)
+  case (Suc m)
+  have "(\<Sum>i\<le>n. i * (n choose i)) = (\<Sum>i\<le>Suc m. i * (Suc m choose i))" by (simp add: Suc)
+  also have "... = Suc m * 2 ^ m"
+    by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_right_distrib[symmetric]) 
+       (simp add: choose_row_sum')
+  finally show ?thesis using Suc by simp
+qed simp_all
+
+lemma choose_alternating_linear_sum:
+  assumes "n \<noteq> 1"
+  shows   "(\<Sum>i\<le>n. (-1)^i * of_nat i * of_nat (n choose i) :: 'a :: comm_ring_1) = 0"
+proof (cases n)
+  case (Suc m)
+  with assms have "m > 0" by simp
+  have "(\<Sum>i\<le>n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) = 
+            (\<Sum>i\<le>Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))" by (simp add: Suc)
+  also have "... = (\<Sum>i\<le>m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))"
+    by (simp only: setsum_atMost_Suc_shift setsum_right_distrib[symmetric] of_nat_mult mult_ac) simp
+  also have "... = -of_nat (Suc m) * (\<Sum>i\<le>m. (-1) ^ i * of_nat ((m choose i)))"
+    by (subst setsum_right_distrib, rule setsum.cong[OF refl], subst Suc_times_binomial)
+       (simp add: algebra_simps of_nat_mult)
+  also have "(\<Sum>i\<le>m. (-1 :: 'a) ^ i * of_nat ((m choose i))) = 0"
+    using choose_alternating_sum[OF `m > 0`] by simp
+  finally show ?thesis by simp
+qed simp
+
+lemma vandermonde:
+  "(\<Sum>k\<le>r. (m choose k) * (n choose (r - k))) = (m + n) choose r"
+proof (induction n arbitrary: r)
+  case 0
+  have "(\<Sum>k\<le>r. (m choose k) * (0 choose (r - k))) = (\<Sum>k\<le>r. if k = r then (m choose k) else 0)"
+    by (intro setsum.cong) simp_all
+  also have "... = m choose r" by (simp add: setsum.delta)
+  finally show ?case by simp
+next
+  case (Suc n r)
+  show ?case by (cases r) (simp_all add: Suc [symmetric] algebra_simps setsum.distrib Suc_diff_le)
+qed
+
+lemma choose_square_sum:
+  "(\<Sum>k\<le>n. (n choose k)^2) = ((2*n) choose n)"
+  using vandermonde[of n n n] by (simp add: power2_eq_square mult_2 binomial_symmetric [symmetric])
+
+lemma pochhammer_binomial_sum:
+  fixes a b :: "'a :: comm_ring_1"
+  shows "pochhammer (a + b) n = (\<Sum>k\<le>n. of_nat (n choose k) * pochhammer a k * pochhammer b (n - k))"
+proof (induction n arbitrary: a b)
+  case (Suc n a b)
+  have "(\<Sum>k\<le>Suc n. of_nat (Suc n choose k) * pochhammer a k * pochhammer b (Suc n - k)) =
+            (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
+            ((\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
+            pochhammer b (Suc n))"
+    by (subst setsum_atMost_Suc_shift) (simp add: ring_distribs setsum.distrib)
+  also have "(\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) =
+               a * pochhammer ((a + 1) + b) n"
+    by (subst Suc) (simp add: setsum_right_distrib pochhammer_rec mult_ac)
+  also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + pochhammer b (Suc n) = 
+               (\<Sum>i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
+    by (subst setsum_head_Suc, simp, subst setsum_shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost)
+  also have "... = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
+    using Suc by (intro setsum.mono_neutral_right) (auto simp: not_le binomial_eq_0)
+  also have "... = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc (n - i)))"
+    by (intro setsum.cong) (simp_all add: Suc_diff_le)
+  also have "... = b * pochhammer (a + (b + 1)) n"
+    by (subst Suc) (simp add: setsum_right_distrib mult_ac pochhammer_rec)
+  also have "a * pochhammer ((a + 1) + b) n + b * pochhammer (a + (b + 1)) n =
+               pochhammer (a + b) (Suc n)" by (simp add: pochhammer_rec algebra_simps)
+  finally show ?case ..
+qed simp_all
+
+
 text\<open>Contributed by Manuel Eberl, generalised by LCP.
   Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"}\<close>
 lemma gbinomial_altdef_of_nat:
@@ -774,6 +940,285 @@
   finally show ?thesis .
 qed
 
+lemma gbinomial_negated_upper: "(a gchoose b) = (-1) ^ b * ((of_nat b - a - 1) gchoose b)"
+  by (simp add: gbinomial_pochhammer pochhammer_minus algebra_simps)
+
+lemma gbinomial_minus: "((-a) gchoose b) = (-1) ^ b * ((a + of_nat b - 1) gchoose b)"
+  by (subst gbinomial_negated_upper) (simp add: add_ac)
+
+lemma Suc_times_gbinomial:
+  "of_nat (Suc b) * ((a + 1) gchoose (Suc b)) = (a + 1) * (a gchoose b)"
+proof (cases b)
+  case (Suc b)
+  hence "((a + 1) gchoose (Suc (Suc b))) = 
+             (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
+    by (simp add: field_simps gbinomial_def)
+  also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
+    by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
+  also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
+    by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
+  finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc)
+qed simp
+
+lemma gbinomial_factors:
+  "((a + 1) gchoose (Suc b)) = (a + 1) / of_nat (Suc b) * (a gchoose b)"
+proof (cases b)
+  case (Suc b)
+  hence "((a + 1) gchoose (Suc (Suc b))) = 
+             (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
+    by (simp add: field_simps gbinomial_def)
+  also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
+    by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
+  also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
+    by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
+  finally show ?thesis by (simp add: Suc)
+qed simp
+
+lemma gbinomial_rec: "((r + 1) gchoose (Suc k)) = (r gchoose k) * ((r + 1) / of_nat (Suc k))"
+  using gbinomial_mult_1[of r k]
+  by (subst gbinomial_Suc_Suc) (simp add: field_simps del: of_nat_Suc, simp add: algebra_simps)
+
+lemma gbinomial_of_nat_symmetric: "k \<le> n \<Longrightarrow> (of_nat n) gchoose k = (of_nat n) gchoose (n - k)"
+  using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric])
+
+
+text \<open>The absorption identity (equation 5.5 \cite[p.~157]{GKP}):\[
+{r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.
+\]\<close>
+lemma gbinomial_absorption': 
+  "k > 0 \<Longrightarrow> (r gchoose k) = (r / of_nat(k)) * (r - 1 gchoose (k - 1))"
+  using gbinomial_rec[of "r - 1" "k - 1"] 
+  by (simp_all add: gbinomial_rec field_simps del: of_nat_Suc)
+
+text \<open>The absorption identity is written in the following form to avoid
+division by $k$ (the lower index) and therefore remove the $k \neq 0$
+restriction\cite[p.~157]{GKP}:\[
+k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k.
+\]\<close>
+lemma gbinomial_absorption:
+  "of_nat (Suc k) * (r gchoose Suc k) = r * ((r - 1) gchoose k)"
+  using gbinomial_absorption'[of "Suc k" r] by (simp add: field_simps del: of_nat_Suc)
+
+text \<open>The absorption identity for natural number binomial coefficients:\<close>
+lemma binomial_absorption:
+  "Suc k * (n choose Suc k) = n * ((n - 1) choose k)"
+  by (cases n) (simp_all add: binomial_eq_0 Suc_times_binomial del: binomial_Suc_Suc mult_Suc)
+
+text \<open>The absorption companion identity for natural number coefficients,
+following the proof by GKP \cite[p.~157]{GKP}:\<close>
+lemma binomial_absorb_comp:
+  "(n - k) * (n choose k) = n * ((n - 1) choose k)" (is "?lhs = ?rhs")
+proof (cases "n \<le> k")
+  case False
+  then have "?rhs = Suc ((n - 1) - k) * (n choose Suc ((n - 1) - k))"
+    using binomial_symmetric[of k "n - 1"] binomial_absorption[of "(n - 1) - k" n]
+    by simp
+  also from False have "Suc ((n - 1) - k) = n - k" by simp
+  also from False have "n choose \<dots> = n choose k" by (intro binomial_symmetric [symmetric]) simp_all
+  finally show ?thesis ..
+qed auto
+
+text \<open>The generalised absorption companion identity:\<close>
+lemma gbinomial_absorb_comp: "(r - of_nat k) * (r gchoose k) = r * ((r - 1) gchoose k)"
+  using pochhammer_absorb_comp[of r k] by (simp add: gbinomial_pochhammer)
+
+lemma gbinomial_addition_formula:
+  "r gchoose (Suc k) = ((r - 1) gchoose (Suc k)) + ((r - 1) gchoose k)"
+  using gbinomial_Suc_Suc[of "r - 1" k] by (simp add: algebra_simps)
+
+lemma binomial_addition_formula:
+  "0 < n \<Longrightarrow> n choose (Suc k) = ((n - 1) choose (Suc k)) + ((n - 1) choose k)"
+  by (subst choose_reduce_nat) simp_all
+
+
+text \<open>
+  Equation 5.9 of the reference material \cite[p.~159]{GKP} is a useful
+  summation formula, operating on both indices:\[
+  \sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n},
+   \quad \textnormal{integer } n.
+  \] 
+\<close>
+lemma gbinomial_parallel_sum:
+"(\<Sum>k\<le>n. (r + of_nat k) gchoose k) = (r + of_nat n + 1) gchoose n"
+proof (induction n)
+  case (Suc m)
+  thus ?case using gbinomial_Suc_Suc[of "(r + of_nat m + 1)" m] by (simp add: add_ac)
+qed auto
+
+subsection \<open>Summation on the upper index\<close>
+text \<open>
+  Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP},
+  aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} = 
+  {n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\]
+\<close>
+lemma gbinomial_sum_up_index:
+  "(\<Sum>k = 0..n. (of_nat k gchoose m) :: 'a :: field_char_0) = (of_nat n + 1) gchoose (m + 1)"
+proof (induction n)
+  case 0
+  show ?case using gbinomial_Suc_Suc[of 0 m] by (cases m) auto
+next
+  case (Suc n)
+  thus ?case using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" m] by (simp add: add_ac)
+qed
+
+lemma gbinomial_index_swap: 
+  "((-1) ^ m) * ((- (of_nat n) - 1) gchoose m) = ((-1) ^ n) * ((- (of_nat m) - 1) gchoose n)"
+  (is "?lhs = ?rhs")
+proof -
+  have "?lhs = (of_nat (m + n) gchoose m)"
+    by (subst gbinomial_negated_upper) (simp add: power_mult_distrib [symmetric])
+  also have "\<dots> = (of_nat (m + n) gchoose n)" by (subst gbinomial_of_nat_symmetric) simp_all
+  also have "\<dots> = ?rhs" by (subst gbinomial_negated_upper) simp
+  finally show ?thesis .
+qed
+
+lemma gbinomial_sum_lower_neg: 
+  "(\<Sum>k\<le>m. (r gchoose k) * (- 1) ^ k) = (- 1) ^ m * (r - 1 gchoose m)" (is "?lhs = ?rhs")
+proof -
+  have "?lhs = (\<Sum>k\<le>m. -(r + 1) + of_nat k gchoose k)"
+    by (intro setsum.cong[OF refl]) (subst gbinomial_negated_upper, simp add: power_mult_distrib)
+  also have "\<dots>  = -r + of_nat m gchoose m" by (subst gbinomial_parallel_sum) simp
+  also have "\<dots> = ?rhs" by (subst gbinomial_negated_upper) (simp add: power_mult_distrib)
+  finally show ?thesis .
+qed
+
+lemma gbinomial_partial_row_sum:
+"(\<Sum>k\<le>m. (r gchoose k) * ((r / 2) - of_nat k)) = ((of_nat m + 1)/2) * (r gchoose (m + 1))"
+proof (induction m)
+  case (Suc mm)
+  hence "(\<Sum>k\<le>Suc mm. (r gchoose k) * (r / 2 - of_nat k)) = 
+             (r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: algebra_simps)
+  also have "\<dots> = r * (r - 1 gchoose Suc mm) / 2" by (subst gbinomial_absorb_comp) (rule refl)
+  also have "\<dots> = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))"
+    by (subst gbinomial_absorption [symmetric]) simp
+  finally show ?case .
+qed simp_all
+
+lemma setsum_bounds_lt_plus1: "(\<Sum>k<mm. f (Suc k)) = (\<Sum>k=1..mm. f k)"
+  by (induction mm) simp_all
+
+lemma gbinomial_partial_sum_poly:
+  "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
+       (\<Sum>k\<le>m. (-r gchoose k) * (-x)^k * (x + y)^(m-k))" (is "?lhs m = ?rhs m")
+proof (induction m)
+  case (Suc mm)
+  def G \<equiv> "\<lambda>i k. (of_nat i + r gchoose k) * x^k * y^(i-k)" and S \<equiv> ?lhs
+  have SG_def: "S = (\<lambda>i. (\<Sum>k\<le>i. (G i k)))" unfolding S_def G_def ..
+
+  have "S (Suc mm) = G (Suc mm) 0 + (\<Sum>k=Suc 0..Suc mm. G (Suc mm) k)"
+    using SG_def by (simp add: setsum_head_Suc atLeast0AtMost [symmetric])
+  also have "(\<Sum>k=Suc 0..Suc mm. G (Suc mm) k) = (\<Sum>k=0..mm. G (Suc mm) (Suc k))"
+    by (subst setsum_shift_bounds_cl_Suc_ivl) simp
+  also have "\<dots> = (\<Sum>k=0..mm. ((of_nat mm + r gchoose (Suc k))
+                    + (of_nat mm + r gchoose k)) * x^(Suc k) * y^(mm - k))"
+    unfolding G_def by (subst gbinomial_addition_formula) simp
+  also have "\<dots> = (\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))
+                  + (\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k))"
+    by (subst setsum.distrib [symmetric]) (simp add: algebra_simps)
+  also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) = 
+               (\<Sum>k<Suc mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))"
+    by (simp only: atLeast0AtMost lessThan_Suc_atMost)
+  also have "\<dots> = (\<Sum>k<mm. (of_nat mm + r gchoose Suc k) * x^(Suc k) * y^(mm-k)) 
+                      + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" (is "_ = ?A + ?B")
+    by (subst setsum_lessThan_Suc) simp
+  also have "?A = (\<Sum>k=1..mm. (of_nat mm + r gchoose k) * x^k * y^(mm - k + 1))"
+  proof (subst setsum_bounds_lt_plus1 [symmetric], intro setsum.cong[OF refl], clarify)
+    fix k assume "k < mm"
+    hence "mm - k = mm - Suc k + 1" by linarith
+    thus "(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - k) =
+            (of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - Suc k + 1)" by (simp only:)
+  qed
+  also have "\<dots> + ?B = y * (\<Sum>k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" 
+    unfolding G_def by (subst setsum_right_distrib) (simp add: algebra_simps)
+  also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k)) = x * (S mm)"
+      unfolding S_def by (subst setsum_right_distrib) (simp add: atLeast0AtMost algebra_simps)
+  also have "(G (Suc mm) 0) = y * (G mm 0)" by (simp add: G_def)
+  finally have "S (Suc mm) = y * ((G mm 0) + (\<Sum>k=1..mm. (G mm k))) 
+                + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)"
+    by (simp add: ring_distribs)
+  also have "(G mm 0) + (\<Sum>k=1..mm. (G mm k)) = S mm" 
+    by (simp add: setsum_head_Suc[symmetric] SG_def atLeast0AtMost)
+  finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" 
+    by (simp add: algebra_simps)
+  also have "(of_nat mm + r gchoose (Suc mm)) = (-1) ^ (Suc mm) * (-r gchoose (Suc mm))"
+    by (subst gbinomial_negated_upper) simp
+  also have "(-1) ^ Suc mm * (- r gchoose Suc mm) * x ^ Suc mm =
+                 (-r gchoose (Suc mm)) * (-x) ^ Suc mm" by (simp add: power_minus[of x])
+  also have "(x + y) * S mm + \<dots> = (x + y) * ?rhs mm + (-r gchoose (Suc mm)) * (-x)^Suc mm"
+    unfolding S_def by (subst Suc.IH) simp
+  also have "(x + y) * ?rhs mm = (\<Sum>n\<le>mm. ((- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n)))"
+    by (subst setsum_right_distrib, rule setsum.cong) (simp_all add: Suc_diff_le)
+  also have "\<dots> + (-r gchoose (Suc mm)) * (-x)^Suc mm = 
+                 (\<Sum>n\<le>Suc mm. (- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))" by simp
+  finally show ?case unfolding S_def .
+qed simp_all
+
+lemma gbinomial_partial_sum_poly_xpos:
+  "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) = 
+     (\<Sum>k\<le>m. (of_nat k + r - 1 gchoose k) * x^k * (x + y)^(m-k))"
+  apply (subst gbinomial_partial_sum_poly)
+  apply (subst gbinomial_negated_upper)
+  apply (intro setsum.cong, rule refl)
+  apply (simp add: power_mult_distrib [symmetric])
+  done
+
+lemma setsum_nat_symmetry: 
+  "(\<Sum>k = 0..(m::nat). f k) = (\<Sum>k = 0..m. f (m - k))"
+  by (rule setsum.reindex_bij_witness[where i="\<lambda>i. m - i" and j="\<lambda>i. m - i"]) auto
+
+lemma binomial_r_part_sum: "(\<Sum>k\<le>m. (2 * m + 1 choose k)) = 2 ^ (2 * m)"
+proof -
+  have "2 * 2^(2*m) = (\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k))"
+    using choose_row_sum[where n="2 * m + 1"] by simp
+  also have "(\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k)) = (\<Sum>k = 0..m. (2 * m + 1 choose k))
+                + (\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k))"
+    using setsum_ub_add_nat[of 0 m "\<lambda>k. 2 * m + 1 choose k" "m+1"] by (simp add: mult_2)
+  also have "(\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k)) =
+                 (\<Sum>k = 0..m. (2 * m + 1 choose (k + (m + 1))))"
+    by (subst setsum_shift_bounds_cl_nat_ivl [symmetric]) (simp add: mult_2)
+  also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose (m - k)))"
+    by (intro setsum.cong[OF refl], subst binomial_symmetric) simp_all
+  also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose k))"
+    by (subst (2) setsum_nat_symmetry) (rule refl)
+  also have "\<dots> + \<dots> = 2 * \<dots>" by simp
+  finally show ?thesis by (subst (asm) mult_cancel1) (simp add: atLeast0AtMost)
+qed
+
+lemma gbinomial_r_part_sum:
+  "(\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)" (is "?lhs = ?rhs")
+proof -
+  have "?lhs = of_nat (\<Sum>k\<le>m. (2 * m + 1) choose k)" 
+    by (simp add: binomial_gbinomial of_nat_mult add_ac of_nat_setsum)
+  also have "\<dots> = of_nat (2 ^ (2 * m))" by (subst binomial_r_part_sum) (rule refl)
+  finally show ?thesis by (simp add: of_nat_power)
+qed
+
+lemma gbinomial_sum_nat_pow2:
+   "(\<Sum>k\<le>m. (of_nat (m + k) gchoose k :: 'a :: field_char_0) / 2 ^ k) = 2 ^ m" (is "?lhs = ?rhs")
+proof -
+  have "2 ^ m * 2 ^ m = (2 ^ (2*m) :: 'a)" by (induction m) simp_all
+  also have "\<dots> = (\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k))" using gbinomial_r_part_sum ..
+  also have "\<dots> = (\<Sum>k\<le>m. (of_nat (m + k) gchoose k) * 2 ^ (m - k))"
+    using gbinomial_partial_sum_poly_xpos[where x="1" and y="1" and r="of_nat m + 1" and m="m"]
+    by (simp add: add_ac)
+  also have "\<dots> = 2 ^ m * (\<Sum>k\<le>m. (of_nat (m + k) gchoose k) / 2 ^ k)"
+    by (subst setsum_right_distrib) (simp add: algebra_simps power_diff)
+  finally show ?thesis by (subst (asm) mult_left_cancel) simp_all
+qed
+
+lemma gbinomial_trinomial_revision:
+  assumes "k \<le> m"
+  shows   "(r gchoose m) * (of_nat m gchoose k) = (r gchoose k) * (r - of_nat k gchoose (m - k))"
+proof -
+  have "(r gchoose m) * (of_nat m gchoose k) = 
+            (r gchoose m) * fact m / (fact k * fact (m - k))"
+    using assms by (simp add: binomial_gbinomial [symmetric] binomial_fact)
+  also have "\<dots> = (r gchoose k) * (r - of_nat k gchoose (m - k))" using assms
+    by (simp add: gbinomial_pochhammer power_diff pochhammer_product)
+  finally show ?thesis .
+qed
+
+
 text\<open>Versions of the theorems above for the natural-number version of "choose"\<close>
 lemma binomial_altdef_of_nat:
   fixes n k :: nat
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Complex.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -171,6 +171,17 @@
     "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
   by (auto simp: Reals_def)
 
+lemma complex_Re_fact [simp]: "Re (fact n) = fact n"
+proof -
+  have "(fact n :: complex) = of_real (fact n)" by simp
+  also have "Re \<dots> = fact n" by (subst Re_complex_of_real) simp_all
+  finally show ?thesis .
+qed
+
+lemma complex_Im_fact [simp]: "Im (fact n) = 0"
+  by (subst of_nat_fact [symmetric]) (simp only: complex_Im_of_nat)
+
+
 subsection \<open>The Complex Number $i$\<close>
 
 primcorec "ii" :: complex  ("\<i>") where
@@ -497,6 +508,12 @@
 lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
   by simp
 
+lemma complex_cnj_fact [simp]: "cnj (fact n) = fact n"
+  by (subst of_nat_fact [symmetric], subst complex_cnj_of_nat) simp
+
+lemma complex_cnj_pochhammer [simp]: "cnj (pochhammer z n) = pochhammer (cnj z) n"
+  by (induction n arbitrary: z) (simp_all add: pochhammer_rec)
+
 lemma bounded_linear_cnj: "bounded_linear cnj"
   using complex_cnj_add complex_cnj_scaleR
   by (rule bounded_linear_intro [where K=1], simp)
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Filter.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -393,6 +393,11 @@
 lemma eventually_happens: "eventually P net \<Longrightarrow> net = bot \<or> (\<exists>x. P x)"
   by (metis frequentlyE eventually_frequently)
 
+lemma eventually_happens':
+  assumes "F \<noteq> bot" "eventually P F"
+  shows   "\<exists>x. P x"
+  using assms eventually_frequently frequentlyE by blast
+
 abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
   where "trivial_limit F \<equiv> F = bot"
 
@@ -611,6 +616,15 @@
 lemma eventually_gt_at_top: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
   unfolding eventually_at_top_dense by auto
 
+lemma eventually_all_ge_at_top:
+  assumes "eventually P (at_top :: ('a :: linorder) filter)"
+  shows   "eventually (\<lambda>x. \<forall>y\<ge>x. P y) at_top"
+proof -
+  from assms obtain x where "\<And>y. y \<ge> x \<Longrightarrow> P y" by (auto simp: eventually_at_top_linorder)
+  hence "\<forall>z\<ge>y. P z" if "y \<ge> x" for y using that by simp
+  thus ?thesis by (auto simp: eventually_at_top_linorder)
+qed
+
 definition at_bot :: "('a::order) filter"
   where "at_bot = (INF k. principal {.. k})"
 
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Int.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -225,6 +225,9 @@
 lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
   by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult)
 
+lemma mult_of_int_commute: "of_int x * y = y * of_int x"
+  by (transfer fixing: times) (auto simp: algebra_simps mult_of_nat_commute)
+
 text\<open>Collapse nested embeddings\<close>
 lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
 by (induct n) auto
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Library/Convex.thy
--- a/src/HOL/Library/Convex.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Library/Convex.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -304,6 +304,42 @@
   where "convex_on s f \<longleftrightarrow>
     (\<forall>x\<in>s. \<forall>y\<in>s. \<forall>u\<ge>0. \<forall>v\<ge>0. u + v = 1 \<longrightarrow> f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y)"
 
+lemma convex_onI [intro?]:
+  assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
+             f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
+  shows   "convex_on A f"
+  unfolding convex_on_def
+proof clarify
+  fix x y u v assume A: "x \<in> A" "y \<in> A" "(u::real) \<ge> 0" "v \<ge> 0" "u + v = 1"
+  from A(5) have [simp]: "v = 1 - u" by (simp add: algebra_simps)
+  from A(1-4) show "f (u *\<^sub>R x + v *\<^sub>R y) \<le> u * f x + v * f y" using assms[of u y x]
+    by (cases "u = 0 \<or> u = 1") (auto simp: algebra_simps)
+qed
+
+lemma convex_on_linorderI [intro?]:
+  fixes A :: "('a::{linorder,real_vector}) set"
+  assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x < y \<Longrightarrow>
+             f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
+  shows   "convex_on A f"
+proof
+  fix t x y assume A: "x \<in> A" "y \<in> A" "(t::real) > 0" "t < 1"
+  case (goal1 t x y)
+  with goal1 assms[of t x y] assms[of "1 - t" y x]
+    show ?case by (cases x y rule: linorder_cases) (auto simp: algebra_simps)
+qed
+
+lemma convex_onD:
+  assumes "convex_on A f"
+  shows   "\<And>t x y. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
+             f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
+  using assms unfolding convex_on_def by auto
+
+lemma convex_onD_Icc:
+  assumes "convex_on {x..y} f" "x \<le> (y :: _ :: {real_vector,preorder})"
+  shows   "\<And>t. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow>
+             f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
+  using assms(2) by (intro convex_onD[OF assms(1)]) simp_all
+
 lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
   unfolding convex_on_def by auto
 
@@ -835,4 +871,91 @@
   show ?thesis by auto
 qed
 
+
+subsection \<open>Convexity of real functions\<close>
+
+lemma convex_on_realI:
+  assumes "connected A"
+  assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
+  assumes "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<le> y \<Longrightarrow> f' x \<le> f' y"
+  shows   "convex_on A f"
+proof (rule convex_on_linorderI)
+  fix t x y :: real
+  assume t: "t > 0" "t < 1" and xy: "x \<in> A" "y \<in> A" "x < y"
+  def z \<equiv> "(1 - t) * x + t * y"
+  with `connected A` and xy have ivl: "{x..y} \<subseteq> A" using connected_contains_Icc by blast
+  
+  from xy t have xz: "z > x" by (simp add: z_def algebra_simps)
+  have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps)
+  also from xy t have "... > 0" by (intro mult_pos_pos) simp_all
+  finally have yz: "z < y" by simp
+    
+  from assms xz yz ivl t have "\<exists>\<xi>. \<xi> > x \<and> \<xi> < z \<and> f z - f x = (z - x) * f' \<xi>"
+    by (intro MVT2) (auto intro!: assms(2))
+  then obtain \<xi> where \<xi>: "\<xi> > x" "\<xi> < z" "f' \<xi> = (f z - f x) / (z - x)" by auto
+  from assms xz yz ivl t have "\<exists>\<eta>. \<eta> > z \<and> \<eta> < y \<and> f y - f z = (y - z) * f' \<eta>"
+    by (intro MVT2) (auto intro!: assms(2))
+  then obtain \<eta> where \<eta>: "\<eta> > z" "\<eta> < y" "f' \<eta> = (f y - f z) / (y - z)" by auto
+  
+  from \<eta>(3) have "(f y - f z) / (y - z) = f' \<eta>" ..
+  also from \<xi> \<eta> ivl have "\<xi> \<in> A" "\<eta> \<in> A" by auto
+  with \<xi> \<eta> have "f' \<eta> \<ge> f' \<xi>" by (intro assms(3)) auto
+  also from \<xi>(3) have "f' \<xi> = (f z - f x) / (z - x)" .
+  finally have "(f y - f z) * (z - x) \<ge> (f z - f x) * (y - z)"
+    using xz yz by (simp add: field_simps)
+  also have "z - x = t * (y - x)" by (simp add: z_def algebra_simps)
+  also have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps)
+  finally have "(f y - f z) * t \<ge> (f z - f x) * (1 - t)" using xy by simp
+  thus "(1 - t) * f x + t * f y \<ge> f ((1 - t) *\<^sub>R x + t *\<^sub>R y)"
+    by (simp add: z_def algebra_simps)
+qed
+
+lemma convex_on_inverse:
+  assumes "A \<subseteq> {0<..}"
+  shows   "convex_on A (inverse :: real \<Rightarrow> real)"
+proof (rule convex_on_subset[OF _ assms], intro convex_on_realI[of _ _ "\<lambda>x. -inverse (x^2)"])
+  fix u v :: real assume "u \<in> {0<..}" "v \<in> {0<..}" "u \<le> v"
+  with assms show "-inverse (u^2) \<le> -inverse (v^2)"
+    by (intro le_imp_neg_le le_imp_inverse_le power_mono) (simp_all)
+qed (insert assms, auto intro!: derivative_eq_intros simp: divide_simps power2_eq_square)
+
+lemma convex_onD_Icc':
+  assumes "convex_on {x..y} f" "c \<in> {x..y}"
+  defines "d \<equiv> y - x"
+  shows   "f c \<le> (f y - f x) / d * (c - x) + f x"
+proof (cases y x rule: linorder_cases)
+  assume less: "x < y"
+  hence d: "d > 0" by (simp add: d_def)
+  from assms(2) less have A: "0 \<le> (c - x) / d" "(c - x) / d \<le> 1" 
+    by (simp_all add: d_def divide_simps)
+  have "f c = f (x + (c - x) * 1)" by simp
+  also from less have "1 = ((y - x) / d)" by (simp add: d_def)
+  also from d have "x + (c - x) * \<dots> = (1 - (c - x) / d) *\<^sub>R x + ((c - x) / d) *\<^sub>R y" 
+    by (simp add: field_simps)
+  also have "f \<dots> \<le> (1 - (c - x) / d) * f x + (c - x) / d * f y" using assms less
+    by (intro convex_onD_Icc) simp_all
+  also from d have "\<dots> = (f y - f x) / d * (c - x) + f x" by (simp add: field_simps)
+  finally show ?thesis .
+qed (insert assms(2), simp_all)
+
+lemma convex_onD_Icc'':
+  assumes "convex_on {x..y} f" "c \<in> {x..y}"
+  defines "d \<equiv> y - x"
+  shows   "f c \<le> (f x - f y) / d * (y - c) + f y"
+proof (cases y x rule: linorder_cases)
+  assume less: "x < y"
+  hence d: "d > 0" by (simp add: d_def)
+  from assms(2) less have A: "0 \<le> (y - c) / d" "(y - c) / d \<le> 1" 
+    by (simp_all add: d_def divide_simps)
+  have "f c = f (y - (y - c) * 1)" by simp
+  also from less have "1 = ((y - x) / d)" by (simp add: d_def)
+  also from d have "y - (y - c) * \<dots> = (1 - (1 - (y - c) / d)) *\<^sub>R x + (1 - (y - c) / d) *\<^sub>R y" 
+    by (simp add: field_simps)
+  also have "f \<dots> \<le> (1 - (1 - (y - c) / d)) * f x + (1 - (y - c) / d) * f y" using assms less
+    by (intro convex_onD_Icc) (simp_all add: field_simps)
+  also from d have "\<dots> = (f x - f y) / d * (y - c) + f y" by (simp add: field_simps)
+  finally show ?thesis .
+qed (insert assms(2), simp_all)
+
+
 end
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Limits.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -137,12 +137,34 @@
     by (auto elim!: allE[of _ n])
 qed
 
+lemma Bseq_bdd_above': 
+  "Bseq (X::nat \<Rightarrow> 'a :: real_normed_vector) \<Longrightarrow> bdd_above (range (\<lambda>n. norm (X n)))"
+proof (elim BseqE, intro bdd_aboveI2)
+  fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "norm (X n) \<le> K"
+    by (auto elim!: allE[of _ n])
+qed
+
 lemma Bseq_bdd_below: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_below (range X)"
 proof (elim BseqE, intro bdd_belowI2)
   fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "- K \<le> X n"
     by (auto elim!: allE[of _ n])
 qed
 
+lemma Bseq_eventually_mono:
+  assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) sequentially" "Bseq g"
+  shows   "Bseq f" 
+proof -
+  from assms(1) obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> norm (f n) \<le> norm (g n)"
+    by (auto simp: eventually_at_top_linorder)
+  moreover from assms(2) obtain K where K: "\<And>n. norm (g n) \<le> K" by (blast elim!: BseqE)
+  ultimately have "norm (f n) \<le> max K (Max {norm (f n) |n. n < N})" for n
+    apply (cases "n < N")
+    apply (rule max.coboundedI2, rule Max.coboundedI, auto) []
+    apply (rule max.coboundedI1, force intro: order.trans[OF N K])
+    done
+  thus ?thesis by (blast intro: BseqI') 
+qed
+
 lemma lemma_NBseq_def:
   "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
 proof safe
@@ -218,6 +240,73 @@
 lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
   by (simp add: Bseq_def)
 
+lemma Bseq_add: 
+  assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
+  shows   "Bseq (\<lambda>x. f x + c)"
+proof -
+  from assms obtain K where K: "\<And>x. norm (f x) \<le> K" unfolding Bseq_def by blast
+  {
+    fix x :: nat
+    have "norm (f x + c) \<le> norm (f x) + norm c" by (rule norm_triangle_ineq)
+    also have "norm (f x) \<le> K" by (rule K)
+    finally have "norm (f x + c) \<le> K + norm c" by simp
+  }
+  thus ?thesis by (rule BseqI')
+qed
+
+lemma Bseq_add_iff: "Bseq (\<lambda>x. f x + c) \<longleftrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
+  using Bseq_add[of f c] Bseq_add[of "\<lambda>x. f x + c" "-c"] by auto
+
+lemma Bseq_mult: 
+  assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_field)"
+  assumes "Bseq (g :: nat \<Rightarrow> 'a :: real_normed_field)"
+  shows   "Bseq (\<lambda>x. f x * g x)"
+proof -
+  from assms obtain K1 K2 where K: "\<And>x. norm (f x) \<le> K1" "K1 > 0" "\<And>x. norm (g x) \<le> K2" "K2 > 0" 
+    unfolding Bseq_def by blast
+  hence "\<And>x. norm (f x * g x) \<le> K1 * K2" by (auto simp: norm_mult intro!: mult_mono)
+  thus ?thesis by (rule BseqI')
+qed
+
+lemma Bfun_const [simp]: "Bfun (\<lambda>_. c) F"
+  unfolding Bfun_metric_def by (auto intro!: exI[of _ c] exI[of _ "1::real"])
+
+lemma Bseq_cmult_iff: "(c :: 'a :: real_normed_field) \<noteq> 0 \<Longrightarrow> Bseq (\<lambda>x. c * f x) \<longleftrightarrow> Bseq f"
+proof
+  assume "c \<noteq> 0" "Bseq (\<lambda>x. c * f x)"
+  find_theorems "Bfun (\<lambda>_. ?c) _"
+  from Bfun_const this(2) have "Bseq (\<lambda>x. inverse c * (c * f x))" by (rule Bseq_mult)
+  with `c \<noteq> 0` show "Bseq f" by (simp add: divide_simps)
+qed (intro Bseq_mult Bfun_const)
+
+lemma Bseq_subseq: "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector) \<Longrightarrow> Bseq (\<lambda>x. f (g x))"
+  unfolding Bseq_def by auto
+
+lemma Bseq_Suc_iff: "Bseq (\<lambda>n. f (Suc n)) \<longleftrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
+  using Bseq_offset[of f 1] by (auto intro: Bseq_subseq)
+
+lemma increasing_Bseq_subseq_iff:
+  assumes "\<And>x y. x \<le> y \<Longrightarrow> norm (f x :: 'a :: real_normed_vector) \<le> norm (f y)" "subseq g"
+  shows   "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f"
+proof
+  assume "Bseq (\<lambda>x. f (g x))"
+  then obtain K where K: "\<And>x. norm (f (g x)) \<le> K" unfolding Bseq_def by auto
+  {
+    fix x :: nat
+    from filterlim_subseq[OF assms(2)] obtain y where "g y \<ge> x"
+      by (auto simp: filterlim_at_top eventually_at_top_linorder)
+    hence "norm (f x) \<le> norm (f (g y))" using assms(1) by blast
+    also have "norm (f (g y)) \<le> K" by (rule K)
+    finally have "norm (f x) \<le> K" .
+  }
+  thus "Bseq f" by (rule BseqI')
+qed (insert Bseq_subseq[of f g], simp_all)
+
+lemma nonneg_incseq_Bseq_subseq_iff:
+  assumes "\<And>x. f x \<ge> 0" "incseq (f :: nat \<Rightarrow> real)" "subseq g"
+  shows   "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f"
+  using assms by (intro increasing_Bseq_subseq_iff) (auto simp: incseq_def)
+
 lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
   apply (simp add: subset_eq)
   apply (rule BseqI'[where K="max (norm a) (norm b)"])
@@ -679,6 +768,16 @@
   shows "(\<And>i. i \<in> S \<Longrightarrow> continuous_on s (f i)) \<Longrightarrow> continuous_on s (\<lambda>x. \<Prod>i\<in>S. f i x)"
   unfolding continuous_on_def by (auto intro: tendsto_setprod)
 
+lemma tendsto_of_real_iff:
+  "((\<lambda>x. of_real (f x) :: 'a :: real_normed_div_algebra) ---> of_real c) F \<longleftrightarrow> (f ---> c) F"
+  unfolding tendsto_iff by simp
+
+lemma tendsto_add_const_iff:
+  "((\<lambda>x. c + f x :: 'a :: real_normed_vector) ---> c + d) F \<longleftrightarrow> (f ---> d) F"
+  using tendsto_add[OF tendsto_const[of c], of f d] 
+        tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto
+
+
 subsubsection \<open>Inverse and division\<close>
 
 lemma (in bounded_bilinear) Zfun_prod_Bfun:
@@ -892,6 +991,55 @@
   qed
 qed force
 
+lemma not_tendsto_and_filterlim_at_infinity:
+  assumes "F \<noteq> bot"
+  assumes "(f ---> (c :: 'a :: real_normed_vector)) F" 
+  assumes "filterlim f at_infinity F"
+  shows   False
+proof -
+  from tendstoD[OF assms(2), of "1/2"] 
+    have "eventually (\<lambda>x. dist (f x) c < 1/2) F" by simp
+  moreover from filterlim_at_infinity[of "norm c" f F] assms(3)
+    have "eventually (\<lambda>x. norm (f x) \<ge> norm c + 1) F" by simp
+  ultimately have "eventually (\<lambda>x. False) F"
+  proof eventually_elim
+    fix x assume A: "dist (f x) c < 1/2" and B: "norm (f x) \<ge> norm c + 1"
+    note B
+    also have "norm (f x) = dist (f x) 0" by (simp add: norm_conv_dist)
+    also have "... \<le> dist (f x) c + dist c 0" by (rule dist_triangle)
+    also note A
+    finally show False by (simp add: norm_conv_dist)
+  qed
+  with assms show False by simp
+qed
+
+lemma filterlim_at_infinity_imp_not_convergent:
+  assumes "filterlim f at_infinity sequentially"
+  shows   "\<not>convergent f"
+  by (rule notI, rule not_tendsto_and_filterlim_at_infinity[OF _ _ assms])
+     (simp_all add: convergent_LIMSEQ_iff)
+
+lemma filterlim_at_infinity_imp_eventually_ne:
+  assumes "filterlim f at_infinity F"
+  shows   "eventually (\<lambda>z. f z \<noteq> c) F"
+proof -
+  have "norm c + 1 > 0" by (intro add_nonneg_pos) simp_all
+  with filterlim_at_infinity[OF order.refl, of f F] assms
+    have "eventually (\<lambda>z. norm (f z) \<ge> norm c + 1) F" by blast
+  thus ?thesis by eventually_elim auto
+qed
+
+lemma tendsto_of_nat [tendsto_intros]: 
+  "filterlim (of_nat :: nat \<Rightarrow> 'a :: real_normed_algebra_1) at_infinity sequentially"
+proof (subst filterlim_at_infinity[OF order.refl], intro allI impI)
+  fix r :: real assume r: "r > 0"
+  def n \<equiv> "nat \<lceil>r\<rceil>"
+  from r have n: "\<forall>m\<ge>n. of_nat m \<ge> r" unfolding n_def by linarith
+  from eventually_ge_at_top[of n] show "eventually (\<lambda>m. norm (of_nat m :: 'a) \<ge> r) sequentially"
+    by eventually_elim (insert n, simp_all)
+qed
+
+
 subsection \<open>Relate @{const at}, @{const at_left} and @{const at_right}\<close>
 
 text \<open>
@@ -1075,9 +1223,27 @@
     by (auto intro: order_trans simp: filterlim_def filtermap_filtermap)
 qed
 
+lemma tendsto_mult_filterlim_at_infinity:
+  assumes "F \<noteq> bot" "(f ---> (c :: 'a :: real_normed_field)) F" "c \<noteq> 0"
+  assumes "filterlim g at_infinity F"
+  shows   "filterlim (\<lambda>x. f x * g x) at_infinity F"
+proof -
+  have "((\<lambda>x. inverse (f x) * inverse (g x)) ---> inverse c * 0) F"
+    by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0])
+  hence "filterlim (\<lambda>x. inverse (f x) * inverse (g x)) (at (inverse c * 0)) F"
+    unfolding filterlim_at using assms
+    by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
+  thus ?thesis by (subst filterlim_inverse_at_iff[symmetric]) simp_all
+qed
+
 lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
  by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
 
+lemma mult_nat_left_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. c * x :: nat) at_top sequentially"
+  by (rule filterlim_subseq) (auto simp: subseq_def)
+
+lemma mult_nat_right_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. x * c :: nat) at_top sequentially"
+  by (rule filterlim_subseq) (auto simp: subseq_def)
 
 lemma at_to_infinity:
   fixes x :: "'a :: {real_normed_field,field}"
@@ -1471,6 +1637,23 @@
 
 subsection \<open>Convergence on sequences\<close>
 
+lemma convergent_cong:
+  assumes "eventually (\<lambda>x. f x = g x) sequentially"
+  shows   "convergent f \<longleftrightarrow> convergent g"
+  unfolding convergent_def by (subst filterlim_cong[OF refl refl assms]) (rule refl)
+
+lemma convergent_Suc_iff: "convergent (\<lambda>n. f (Suc n)) \<longleftrightarrow> convergent f"
+  by (auto simp: convergent_def LIMSEQ_Suc_iff)
+
+lemma convergent_ignore_initial_segment: "convergent (\<lambda>n. f (n + m)) = convergent f"
+proof (induction m arbitrary: f)
+  case (Suc m)
+  have "convergent (\<lambda>n. f (n + Suc m)) \<longleftrightarrow> convergent (\<lambda>n. f (Suc n + m))" by simp
+  also have "\<dots> \<longleftrightarrow> convergent (\<lambda>n. f (n + m))" by (rule convergent_Suc_iff)
+  also have "\<dots> \<longleftrightarrow> convergent f" by (rule Suc)
+  finally show ?case .
+qed simp_all
+
 lemma convergent_add:
   fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
   assumes "convergent (\<lambda>n. X n)"
@@ -1505,6 +1688,71 @@
 apply (drule tendsto_minus, auto)
 done
 
+lemma convergent_diff:
+  fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
+  assumes "convergent (\<lambda>n. X n)"
+  assumes "convergent (\<lambda>n. Y n)"
+  shows "convergent (\<lambda>n. X n - Y n)"
+  using assms unfolding convergent_def by (fast intro: tendsto_diff)
+
+lemma convergent_norm:
+  assumes "convergent f"
+  shows   "convergent (\<lambda>n. norm (f n))"
+proof -
+  from assms have "f ----> lim f" by (simp add: convergent_LIMSEQ_iff)
+  hence "(\<lambda>n. norm (f n)) ----> norm (lim f)" by (rule tendsto_norm)
+  thus ?thesis by (auto simp: convergent_def)
+qed
+
+lemma convergent_of_real: 
+  "convergent f \<Longrightarrow> convergent (\<lambda>n. of_real (f n) :: 'a :: real_normed_algebra_1)"
+  unfolding convergent_def by (blast intro!: tendsto_of_real)
+
+lemma convergent_add_const_iff: 
+  "convergent (\<lambda>n. c + f n :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
+proof
+  assume "convergent (\<lambda>n. c + f n)"
+  from convergent_diff[OF this convergent_const[of c]] show "convergent f" by simp
+next
+  assume "convergent f"
+  from convergent_add[OF convergent_const[of c] this] show "convergent (\<lambda>n. c + f n)" by simp
+qed
+
+lemma convergent_add_const_right_iff: 
+  "convergent (\<lambda>n. f n + c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
+  using convergent_add_const_iff[of c f] by (simp add: add_ac)
+
+lemma convergent_diff_const_right_iff: 
+  "convergent (\<lambda>n. f n - c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
+  using convergent_add_const_right_iff[of f "-c"] by (simp add: add_ac)
+
+lemma convergent_mult:
+  fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
+  assumes "convergent (\<lambda>n. X n)"
+  assumes "convergent (\<lambda>n. Y n)"
+  shows "convergent (\<lambda>n. X n * Y n)"
+  using assms unfolding convergent_def by (fast intro: tendsto_mult)
+
+lemma convergent_mult_const_iff:
+  assumes "c \<noteq> 0"
+  shows   "convergent (\<lambda>n. c * f n :: 'a :: real_normed_field) \<longleftrightarrow> convergent f"
+proof
+  assume "convergent (\<lambda>n. c * f n)"
+  from assms convergent_mult[OF this convergent_const[of "inverse c"]] 
+    show "convergent f" by (simp add: field_simps)
+next
+  assume "convergent f"
+  from convergent_mult[OF convergent_const[of c] this] show "convergent (\<lambda>n. c * f n)" by simp
+qed
+
+lemma convergent_mult_const_right_iff:
+  assumes "c \<noteq> 0"
+  shows   "convergent (\<lambda>n. (f n :: 'a :: real_normed_field) * c) \<longleftrightarrow> convergent f"
+  using convergent_mult_const_iff[OF assms, of f] by (simp add: mult_ac)
+
+lemma convergent_imp_Bseq: "convergent f \<Longrightarrow> Bseq f"
+  by (simp add: Cauchy_Bseq convergent_Cauchy)
+
 
 text \<open>A monotone sequence converges to its least upper bound.\<close>
 
@@ -1532,6 +1780,19 @@
 lemma Bseq_mono_convergent: "Bseq X \<Longrightarrow> (\<forall>m n. m \<le> n \<longrightarrow> X m \<le> X n) \<Longrightarrow> convergent (X::nat\<Rightarrow>real)"
   by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def)
 
+lemma monoseq_imp_convergent_iff_Bseq: "monoseq (f :: nat \<Rightarrow> real) \<Longrightarrow> convergent f \<longleftrightarrow> Bseq f"
+  using Bseq_monoseq_convergent[of f] convergent_imp_Bseq[of f] by blast
+
+lemma Bseq_monoseq_convergent'_inc:
+  "Bseq (\<lambda>n. f (n + M) :: real) \<Longrightarrow> (\<And>m n. M \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m \<le> f n) \<Longrightarrow> convergent f"
+  by (subst convergent_ignore_initial_segment [symmetric, of _ M])
+     (auto intro!: Bseq_monoseq_convergent simp: monoseq_def)
+
+lemma Bseq_monoseq_convergent'_dec:
+  "Bseq (\<lambda>n. f (n + M) :: real) \<Longrightarrow> (\<And>m n. M \<le> m \<Longrightarrow> m \<le> n \<Longrightarrow> f m \<ge> f n) \<Longrightarrow> convergent f"
+  by (subst convergent_ignore_initial_segment [symmetric, of _ M])
+     (auto intro!: Bseq_monoseq_convergent simp: monoseq_def)
+
 lemma Cauchy_iff:
   fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -819,6 +819,7 @@
 
 subsection\<open>Complex differentiation of sequences and series\<close>
 
+(* TODO: Could probably be simplified using Uniform_Limit *)
 lemma has_complex_derivative_sequence:
   fixes s :: "complex set"
   assumes cvs: "convex s"
@@ -899,6 +900,41 @@
   qed
 qed
 
+
+lemma complex_differentiable_series:
+  fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+  assumes "convex s" "open s"
+  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
+  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
+  shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)"
+proof -
+  from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+    unfolding uniformly_convergent_on_def by blast
+  from x and `open s` have s: "at x within s = at x" by (rule at_within_open)
+  have "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
+    by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
+  then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
+    "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
+  from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
+  from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
+    by (simp add: has_field_derivative_def s)
+  have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
+    by (rule has_derivative_transform_within_open[OF `open s` x _ g'])
+       (insert g, auto simp: sums_iff)
+  thus "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)" unfolding differentiable_def
+    by (auto simp: summable_def complex_differentiable_def has_field_derivative_def)
+qed
+
+lemma complex_differentiable_series':
+  fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
+  assumes "convex s" "open s"
+  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
+  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
+  shows   "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x0)"
+  using complex_differentiable_series[OF assms, of x0] `x0 \<in> s` by blast+
+
 subsection\<open>Bound theorem\<close>
 
 lemma complex_differentiable_bound:
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -1788,14 +1788,6 @@
 
 subsubsection \<open>Another formulation from Lars Schewe\<close>
 
-lemma setsum_constant_scaleR:
-  fixes y :: "'a::real_vector"
-  shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
-  apply (cases "finite A")
-  apply (induct set: finite)
-  apply (simp_all add: algebra_simps)
-  done
-
 lemma convex_hull_explicit:
   fixes p :: "'a::real_vector set"
   shows "convex hull p =
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Multivariate_Analysis/Derivative.thy
--- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -6,7 +6,7 @@
 section \<open>Multivariate calculus in Euclidean space\<close>
 
 theory Derivative
-imports Brouwer_Fixpoint Operator_Norm
+imports Brouwer_Fixpoint Operator_Norm "~~/src/HOL/Multivariate_Analysis/Uniform_Limit"
 begin
 
 lemma netlimit_at_vector: (* TODO: move *)
@@ -2202,6 +2202,92 @@
   apply auto
   done
 
+lemma has_field_derivative_series:
+  fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
+  assumes "convex s"
+  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
+  assumes "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
+  shows   "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
+unfolding has_field_derivative_def
+proof (rule has_derivative_series)
+  show "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h"
+  proof (intro allI impI)
+    fix e :: real assume "e > 0"
+    with assms(3) obtain N where N: "\<And>n x. n \<ge> N \<Longrightarrow> x \<in> s \<Longrightarrow> norm ((\<Sum>i<n. f' i x) - g' x) < e"
+      unfolding uniform_limit_iff eventually_at_top_linorder dist_norm by blast
+    {
+      fix n :: nat and x h :: 'a assume nx: "n \<ge> N" "x \<in> s"
+      have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) = norm ((\<Sum>i<n. f' i x) - g' x) * norm h"
+        by (simp add: norm_mult [symmetric] ring_distribs setsum_left_distrib)
+      also from N[OF nx] have "norm ((\<Sum>i<n. f' i x) - g' x) \<le> e" by simp
+      hence "norm ((\<Sum>i<n. f' i x) - g' x) * norm h \<le> e * norm h" 
+        by (intro mult_right_mono) simp_all
+      finally have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" .
+    }
+    thus "\<exists>N. \<forall>n\<ge>N. \<forall>x\<in>s. \<forall>h. norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" by blast
+  qed
+qed (insert assms, auto simp: has_field_derivative_def)
+
+lemma has_field_derivative_series':
+  fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
+  assumes "convex s"
+  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
+  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
+  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" "x \<in> interior s"
+  shows   "summable (\<lambda>n. f n x)" "((\<lambda>x. \<Sum>n. f n x) has_field_derivative (\<Sum>n. f' n x)) (at x)"
+proof -
+  from \<open>x \<in> interior s\<close> have "x \<in> s" using interior_subset by blast
+  def g' \<equiv> "\<lambda>x. \<Sum>i. f' i x"
+  from assms(3) have "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+    by (simp add: uniformly_convergent_uniform_limit_iff suminf_eq_lim g'_def)
+  from has_field_derivative_series[OF assms(1,2) this assms(4,5)] obtain g where g:
+    "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
+    "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
+  from g(1)[OF \<open>x \<in> s\<close>] show "summable (\<lambda>n. f n x)" by (simp add: sums_iff)
+  from g(2)[OF \<open>x \<in> s\<close>] \<open>x \<in> interior s\<close> have "(g has_field_derivative g' x) (at x)" 
+    by (simp add: at_within_interior[of x s])
+  also have "(g has_field_derivative g' x) (at x) \<longleftrightarrow> 
+                ((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)"
+    using eventually_nhds_in_nhd[OF \<open>x \<in> interior s\<close>] interior_subset[of s] g(1)
+    by (intro DERIV_cong_ev) (auto elim!: eventually_elim1 simp: sums_iff)
+  finally show "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)" .
+qed
+
+lemma differentiable_series:
+  fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
+  assumes "convex s" "open s"
+  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
+  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
+  shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)"
+proof -
+  from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
+    unfolding uniformly_convergent_on_def by blast
+  from x and `open s` have s: "at x within s = at x" by (rule at_within_open)
+  have "\<exists>g. \<forall>x\<in>s. (\<lambda>n. f n x) sums g x \<and> (g has_field_derivative g' x) (at x within s)"
+    by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
+  then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
+    "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
+  from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
+  from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
+    by (simp add: has_field_derivative_def s)
+  have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
+    by (rule has_derivative_transform_within_open[OF `open s` x _ g'])
+       (insert g, auto simp: sums_iff)
+  thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
+    by (auto simp: summable_def differentiable_def has_field_derivative_def)
+qed
+
+lemma differentiable_series':
+  fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
+  assumes "convex s" "open s"
+  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
+  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
+  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
+  shows   "(\<lambda>x. \<Sum>n. f n x) differentiable (at x0)"
+  using differentiable_series[OF assms, of x0] `x0 \<in> s` by blast+
+
 text \<open>Considering derivative @{typ "real \<Rightarrow> 'b::real_normed_vector"} as a vector.\<close>
 
 definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
@@ -2445,4 +2531,61 @@
          vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"
 by (metis vector_diff_chain_at vector_derivative_at vector_derivative_works assms)
 
+
+subsection \<open>Relation between convexity and derivative\<close>
+
+(* TODO: Generalise to real vector spaces? *)
+lemma convex_on_imp_above_tangent:
+  assumes convex: "convex_on A f" and connected: "connected A"
+  assumes c: "c \<in> interior A" and x : "x \<in> A"
+  assumes deriv: "(f has_field_derivative f') (at c within A)"
+  shows   "f x - f c \<ge> f' * (x - c)"
+proof (cases x c rule: linorder_cases)
+  assume xc: "x > c"
+  let ?A' = "interior A \<inter> {c<..}"
+  from c have "c \<in> interior A \<inter> closure {c<..}" by auto
+  also have "\<dots> \<subseteq> closure (interior A \<inter> {c<..})" by (intro open_inter_closure_subset) auto
+  finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
+  moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) ---> f') (at c within ?A')"
+    unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
+  moreover from eventually_at_right_real[OF xc]
+    have "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at_right c)"
+  proof eventually_elim
+    fix y assume y: "y \<in> {c<..<x}"
+    with convex connected x c have "f y \<le> (f x - f c) / (x - c) * (y - c) + f c"
+      using interior_subset[of A]
+      by (intro convex_onD_Icc' convex_on_subset[OF convex] connected_contains_Icc) auto
+    hence "f y - f c \<le> (f x - f c) / (x - c) * (y - c)" by simp
+    thus "(f y - f c) / (y - c) \<le> (f x - f c) / (x - c)" using y xc by (simp add: divide_simps)
+  qed
+  hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at c within ?A')"
+    by (blast intro: filter_leD at_le)
+  ultimately have "f' \<le> (f x - f c) / (x - c)" by (rule tendsto_ge_const)
+  thus ?thesis using xc by (simp add: field_simps)
+next
+  assume xc: "x < c"
+  let ?A' = "interior A \<inter> {..<c}"
+  from c have "c \<in> interior A \<inter> closure {..<c}" by auto
+  also have "\<dots> \<subseteq> closure (interior A \<inter> {..<c})" by (intro open_inter_closure_subset) auto
+  finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
+  moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) ---> f') (at c within ?A')"
+    unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
+  moreover from eventually_at_left_real[OF xc]
+    have "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at_left c)"
+  proof eventually_elim
+    fix y assume y: "y \<in> {x<..<c}"
+    with convex connected x c have "f y \<le> (f x - f c) / (c - x) * (c - y) + f c"
+      using interior_subset[of A]
+      by (intro convex_onD_Icc'' convex_on_subset[OF convex] connected_contains_Icc) auto
+    hence "f y - f c \<le> (f x - f c) * ((c - y) / (c - x))" by simp
+    also have "(c - y) / (c - x) = (y - c) / (x - c)" using y xc by (simp add: field_simps)
+    finally show "(f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)" using y xc 
+      by (simp add: divide_simps)
+  qed
+  hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at c within ?A')"
+    by (blast intro: filter_leD at_le)
+  ultimately have "f' \<ge> (f x - f c) / (x - c)" by (rule tendsto_le_const)
+  thus ?thesis using xc by (simp add: field_simps)
+qed simp_all
+
 end
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -896,6 +896,15 @@
   unfolding dist_norm norm_eq_sqrt_inner setL2_def
   by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
 
+lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
+  by (rule eventually_nhds_in_open) simp_all
+
+lemma eventually_at_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<in> A) (at z within A)"
+  unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
+
+lemma eventually_at_ball': "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<noteq> z \<and> t \<in> A) (at z within A)"
+  unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
+
 
 subsection \<open>Boxes\<close>
 
@@ -1582,6 +1591,9 @@
   using open_contains_ball_eq [where S="interior S"]
   by (simp add: open_subset_interior)
 
+lemma eventually_nhds_in_nhd: "x \<in> interior s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
+  using interior_subset[of s] by (subst eventually_nhds) blast
+
 lemma interior_limit_point [intro]:
   fixes x :: "'a::perfect_space"
   assumes x: "x \<in> interior S"
@@ -1832,6 +1844,7 @@
     "closed s \<Longrightarrow> (closedin (subtopology euclidean s) t \<longleftrightarrow> closed t \<and> t \<subseteq> s)"
   by (meson closed_in_limpt closed_subset closedin_closed_trans)
 
+
 subsection\<open>Connected components, considered as a connectedness relation or a set\<close>
 
 definition
@@ -2258,6 +2271,9 @@
   using islimpt_in_closure
   by (metis trivial_limit_within)
 
+lemma at_within_eq_bot_iff: "(at c within A = bot) \<longleftrightarrow> (c \<notin> closure (A - {c}))"
+  using not_trivial_limit_within[of c A] by blast
+
 text \<open>Some property holds "sufficiently close" to the limit point.\<close>
 
 lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Multivariate_Analysis/Uniform_Limit.thy
--- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -15,6 +15,12 @@
 abbreviation
   "uniform_limit S f l \<equiv> filterlim f (uniformly_on S l)"
 
+definition uniformly_convergent_on where
+  "uniformly_convergent_on X f \<longleftrightarrow> (\<exists>l. uniform_limit X f l sequentially)"
+
+definition uniformly_Cauchy_on where 
+  "uniformly_Cauchy_on X f \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>x\<in>X. \<forall>(m::nat)\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e)"
+  
 lemma uniform_limit_iff:
   "uniform_limit S f l F \<longleftrightarrow> (\<forall>e>0. \<forall>\<^sub>F n in F. \<forall>x\<in>S. dist (f n x) (l x) < e)"
   unfolding filterlim_iff uniformly_on_def
@@ -114,9 +120,115 @@
     by (rule swap_uniform_limit) fact+
 qed
 
-lemma weierstrass_m_test:
+lemma uniformly_Cauchy_onI:
+  assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e"
+  shows   "uniformly_Cauchy_on X f"
+  using assms unfolding uniformly_Cauchy_on_def by blast
+
+lemma uniformly_Cauchy_onI':
+  assumes "\<And>e. e > 0 \<Longrightarrow> \<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n>m. dist (f m x) (f n x) < e"
+  shows   "uniformly_Cauchy_on X f"
+proof (rule uniformly_Cauchy_onI)
+  fix e :: real assume e: "e > 0"
+  from assms[OF this] obtain M 
+    where M: "\<And>x m n. x \<in> X \<Longrightarrow> m \<ge> M \<Longrightarrow> n > m \<Longrightarrow> dist (f m x) (f n x) < e" by fast
+  {
+    fix x m n assume x: "x \<in> X" and m: "m \<ge> M" and n: "n \<ge> M"
+    with M[OF this(1,2), of n] M[OF this(1,3), of m] e have "dist (f m x) (f n x) < e"
+      by (cases m n rule: linorder_cases) (simp_all add: dist_commute)
+  }
+  thus "\<exists>M. \<forall>x\<in>X. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m x) (f n x) < e" by fast
+qed
+
+lemma uniformly_Cauchy_imp_Cauchy: 
+  "uniformly_Cauchy_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> Cauchy (\<lambda>n. f n x)"
+  unfolding Cauchy_def uniformly_Cauchy_on_def by fast
+
+lemma uniform_limit_cong:
+  fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ('c :: metric_space)" and h i :: "'b \<Rightarrow> 'c"
+  assumes "eventually (\<lambda>y. \<forall>x\<in>X. f y x = g y x) F"
+  assumes "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
+  shows   "uniform_limit X f h F \<longleftrightarrow> uniform_limit X g i F"
+proof -
+  {
+    fix f g :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" and h i :: "'b \<Rightarrow> 'c"
+    assume C: "uniform_limit X f h F" and A: "eventually (\<lambda>y. \<forall>x\<in>X. f y x = g y x) F"
+       and B: "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
+    {
+      fix e ::real assume "e > 0"
+      with C have "eventually (\<lambda>y. \<forall>x\<in>X. dist (f y x) (h x) < e) F" 
+        unfolding uniform_limit_iff by blast
+      with A have "eventually (\<lambda>y. \<forall>x\<in>X. dist (g y x) (i x) < e) F"
+        by eventually_elim (insert B, simp_all)
+    }
+    hence "uniform_limit X g i F" unfolding uniform_limit_iff by blast
+  } note A = this
+  show ?thesis by (rule iffI) (erule A; insert assms; simp add: eq_commute)+
+qed
+
+lemma uniform_limit_cong':
+  fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ('c :: metric_space)" and h i :: "'b \<Rightarrow> 'c"
+  assumes "\<And>y x. x \<in> X \<Longrightarrow> f y x = g y x"
+  assumes "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
+  shows   "uniform_limit X f h F \<longleftrightarrow> uniform_limit X g i F"
+  using assms by (intro uniform_limit_cong always_eventually) blast+
+
+lemma uniformly_convergent_uniform_limit_iff:
+  "uniformly_convergent_on X f \<longleftrightarrow> uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially"
+proof
+  assume "uniformly_convergent_on X f"
+  then obtain l where l: "uniform_limit X f l sequentially" 
+    unfolding uniformly_convergent_on_def by blast
+  from l have "uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially \<longleftrightarrow>
+                      uniform_limit X f l sequentially"
+    by (intro uniform_limit_cong' limI tendsto_uniform_limitI[of f X l]) simp_all
+  also note l
+  finally show "uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially" .
+qed (auto simp: uniformly_convergent_on_def)
+
+lemma uniformly_convergentI: "uniform_limit X f l sequentially \<Longrightarrow> uniformly_convergent_on X f"
+  unfolding uniformly_convergent_on_def by blast
+
+lemma Cauchy_uniformly_convergent:
+  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: complete_space"
+  assumes "uniformly_Cauchy_on X f"
+  shows   "uniformly_convergent_on X f"
+unfolding uniformly_convergent_uniform_limit_iff uniform_limit_iff
+proof safe
+  let ?f = "\<lambda>x. lim (\<lambda>n. f n x)"
+  fix e :: real assume e: "e > 0"
+  hence "e/2 > 0" by simp
+  with assms obtain N where N: "\<And>x m n. x \<in> X \<Longrightarrow> m \<ge> N \<Longrightarrow> n \<ge> N \<Longrightarrow> dist (f m x) (f n x) < e/2"
+    unfolding uniformly_Cauchy_on_def by fast
+  show "eventually (\<lambda>n. \<forall>x\<in>X. dist (f n x) (?f x) < e) sequentially"
+    using eventually_ge_at_top[of N]
+  proof eventually_elim
+    fix n assume n: "n \<ge> N"
+    show "\<forall>x\<in>X. dist (f n x) (?f x) < e"
+    proof
+      fix x assume x: "x \<in> X"
+      with assms have "(\<lambda>n. f n x) ----> ?f x" 
+        by (auto dest!: Cauchy_convergent uniformly_Cauchy_imp_Cauchy simp: convergent_LIMSEQ_iff)
+      with `e/2 > 0` have "eventually (\<lambda>m. m \<ge> N \<and> dist (f m x) (?f x) < e/2) sequentially"
+        by (intro tendstoD eventually_conj eventually_ge_at_top)
+      then obtain m where m: "m \<ge> N" "dist (f m x) (?f x) < e/2" 
+        unfolding eventually_at_top_linorder by blast
+      have "dist (f n x) (?f x) \<le> dist (f n x) (f m x) + dist (f m x) (?f x)"
+          by (rule dist_triangle)
+      also from x n have "... < e/2 + e/2" by (intro add_strict_mono N m)
+      finally show "dist (f n x) (?f x) < e" by simp
+    qed
+  qed
+qed
+
+lemma uniformly_convergent_imp_convergent:
+  "uniformly_convergent_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> convergent (\<lambda>n. f n x)"
+  unfolding uniformly_convergent_on_def convergent_def
+  by (auto dest: tendsto_uniform_limitI)
+
+lemma weierstrass_m_test_ev:
 fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
-assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
+assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially"
 assumes "summable M"
 shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
 proof (rule uniform_limitI)
@@ -125,14 +237,15 @@
   from suminf_exist_split[OF \<open>0 < e\<close> \<open>summable M\<close>]
   have "\<forall>\<^sub>F k in sequentially. norm (\<Sum>i. M (i + k)) < e"
     by (auto simp: eventually_sequentially)
-  thus "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. dist (\<Sum>i<n. f i x) (\<Sum>i. f i x) < e"
+  with eventually_all_ge_at_top[OF assms(1)]
+    show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. dist (\<Sum>i<n. f i x) (\<Sum>i. f i x) < e"
   proof eventually_elim
     case (elim k)
     show ?case
     proof safe
       fix x assume "x \<in> A"
       have "\<exists>N. \<forall>n\<ge>N. norm (f n x) \<le> M n"
-        using assms(1)[OF \<open>x \<in> A\<close>] by simp
+        using assms(1) \<open>x \<in> A\<close> by (force simp: eventually_at_top_linorder)
       hence summable_norm_f: "summable (\<lambda>n. norm (f n x))"
         by(rule summable_norm_comparison_test[OF _ \<open>summable M\<close>])
       have summable_f: "summable (\<lambda>n. f n x)"
@@ -152,13 +265,32 @@
         using summable_norm[OF summable_norm_f_plus_k] .
       also have "... \<le> (\<Sum>i. M (i + k))"
         by (rule suminf_le[OF _ summable_norm_f_plus_k summable_M_plus_k])
-           (simp add: assms(1)[OF \<open>x \<in> A\<close>])
+           (insert elim(1) \<open>x \<in> A\<close>, simp)
       finally show "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) < e"
         using elim by auto
     qed
   qed
 qed
 
+lemma weierstrass_m_test:
+fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
+assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
+assumes "summable M"
+shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
+  using assms by (intro weierstrass_m_test_ev always_eventually) auto
+  
+lemma weierstrass_m_test'_ev:
+  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
+  assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially" "summable M" 
+  shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
+  unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test_ev[OF assms])
+
+lemma weierstrass_m_test':
+  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
+  assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n" "summable M" 
+  shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
+  unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test[OF assms])
+
 lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
   by simp
 
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Nat.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -1472,6 +1472,9 @@
 lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
   by (induct m) (simp_all add: ac_simps distrib_right)
 
+lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"
+  by (induction x) (simp_all add: algebra_simps)
+
 primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   "of_nat_aux inc 0 i = i"
 | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- \<open>tail recursive\<close>
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Parity.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -233,7 +233,7 @@
 
 subsection \<open>Parity and powers\<close>
 
-context comm_ring_1
+context ring_1
 begin
 
 lemma power_minus_even [simp]:
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Power.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -283,6 +283,9 @@
     by (simp del: power_Suc add: power_Suc2 mult.assoc)
 qed
 
+lemma power_minus': "NO_MATCH 1 x \<Longrightarrow> (-x) ^ n = (-1)^n * x ^ n"
+  by (rule power_minus)
+
 lemma power_minus_Bit0:
   "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)"
   by (induct k, simp_all only: numeral_class.numeral.simps power_add
@@ -307,7 +310,7 @@
 lemma power_minus1_odd:
   "(- 1) ^ Suc (2*n) = -1"
   by simp
-
+  
 lemma power_minus_even [simp]:
   "(-a) ^ (2*n) = a ^ (2*n)"
   by (simp add: power_minus [of a])
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -228,6 +228,14 @@
 apply (erule (1) nonzero_inverse_scaleR_distrib)
 done
 
+lemma setsum_constant_scaleR:
+  fixes y :: "'a::real_vector"
+  shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
+  apply (cases "finite A")
+  apply (induct set: finite)
+  apply (simp_all add: algebra_simps)
+  done
+
 lemma real_vector_affinity_eq:
   fixes x :: "'a :: real_vector"
   assumes m0: "m \<noteq> 0"
@@ -1614,6 +1622,12 @@
   apply auto
   done
 
+lemma eventually_at_left_real: "a > (b :: real) \<Longrightarrow> eventually (\<lambda>x. x \<in> {b<..<a}) (at_left a)"
+  by (subst eventually_at, rule exI[of _ "a - b"]) (force simp: dist_real_def)
+
+lemma eventually_at_right_real: "a < (b :: real) \<Longrightarrow> eventually (\<lambda>x. x \<in> {a<..<b}) (at_right a)"
+  by (subst eventually_at, rule exI[of _ "b - a"]) (force simp: dist_real_def)
+
 lemma metric_tendsto_imp_tendsto:
   fixes a :: "'a :: metric_space" and b :: "'b :: metric_space"
   assumes f: "(f ---> a) F"
@@ -1709,12 +1723,36 @@
 definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
 
-subsection \<open>Cauchy Sequences\<close>
+lemma Cauchy_altdef:
+  "Cauchy f = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e)"
+proof
+  assume A: "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
+  show "Cauchy f" unfolding Cauchy_def
+  proof (intro allI impI)
+    fix e :: real assume e: "e > 0"
+    with A obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n > m \<Longrightarrow> dist (f m) (f n) < e" by blast
+    have "dist (f m) (f n) < e" if "m \<ge> M" "n \<ge> M" for m n
+      using M[of m n] M[of n m] e that by (cases m n rule: linorder_cases) (auto simp: dist_commute)
+    thus "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m) (f n) < e" by blast
+  qed
+next
+  assume "Cauchy f"
+  show "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e" 
+  proof (intro allI impI)
+    fix e :: real assume e: "e > 0"
+    with `Cauchy f` obtain M where "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (f m) (f n) < e"
+      unfolding Cauchy_def by fast
+    thus "\<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e" by (intro exI[of _ M]) force
+  qed
+qed
 
 lemma metric_CauchyI:
   "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
   by (simp add: Cauchy_def)
 
+lemma CauchyI': "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
+  unfolding Cauchy_altdef by blast
+
 lemma metric_CauchyD:
   "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
   by (simp add: Cauchy_def)
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Series.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -35,12 +35,20 @@
 lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
   by simp
 
+lemma sums_cong: "(\<And>n. f n = g n) \<Longrightarrow> f sums c \<longleftrightarrow> g sums c"
+  by (drule ext) simp
+
 lemma sums_summable: "f sums l \<Longrightarrow> summable f"
   by (simp add: sums_def summable_def, blast)
 
 lemma summable_iff_convergent: "summable f \<longleftrightarrow> convergent (\<lambda>n. \<Sum>i<n. f i)"
   by (simp add: summable_def sums_def convergent_def)
 
+lemma summable_iff_convergent':
+  "summable f \<longleftrightarrow> convergent (\<lambda>n. setsum f {..n})"
+  by (simp_all only: summable_iff_convergent convergent_def 
+        lessThan_Suc_atMost [symmetric] LIMSEQ_Suc_iff[of "\<lambda>n. setsum f {..<n}"])
+
 lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)"
   by (simp add: suminf_def sums_def lim_def)
 
@@ -62,6 +70,34 @@
   apply simp
   done
 
+lemma suminf_cong: "(\<And>n. f n = g n) \<Longrightarrow> suminf f = suminf g"
+  by (rule arg_cong[of f g], rule ext) simp
+
+lemma summable_cong:
+  assumes "eventually (\<lambda>x. f x = (g x :: 'a :: real_normed_vector)) sequentially"
+  shows   "summable f = summable g"
+proof -
+  from assms obtain N where N: "\<forall>n\<ge>N. f n = g n" by (auto simp: eventually_at_top_linorder)
+  def C \<equiv> "(\<Sum>k<N. f k - g k)"
+  from eventually_ge_at_top[of N] 
+    have "eventually (\<lambda>n. setsum f {..<n} = C + setsum g {..<n}) sequentially"
+  proof eventually_elim
+    fix n assume n: "n \<ge> N"
+    from n have "{..<n} = {..<N} \<union> {N..<n}" by auto
+    also have "setsum f ... = setsum f {..<N} + setsum f {N..<n}"
+      by (intro setsum.union_disjoint) auto
+    also from N have "setsum f {N..<n} = setsum g {N..<n}" by (intro setsum.cong) simp_all
+    also have "setsum f {..<N} + setsum g {N..<n} = C + (setsum g {..<N} + setsum g {N..<n})" 
+      unfolding C_def by (simp add: algebra_simps setsum_subtractf)
+    also have "setsum g {..<N} + setsum g {N..<n} = setsum g ({..<N} \<union> {N..<n})"
+      by (intro setsum.union_disjoint [symmetric]) auto
+    also from n have "{..<N} \<union> {N..<n} = {..<n}" by auto
+    finally show "setsum f {..<n} = C + setsum g {..<n}" .
+  qed
+  from convergent_cong[OF this] show ?thesis
+    by (simp add: summable_iff_convergent convergent_add_const_iff)
+qed
+
 lemma sums_finite:
   assumes [simp]: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
   shows "f sums (\<Sum>n\<in>N. f n)"
@@ -125,6 +161,10 @@
 lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
   by (metis summable_sums sums_summable sums_unique)
 
+lemma summable_sums_iff: 
+  "summable (f :: nat \<Rightarrow> 'a :: {comm_monoid_add,t2_space}) \<longleftrightarrow> f sums suminf f"
+  by (auto simp: sums_iff summable_sums)
+
 lemma sums_unique2:
   fixes a b :: "'a::{comm_monoid_add,t2_space}"
   shows "f sums a \<Longrightarrow> f sums b \<Longrightarrow> a = b"
@@ -221,6 +261,7 @@
       by (auto intro: le_less_trans simp: eventually_sequentially) }
 qed
 
+
 subsection \<open>Infinite summability on real normed vector spaces\<close>
 
 lemma sums_Suc_iff:
@@ -241,6 +282,14 @@
   finally show ?thesis ..
 qed
 
+lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n) :: 'a :: real_normed_vector) = summable f"
+proof
+  assume "summable f"
+  hence "f sums suminf f" by (rule summable_sums)
+  hence "(\<lambda>n. f (Suc n)) sums (suminf f - f 0)" by (simp add: sums_Suc_iff)
+  thus "summable (\<lambda>n. f (Suc n))" unfolding summable_def by blast
+qed (auto simp: sums_Suc_iff summable_def)
+
 context
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
 begin
@@ -299,6 +348,9 @@
 lemma suminf_split_initial_segment: "summable f \<Longrightarrow> suminf f = (\<Sum>n. f(n + k)) + (\<Sum>i<k. f i)"
   by (auto simp add: suminf_minus_initial_segment)
 
+lemma suminf_split_head: "summable f \<Longrightarrow> (\<Sum>n. f (Suc n)) = suminf f - f 0"
+  using suminf_split_initial_segment[of 1] by simp
+
 lemma suminf_exist_split: 
   fixes r :: real assumes "0 < r" and "summable f"
   shows "\<exists>N. \<forall>n\<ge>N. norm (\<Sum>i. f (i + n)) < r"
@@ -319,6 +371,14 @@
   apply (drule_tac x="n" in spec, simp)
   done
 
+lemma summable_imp_convergent:
+  "summable (f :: nat \<Rightarrow> 'a) \<Longrightarrow> convergent f"
+  by (force dest!: summable_LIMSEQ_zero simp: convergent_def)
+
+lemma summable_imp_Bseq:
+  "summable f \<Longrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
+  by (simp add: convergent_imp_Bseq summable_imp_convergent)
+
 end
 
 lemma summable_minus_iff:
@@ -363,6 +423,23 @@
 lemmas summable_scaleR_right = bounded_linear.summable[OF bounded_linear_scaleR_right]
 lemmas suminf_scaleR_right = bounded_linear.suminf[OF bounded_linear_scaleR_right]
 
+lemma summable_const_iff: "summable (\<lambda>_. c) \<longleftrightarrow> (c :: 'a :: real_normed_vector) = 0"
+proof -
+  {
+    assume "c \<noteq> 0"
+    hence "filterlim (\<lambda>n. of_nat n * norm c) at_top sequentially"
+      unfolding real_of_nat_def[symmetric]
+      by (subst mult.commute)
+         (auto intro!: filterlim_tendsto_pos_mult_at_top filterlim_real_sequentially)
+    hence "\<not>convergent (\<lambda>n. norm (\<Sum>k<n. c))"
+      by (intro filterlim_at_infinity_imp_not_convergent filterlim_at_top_imp_at_infinity) 
+         (simp_all add: setsum_constant_scaleR)
+    hence "\<not>summable (\<lambda>_. c)" unfolding summable_iff_convergent using convergent_norm by blast
+  }
+  thus ?thesis by auto
+qed
+
+
 subsection \<open>Infinite summability on real normed algebras\<close>
 
 context
@@ -389,6 +466,22 @@
 
 end
 
+lemma sums_mult_iff:
+  assumes "c \<noteq> 0"
+  shows   "(\<lambda>n. c * f n :: 'a :: {real_normed_algebra,field}) sums (c * d) \<longleftrightarrow> f sums d"
+  using sums_mult[of f d c] sums_mult[of "\<lambda>n. c * f n" "c * d" "inverse c"]
+  by (force simp: field_simps assms)
+
+lemma sums_mult2_iff:
+  assumes "c \<noteq> (0 :: 'a :: {real_normed_algebra, field})"
+  shows   "(\<lambda>n. f n * c) sums (d * c) \<longleftrightarrow> f sums d"
+  using sums_mult_iff[OF assms, of f d] by (simp add: mult.commute)
+
+lemma sums_of_real_iff:
+  "(\<lambda>n. of_real (f n) :: 'a :: real_normed_div_algebra) sums of_real c \<longleftrightarrow> f sums c"
+  by (simp add: sums_def of_real_setsum[symmetric] tendsto_of_real_iff del: of_real_setsum)
+
+
 subsection \<open>Infinite summability on real normed fields\<close>
 
 context
@@ -427,6 +520,16 @@
 lemma suminf_geometric: "norm c < 1 \<Longrightarrow> suminf (\<lambda>n. c^n) = 1 / (1 - c)"
   by (rule sums_unique[symmetric]) (rule geometric_sums)
 
+lemma summable_geometric_iff: "summable (\<lambda>n. c ^ n) \<longleftrightarrow> norm c < 1"
+proof
+  assume "summable (\<lambda>n. c ^ n :: 'a :: real_normed_field)"
+  hence "(\<lambda>n. norm c ^ n) ----> 0"
+    by (simp add: norm_power [symmetric] tendsto_norm_zero_iff summable_LIMSEQ_zero)
+  from order_tendstoD(2)[OF this zero_less_one] obtain n where "norm c ^ n < 1"
+    by (auto simp: eventually_at_top_linorder)
+  thus "norm c < 1" using one_le_power[of "norm c" n] by (cases "norm c \<ge> 1") (linarith, simp)
+qed (rule summable_geometric)
+  
 end
 
 lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
@@ -439,6 +542,36 @@
     by simp
 qed
 
+
+subsection \<open>Telescoping\<close>
+
+lemma telescope_sums:
+  assumes "f ----> (c :: 'a :: real_normed_vector)"
+  shows   "(\<lambda>n. f (Suc n) - f n) sums (c - f 0)"
+  unfolding sums_def
+proof (subst LIMSEQ_Suc_iff [symmetric])
+  have "(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)"
+    by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setsum_Suc_diff)
+  also have "\<dots> ----> c - f 0" by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const)
+  finally show "(\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) ----> c - f 0" .
+qed
+
+lemma telescope_sums':
+  assumes "f ----> (c :: 'a :: real_normed_vector)"
+  shows   "(\<lambda>n. f n - f (Suc n)) sums (f 0 - c)"
+  using sums_minus[OF telescope_sums[OF assms]] by (simp add: algebra_simps)
+
+lemma telescope_summable:
+  assumes "f ----> (c :: 'a :: real_normed_vector)"
+  shows   "summable (\<lambda>n. f (Suc n) - f n)"
+  using telescope_sums[OF assms] by (simp add: sums_iff)
+
+lemma telescope_summable':
+  assumes "f ----> (c :: 'a :: real_normed_vector)"
+  shows   "summable (\<lambda>n. f n - f (Suc n))"
+  using summable_minus[OF telescope_summable[OF assms]] by (simp add: algebra_simps)
+
+
 subsection \<open>Infinite summability on Banach spaces\<close>
 
 text\<open>Cauchy-type criterion for convergence of series (c.f. Harrison)\<close>
@@ -463,7 +596,7 @@
 
 context
   fixes f :: "nat \<Rightarrow> 'a::banach"
-begin  
+begin
 
 text\<open>Absolute convergence imples normal convergence\<close>
 
@@ -495,6 +628,10 @@
   apply (auto intro: setsum_mono simp add: abs_less_iff)
   done
 
+lemma summable_comparison_test_ev:
+  shows "eventually (\<lambda>n. norm (f n) \<le> g n) sequentially \<Longrightarrow> summable g \<Longrightarrow> summable f"
+  by (rule summable_comparison_test) (auto simp: eventually_at_top_linorder)
+
 (*A better argument order*)
 lemma summable_comparison_test': "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
   by (rule summable_comparison_test) auto
@@ -669,6 +806,21 @@
 lemma summable_rabs: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
   by (fold real_norm_def) (rule summable_norm)
 
+lemma summable_zero_power [simp]: "summable (\<lambda>n. 0 ^ n :: 'a :: {comm_ring_1,topological_space})"
+proof -
+  have "(\<lambda>n. 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then 0^0 else 0)" by (intro ext) (simp add: zero_power)
+  moreover have "summable \<dots>" by simp
+  ultimately show ?thesis by simp
+qed
+
+lemma summable_zero_power' [simp]: "summable (\<lambda>n. f n * 0 ^ n :: 'a :: {ring_1,topological_space})"
+proof -
+  have "(\<lambda>n. f n * 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then f 0 * 0^0 else 0)" 
+    by (intro ext) (simp add: zero_power)
+  moreover have "summable \<dots>" by simp
+  ultimately show ?thesis by simp
+qed
+
 lemma summable_power_series:
   fixes z :: real
   assumes le_1: "\<And>i. f i \<le> 1" and nonneg: "\<And>i. 0 \<le> f i" and z: "0 \<le> z" "z < 1"
@@ -679,6 +831,79 @@
     using z by (auto intro!: exI[of _ 0] mult_left_le_one_le simp: abs_mult nonneg power_abs less_imp_le le_1)
 qed
 
+lemma summable_0_powser:
+  "summable (\<lambda>n. f n * 0 ^ n :: 'a :: real_normed_div_algebra)"
+proof -
+  have A: "(\<lambda>n. f n * 0 ^ n) = (\<lambda>n. if n = 0 then f n else 0)"
+    by (intro ext) auto
+  thus ?thesis by (subst A) simp_all
+qed
+
+lemma summable_powser_split_head:
+  "summable (\<lambda>n. f (Suc n) * z ^ n :: 'a :: real_normed_div_algebra) = summable (\<lambda>n. f n * z ^ n)"
+proof -
+  have "summable (\<lambda>n. f (Suc n) * z ^ n) \<longleftrightarrow> summable (\<lambda>n. f (Suc n) * z ^ Suc n)"
+  proof
+    assume "summable (\<lambda>n. f (Suc n) * z ^ n)"
+    from summable_mult2[OF this, of z] show "summable (\<lambda>n. f (Suc n) * z ^ Suc n)" 
+      by (simp add: power_commutes algebra_simps)
+  next
+    assume "summable (\<lambda>n. f (Suc n) * z ^ Suc n)"
+    from summable_mult2[OF this, of "inverse z"] show "summable (\<lambda>n. f (Suc n) * z ^ n)"
+      by (cases "z \<noteq> 0", subst (asm) power_Suc2) (simp_all add: algebra_simps)
+  qed
+  also have "\<dots> \<longleftrightarrow> summable (\<lambda>n. f n * z ^ n)" by (rule summable_Suc_iff)
+  finally show ?thesis .
+qed
+
+lemma powser_split_head:
+  assumes "summable (\<lambda>n. f n * z ^ n :: 'a :: {real_normed_div_algebra,banach})"
+  shows   "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z"
+          "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n) - f 0"
+          "summable (\<lambda>n. f (Suc n) * z ^ n)"
+proof -
+  from assms show "summable (\<lambda>n. f (Suc n) * z ^ n)" by (subst summable_powser_split_head)
+
+  from suminf_mult2[OF this, of z] 
+    have "(\<Sum>n. f (Suc n) * z ^ n) * z = (\<Sum>n. f (Suc n) * z ^ Suc n)"
+    by (simp add: power_commutes algebra_simps)
+  also from assms have "\<dots> = suminf (\<lambda>n. f n * z ^ n) - f 0"
+    by (subst suminf_split_head) simp_all
+  finally show "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z" by simp
+  thus "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n) - f 0" by simp
+qed
+
+lemma summable_partial_sum_bound:
+  fixes f :: "nat \<Rightarrow> 'a :: banach"
+  assumes summable: "summable f" and e: "e > (0::real)"
+  obtains N where "\<And>m n. m \<ge> N \<Longrightarrow> norm (\<Sum>k=m..n. f k) < e"
+proof -
+  from summable have "Cauchy (\<lambda>n. \<Sum>k<n. f k)" 
+    by (simp add: Cauchy_convergent_iff summable_iff_convergent)
+  from CauchyD[OF this e] obtain N 
+    where N: "\<And>m n. m \<ge> N \<Longrightarrow> n \<ge> N \<Longrightarrow> norm ((\<Sum>k<m. f k) - (\<Sum>k<n. f k)) < e" by blast
+  {
+    fix m n :: nat assume m: "m \<ge> N"
+    have "norm (\<Sum>k=m..n. f k) < e"
+    proof (cases "n \<ge> m")
+      assume n: "n \<ge> m"
+      with m have "norm ((\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k)) < e" by (intro N) simp_all
+      also from n have "(\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k) = (\<Sum>k=m..n. f k)"
+        by (subst setsum_diff [symmetric]) (simp_all add: setsum_last_plus)
+      finally show ?thesis .
+    qed (insert e, simp_all)
+  }
+  thus ?thesis by (rule that)
+qed
+
+lemma powser_sums_if: 
+  "(\<lambda>n. (if n = m then (1 :: 'a :: {ring_1,topological_space}) else 0) * z^n) sums z^m"
+proof -
+  have "(\<lambda>n. (if n = m then 1 else 0) * z^n) = (\<lambda>n. if n = m then z^n else 0)" 
+    by (intro ext) auto
+  thus ?thesis by (simp add: sums_single)
+qed
+
 lemma
    fixes f :: "nat \<Rightarrow> real"
    assumes "summable f"
@@ -742,4 +967,82 @@
   with le show "suminf (f \<circ> g) = suminf f" by(rule antisym)
 qed
 
+lemma sums_mono_reindex:
+  assumes subseq: "subseq g" and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
+  shows   "(\<lambda>n. f (g n)) sums c \<longleftrightarrow> f sums c"
+unfolding sums_def
+proof
+  assume lim: "(\<lambda>n. \<Sum>k<n. f k) ----> c"
+  have "(\<lambda>n. \<Sum>k<n. f (g k)) = (\<lambda>n. \<Sum>k<g n. f k)"
+  proof
+    fix n :: nat
+    from subseq have "(\<Sum>k<n. f (g k)) = (\<Sum>k\<in>g`{..<n}. f k)"
+      by (subst setsum.reindex) (auto intro: subseq_imp_inj_on)
+    also from subseq have "\<dots> = (\<Sum>k<g n. f k)"
+      by (intro setsum.mono_neutral_left ballI zero)
+         (auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq)
+    finally show "(\<Sum>k<n. f (g k)) = (\<Sum>k<g n. f k)" .
+  qed
+  also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> ----> c" unfolding o_def .
+  finally show "(\<lambda>n. \<Sum>k<n. f (g k)) ----> c" .
+next
+  assume lim: "(\<lambda>n. \<Sum>k<n. f (g k)) ----> c"
+  def g_inv \<equiv> "\<lambda>n. LEAST m. g m \<ge> n"
+  from filterlim_subseq[OF subseq] have g_inv_ex: "\<exists>m. g m \<ge> n" for n
+    by (auto simp: filterlim_at_top eventually_at_top_linorder)
+  hence g_inv: "g (g_inv n) \<ge> n" for n unfolding g_inv_def by (rule LeastI_ex)
+  have g_inv_least: "m \<ge> g_inv n" if "g m \<ge> n" for m n using that 
+    unfolding g_inv_def by (rule Least_le)
+  have g_inv_least': "g m < n" if "m < g_inv n" for m n using that g_inv_least[of n m] by linarith  
+  have "(\<lambda>n. \<Sum>k<n. f k) = (\<lambda>n. \<Sum>k<g_inv n. f (g k))"
+  proof
+    fix n :: nat
+    {
+      fix k assume k: "k \<in> {..<n} - g`{..<g_inv n}"
+      have "k \<notin> range g"
+      proof (rule notI, elim imageE)
+        fix l assume l: "k = g l"
+        have "g l < g (g_inv n)" by (rule less_le_trans[OF _ g_inv]) (insert k l, simp_all)
+        with subseq have "l < g_inv n" by (simp add: subseq_strict_mono strict_mono_less)
+        with k l show False by simp
+      qed
+      hence "f k = 0" by (rule zero)
+    }
+    with g_inv_least' g_inv have "(\<Sum>k<n. f k) = (\<Sum>k\<in>g`{..<g_inv n}. f k)"
+      by (intro setsum.mono_neutral_right) auto
+    also from subseq have "\<dots> = (\<Sum>k<g_inv n. f (g k))" using subseq_imp_inj_on 
+      by (subst setsum.reindex) simp_all
+    finally show "(\<Sum>k<n. f k) = (\<Sum>k<g_inv n. f (g k))" .
+  qed
+  also {
+    fix K n :: nat assume "g K \<le> n"
+    also have "n \<le> g (g_inv n)" by (rule g_inv)
+    finally have "K \<le> g_inv n" using subseq by (simp add: strict_mono_less_eq subseq_strict_mono)
+  }
+  hence "filterlim g_inv at_top sequentially" 
+    by (auto simp: filterlim_at_top eventually_at_top_linorder)
+  from lim and this have "(\<lambda>n. \<Sum>k<g_inv n. f (g k)) ----> c" by (rule filterlim_compose)
+  finally show "(\<lambda>n. \<Sum>k<n. f k) ----> c" .
+qed
+
+lemma summable_mono_reindex:
+  assumes subseq: "subseq g" and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
+  shows   "summable (\<lambda>n. f (g n)) \<longleftrightarrow> summable f"
+  using sums_mono_reindex[of g f, OF assms] by (simp add: summable_def)
+
+lemma suminf_mono_reindex:                                                                 
+  assumes "subseq g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = (0 :: 'a :: {t2_space,comm_monoid_add})"
+  shows   "suminf (\<lambda>n. f (g n)) = suminf f"
+proof (cases "summable f")
+  case False
+  hence "\<not>(\<exists>c. f sums c)" unfolding summable_def by blast
+  hence "suminf f = The (\<lambda>_. False)" by (simp add: suminf_def)
+  moreover from False have "\<not>summable (\<lambda>n. f (g n))"
+    using summable_mono_reindex[of g f, OF assms] by simp
+  hence "\<not>(\<exists>c. (\<lambda>n. f (g n)) sums c)" unfolding summable_def by blast
+  hence "suminf (\<lambda>n. f (g n)) = The (\<lambda>_. False)" by (simp add: suminf_def)
+  ultimately show ?thesis by simp
+qed (insert sums_mono_reindex[of g f, OF assms] summable_mono_reindex[of g f, OF assms], 
+     simp_all add: sums_iff)
+
 end
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Topological_Spaces.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -353,6 +353,10 @@
   "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
   unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)
 
+lemma (in topological_space) eventually_nhds_in_open: 
+  "open s \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
+  by (subst eventually_nhds) blast
+
 lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
   unfolding trivial_limit_def eventually_nhds by simp
 
@@ -497,6 +501,12 @@
    "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
    unfolding nhds_def filterlim_INF filterlim_principal by auto
 
+lemma tendsto_cong:
+  assumes "eventually (\<lambda>x. f x = g x) F"
+  shows   "(f ---> c) F \<longleftrightarrow> (g ---> c) F"
+  by (rule filterlim_cong[OF refl refl assms])
+
+
 lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
   unfolding tendsto_def le_filter_def by fast
 
@@ -625,6 +635,28 @@
     using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
 qed
 
+lemma limit_frequently_eq:
+  assumes "F \<noteq> bot"
+  assumes "frequently (\<lambda>x. f x = c) F"
+  assumes "(f ---> d) F"
+  shows   "d = (c :: 'a :: t1_space)"
+proof (rule ccontr)
+  assume "d \<noteq> c"
+  from t1_space[OF this] obtain U where "open U" "d \<in> U" "c \<notin> U" by blast
+  from this assms have "eventually (\<lambda>x. f x \<in> U) F" unfolding tendsto_def by blast
+  hence "eventually (\<lambda>x. f x \<noteq> c) F" by eventually_elim (insert `c \<notin> U`, blast)
+  with assms(2) show False unfolding frequently_def by contradiction
+qed
+
+lemma tendsto_imp_eventually_ne:
+  assumes "F \<noteq> bot" "(f ---> c) F" "c \<noteq> (c' :: 'a :: t1_space)"
+  shows   "eventually (\<lambda>z. f z \<noteq> c') F"
+proof (rule ccontr)
+  assume "\<not>eventually (\<lambda>z. f z \<noteq> c') F"
+  hence "frequently (\<lambda>z. f z = c') F" by (simp add: frequently_def)
+  from limit_frequently_eq[OF assms(1) this assms(2)] and assms(3) show False by contradiction
+qed
+
 lemma tendsto_le:
   fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
   assumes F: "\<not> trivial_limit F"
@@ -657,6 +689,9 @@
   shows "a \<ge> x"
   by (rule tendsto_le [OF F tendsto_const x a])
 
+
+
+
 subsubsection \<open>Rules about @{const Lim}\<close>
 
 lemma tendsto_Lim:
@@ -924,6 +959,17 @@
 lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n"
   using assms by (auto simp: subseq_def)
 
+lemma subseq_imp_inj_on: "subseq g \<Longrightarrow> inj_on g A"
+proof (rule inj_onI)
+  assume g: "subseq g"
+  fix x y assume "g x = g y"
+  with subseq_mono[OF g, of x y] subseq_mono[OF g, of y x] show "x = y" 
+    by (cases x y rule: linorder_cases) simp_all
+qed
+
+lemma subseq_strict_mono: "subseq g \<Longrightarrow> strict_mono g"
+  by (intro strict_monoI subseq_mono[of g])
+
 lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
   by (simp add: incseq_def monoseq_def)
 
@@ -2142,6 +2188,15 @@
   assumes A: "connected A" "a \<in> A" "b \<in> A" shows "{a <..< b} \<subseteq> A"
   using connectedD_interval[OF A] by (simp add: subset_eq Ball_def less_imp_le)
 
+lemma connected_contains_Icc:
+  assumes "connected (A :: ('a :: {linorder_topology}) set)" "a \<in> A" "b \<in> A"
+  shows   "{a..b} \<subseteq> A"
+proof
+  fix x assume "x \<in> {a..b}"
+  hence "x = a \<or> x = b \<or> x \<in> {a<..<b}" by auto
+  thus "x \<in> A" using assms connected_contains_Ioo[of A a b] by auto
+qed
+
 subsection \<open>Intermediate Value Theorem\<close>
 
 lemma IVT':
diff -r f2e51e704a96 -r ab2e862263e7 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/HOL/Transcendental.thy	Mon Nov 02 11:56:28 2015 +0100
@@ -16,6 +16,11 @@
   using floor_correct [of "x/y"] assms
   by (auto simp: Real.real_of_nat_Suc field_simps intro: that [of "nat (floor (x/y))"])
 
+lemma fact_in_Reals: "fact n \<in> \<real>" by (induction n) auto
+
+lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
+  by (simp add: pochhammer_def)
+
 lemma of_real_fact [simp]: "of_real (fact n) = fact n"
   by (metis of_nat_fact of_real_of_nat_eq)
 
@@ -1081,6 +1086,15 @@
 qed
 
 
+lemma isCont_pochhammer [continuous_intros]: "isCont (\<lambda>z::'a::real_normed_field. pochhammer z n) z"
+  by (induction n) (auto intro!: continuous_intros simp: pochhammer_rec')
+
+lemma continuous_on_pochhammer [continuous_intros]: 
+  fixes A :: "'a :: real_normed_field set"
+  shows "continuous_on A (\<lambda>z. pochhammer z n)"
+  by (intro continuous_at_imp_continuous_on ballI isCont_pochhammer)
+
+
 subsection \<open>Exponential Function\<close>
 
 definition exp :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
@@ -4227,6 +4241,93 @@
 lemma tan_cot: "tan(pi/2 - x) = inverse(tan x)"
   by (simp add: tan_def sin_diff cos_diff)
 
+subsection \<open>Cotangent\<close>
+
+definition cot :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
+  where "cot = (\<lambda>x. cos x / sin x)"
+
+lemma cot_of_real:
+  "of_real (cot x) = (cot (of_real x) :: 'a::{real_normed_field,banach})"
+  by (simp add: cot_def sin_of_real cos_of_real)
+
+lemma cot_in_Reals [simp]:
+  fixes z :: "'a::{real_normed_field,banach}"
+  shows "z \<in> \<real> \<Longrightarrow> cot z \<in> \<real>"
+  by (simp add: cot_def)
+
+lemma cot_zero [simp]: "cot 0 = 0"
+  by (simp add: cot_def)
+
+lemma cot_pi [simp]: "cot pi = 0"
+  by (simp add: cot_def)
+
+lemma cot_npi [simp]: "cot (real (n::nat) * pi) = 0"
+  by (simp add: cot_def)
+
+lemma cot_minus [simp]: "cot (-x) = - cot x"
+  by (simp add: cot_def)
+
+lemma cot_periodic [simp]: "cot (x + 2*pi) = cot x"
+  by (simp add: cot_def)
+  
+lemma cot_altdef: "cot x = inverse (tan x)"
+  by (simp add: cot_def tan_def)
+
+lemma tan_altdef: "tan x = inverse (cot x)"
+  by (simp add: cot_def tan_def)
+
+lemma tan_cot': "tan(pi/2 - x) = cot x"
+  by (simp add: tan_cot cot_altdef)
+
+lemma cot_gt_zero: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < cot x"
+  by (simp add: cot_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
+
+lemma cot_less_zero:
+  assumes lb: "- pi/2 < x" and "x < 0"
+  shows "cot x < 0"
+proof -
+  have "0 < cot (- x)" using assms by (simp only: cot_gt_zero)
+  thus ?thesis by simp
+qed
+
+lemma DERIV_cot [simp]:
+  fixes x :: "'a::{real_normed_field,banach}"
+  shows "sin x \<noteq> 0 \<Longrightarrow> DERIV cot x :> -inverse ((sin x)\<^sup>2)"
+  unfolding cot_def using cos_squared_eq[of x]
+  by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
+
+lemma isCont_cot:
+  fixes x :: "'a::{real_normed_field,banach}"
+  shows "sin x \<noteq> 0 \<Longrightarrow> isCont cot x"
+  by (rule DERIV_cot [THEN DERIV_isCont])
+
+lemma isCont_cot' [simp,continuous_intros]:
+  fixes a :: "'a::{real_normed_field,banach}" and f :: "'a \<Rightarrow> 'a"
+  shows "\<lbrakk>isCont f a; sin (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. cot (f x)) a"
+  by (rule isCont_o2 [OF _ isCont_cot])
+
+lemma tendsto_cot [tendsto_intros]:
+  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
+  shows "\<lbrakk>(f ---> a) F; sin a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. cot (f x)) ---> cot a) F"
+  by (rule isCont_tendsto_compose [OF isCont_cot])
+
+lemma continuous_cot:
+  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
+  shows "continuous F f \<Longrightarrow> sin (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. cot (f x))"
+  unfolding continuous_def by (rule tendsto_cot)
+
+lemma continuous_on_cot [continuous_intros]:
+  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
+  shows "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. sin (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. cot (f x))"
+  unfolding continuous_on_def by (auto intro: tendsto_cot)
+
+lemma continuous_within_cot [continuous_intros]:
+  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
+  shows
+  "continuous (at x within s) f \<Longrightarrow> sin (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. cot (f x))"
+  unfolding continuous_within by (rule tendsto_cot)
+
+
 subsection \<open>Inverse Trigonometric Functions\<close>
 
 definition arcsin :: "real => real"