Rounding function, uniform limits, cotangent, binomial identities
authoreberlm
Mon Nov 02 11:56:28 2015 +0100 (2015-11-02)
changeset 61531ab2e862263e7
parent 61524 f2e51e704a96
child 61532 e3984606b4b6
Rounding function, uniform limits, cotangent, binomial identities
src/HOL/Archimedean_Field.thy
src/HOL/Binomial.thy
src/HOL/Complex.thy
src/HOL/Filter.thy
src/HOL/Int.thy
src/HOL/Library/Convex.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Derivative.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Uniform_Limit.thy
src/HOL/Nat.thy
src/HOL/Parity.thy
src/HOL/Power.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Series.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Thu Oct 29 15:40:52 2015 +0100
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Mon Nov 02 11:56:28 2015 +0100
     1.3 @@ -486,6 +486,11 @@
     1.4    "- numeral v < ceiling x \<longleftrightarrow> - numeral v < x"
     1.5    by (simp add: less_ceiling_iff)
     1.6  
     1.7 +lemma ceiling_altdef: "ceiling x = (if x = of_int (floor x) then floor x else floor x + 1)"
     1.8 +  by (intro ceiling_unique, (simp, linarith?)+)
     1.9 +
    1.10 +lemma floor_le_ceiling [simp]: "floor x \<le> ceiling x" by (simp add: ceiling_altdef)
    1.11 +
    1.12  text \<open>Addition and subtraction of integers\<close>
    1.13  
    1.14  lemma ceiling_add_of_int [simp]: "ceiling (x + of_int z) = ceiling x + z"
    1.15 @@ -592,4 +597,79 @@
    1.16    apply (simp add: frac_def)
    1.17    by (meson frac_lt_1 less_iff_diff_less_0 not_le not_less_iff_gr_or_eq)
    1.18  
    1.19 +
    1.20 +subsection \<open>Rounding to the nearest integer\<close>
    1.21 +
    1.22 +definition round where "round x = \<lfloor>x + 1/2\<rfloor>"
    1.23 +
    1.24 +lemma of_int_round_ge:     "of_int (round x) \<ge> x - 1/2"
    1.25 +  and of_int_round_le:     "of_int (round x) \<le> x + 1/2"
    1.26 +  and of_int_round_abs_le: "\<bar>of_int (round x) - x\<bar> \<le> 1/2"
    1.27 +  and of_int_round_gt:     "of_int (round x) > x - 1/2"
    1.28 +proof -
    1.29 +  from floor_correct[of "x + 1/2"] have "x + 1/2 < of_int (round x) + 1" by (simp add: round_def)
    1.30 +  from add_strict_right_mono[OF this, of "-1"] show A: "of_int (round x) > x - 1/2" by simp
    1.31 +  thus "of_int (round x) \<ge> x - 1/2" by simp
    1.32 +  from floor_correct[of "x + 1/2"] show "of_int (round x) \<le> x + 1/2" by (simp add: round_def)
    1.33 +  with A show "\<bar>of_int (round x) - x\<bar> \<le> 1/2" by linarith
    1.34 +qed
    1.35 +
    1.36 +lemma round_of_int [simp]: "round (of_int n) = n"
    1.37 +  unfolding round_def by (subst floor_unique_iff) force
    1.38 +
    1.39 +lemma round_0 [simp]: "round 0 = 0"
    1.40 +  using round_of_int[of 0] by simp
    1.41 +
    1.42 +lemma round_1 [simp]: "round 1 = 1"
    1.43 +  using round_of_int[of 1] by simp
    1.44 +
    1.45 +lemma round_numeral [simp]: "round (numeral n) = numeral n"
    1.46 +  using round_of_int[of "numeral n"] by simp
    1.47 +
    1.48 +lemma round_neg_numeral [simp]: "round (-numeral n) = -numeral n"
    1.49 +  using round_of_int[of "-numeral n"] by simp
    1.50 +
    1.51 +lemma round_of_nat [simp]: "round (of_nat n) = of_nat n"
    1.52 +  using round_of_int[of "int n"] by simp
    1.53 +
    1.54 +lemma round_mono: "x \<le> y \<Longrightarrow> round x \<le> round y"
    1.55 +  unfolding round_def by (intro floor_mono) simp
    1.56 +
    1.57 +lemma round_unique: "of_int y > x - 1/2 \<Longrightarrow> of_int y \<le> x + 1/2 \<Longrightarrow> round x = y"
    1.58 +unfolding round_def
    1.59 +proof (rule floor_unique)
    1.60 +  assume "x - 1 / 2 < of_int y"
    1.61 +  from add_strict_left_mono[OF this, of 1] show "x + 1 / 2 < of_int y + 1" by simp
    1.62 +qed
    1.63 +
    1.64 +lemma round_altdef: "round x = (if frac x \<ge> 1/2 then ceiling x else floor x)"
    1.65 +  by (cases "frac x \<ge> 1/2")
    1.66 +     (rule round_unique, ((simp add: frac_def field_simps ceiling_altdef, linarith?)+)[2])+
    1.67 +
    1.68 +lemma floor_le_round: "\<lfloor>x\<rfloor> \<le> round x"
    1.69 +  unfolding round_def by (intro floor_mono) simp
    1.70 +
    1.71 +lemma ceiling_ge_round: "\<lceil>x\<rceil> \<ge> round x" unfolding round_altdef by simp
    1.72 +     
    1.73 +lemma round_diff_minimal: 
    1.74 +  fixes z :: "'a :: floor_ceiling"
    1.75 +  shows "abs (z - of_int (round z)) \<le> abs (z - of_int m)"
    1.76 +proof (cases "of_int m \<ge> z")
    1.77 +  case True
    1.78 +  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (ceiling z) - z\<bar>"
    1.79 +    unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith?
    1.80 +  also have "of_int \<lceil>z\<rceil> - z \<ge> 0" by linarith
    1.81 +  with True have "\<bar>of_int (ceiling z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
    1.82 +    by (simp add: ceiling_le_iff)
    1.83 +  finally show ?thesis .
    1.84 +next
    1.85 +  case False
    1.86 +  hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int (floor z) - z\<bar>"
    1.87 +    unfolding round_altdef by (simp add: ceiling_altdef frac_def) linarith?
    1.88 +  also have "z - of_int \<lfloor>z\<rfloor> \<ge> 0" by linarith
    1.89 +  with False have "\<bar>of_int (floor z) - z\<bar> \<le> \<bar>z - of_int m\<bar>"
    1.90 +    by (simp add: le_floor_iff)
    1.91 +  finally show ?thesis .
    1.92 +qed
    1.93 +
    1.94  end
     2.1 --- a/src/HOL/Binomial.thy	Thu Oct 29 15:40:52 2015 +0100
     2.2 +++ b/src/HOL/Binomial.thy	Mon Nov 02 11:56:28 2015 +0100
     2.3 @@ -38,6 +38,10 @@
     2.4  lemma fact_mono_nat: "m \<le> n \<Longrightarrow> fact m \<le> (fact n :: nat)"
     2.5    by (induct n) (auto simp: le_Suc_eq)
     2.6  
     2.7 +lemma fact_in_Nats: "fact n \<in> \<nat>" by (induction n) auto
     2.8 +
     2.9 +lemma fact_in_Ints: "fact n \<in> \<int>" by (induction n) auto
    2.10 +
    2.11  context
    2.12    assumes "SORT_CONSTRAINT('a::linordered_semidom)"
    2.13  begin
    2.14 @@ -381,6 +385,41 @@
    2.15  lemma sum_choose_upper: "(\<Sum>k=0..n. k choose m) = Suc n choose Suc m"
    2.16    by (induct n) auto
    2.17  
    2.18 +lemma choose_alternating_sum: 
    2.19 +  "n > 0 \<Longrightarrow> (\<Sum>i\<le>n. (-1)^i * of_nat (n choose i)) = (0 :: 'a :: comm_ring_1)"
    2.20 +  using binomial_ring[of "-1 :: 'a" 1 n] by (simp add: atLeast0AtMost mult_of_nat_commute zero_power)
    2.21 +
    2.22 +lemma choose_even_sum:
    2.23 +  assumes "n > 0"
    2.24 +  shows   "2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"
    2.25 +proof - 
    2.26 +  have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) + (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"
    2.27 +    using choose_row_sum[of n]
    2.28 +    by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)
    2.29 +  also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) + (-1) ^ i * of_nat (n choose i))"
    2.30 +    by (simp add: setsum.distrib)
    2.31 +  also have "\<dots> = 2 * (\<Sum>i\<le>n. if even i then of_nat (n choose i) else 0)" 
    2.32 +    by (subst setsum_right_distrib, intro setsum.cong) simp_all
    2.33 +  finally show ?thesis ..
    2.34 +qed
    2.35 +
    2.36 +lemma choose_odd_sum:
    2.37 +  assumes "n > 0"
    2.38 +  shows   "2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0) = (2 ^ n :: 'a :: comm_ring_1)"
    2.39 +proof - 
    2.40 +  have "2 ^ n = (\<Sum>i\<le>n. of_nat (n choose i)) - (\<Sum>i\<le>n. (-1) ^ i * of_nat (n choose i) :: 'a)"
    2.41 +    using choose_row_sum[of n]
    2.42 +    by (simp add: choose_alternating_sum assms atLeast0AtMost of_nat_setsum[symmetric] of_nat_power)
    2.43 +  also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) - (-1) ^ i * of_nat (n choose i))"
    2.44 +    by (simp add: setsum_subtractf)
    2.45 +  also have "\<dots> = 2 * (\<Sum>i\<le>n. if odd i then of_nat (n choose i) else 0)" 
    2.46 +    by (subst setsum_right_distrib, intro setsum.cong) simp_all
    2.47 +  finally show ?thesis ..
    2.48 +qed
    2.49 +
    2.50 +lemma choose_row_sum': "(\<Sum>k\<le>n. (n choose k)) = 2 ^ n"
    2.51 +  using choose_row_sum[of n] by (simp add: atLeast0AtMost)
    2.52 +
    2.53  lemma natsum_reverse_index:
    2.54    fixes m::nat
    2.55    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)"
    2.56 @@ -417,6 +456,12 @@
    2.57  
    2.58  lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"
    2.59    by (simp add: pochhammer_def)
    2.60 +  
    2.61 +lemma pochhammer_of_nat: "pochhammer (of_nat x) n = of_nat (pochhammer x n)"
    2.62 +  by (simp add: pochhammer_def of_nat_setprod)
    2.63 +
    2.64 +lemma pochhammer_of_int: "pochhammer (of_int x) n = of_int (pochhammer x n)"
    2.65 +  by (simp add: pochhammer_def of_int_setprod)
    2.66  
    2.67  lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"
    2.68  proof -
    2.69 @@ -460,6 +505,18 @@
    2.70      done
    2.71  qed
    2.72  
    2.73 +lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"
    2.74 +proof (induction n arbitrary: z)
    2.75 +  case (Suc n z)
    2.76 +  have "pochhammer z (Suc (Suc n)) = z * pochhammer (z + 1) (Suc n)" 
    2.77 +    by (simp add: pochhammer_rec)
    2.78 +  also note Suc
    2.79 +  also have "z * ((z + 1 + of_nat n) * pochhammer (z + 1) n) = 
    2.80 +               (z + of_nat (Suc n)) * pochhammer z (Suc n)"
    2.81 +    by (simp_all add: pochhammer_rec algebra_simps)
    2.82 +  finally show ?case .
    2.83 +qed simp_all
    2.84 +
    2.85  lemma pochhammer_fact: "fact n = pochhammer 1 n"
    2.86    unfolding fact_altdef
    2.87    apply (cases n)
    2.88 @@ -547,6 +604,32 @@
    2.89    unfolding pochhammer_minus
    2.90    by (simp add: of_nat_diff pochhammer_fact)
    2.91  
    2.92 +lemma pochhammer_product': 
    2.93 +  "pochhammer z (n + m) = pochhammer z n * pochhammer (z + of_nat n) m"
    2.94 +proof (induction n arbitrary: z)
    2.95 +  case (Suc n z)
    2.96 +  have "pochhammer z (Suc n) * pochhammer (z + of_nat (Suc n)) m = 
    2.97 +            z * (pochhammer (z + 1) n * pochhammer (z + 1 + of_nat n) m)"
    2.98 +    by (simp add: pochhammer_rec ac_simps)
    2.99 +  also note Suc[symmetric]
   2.100 +  also have "z * pochhammer (z + 1) (n + m) = pochhammer z (Suc (n + m))"
   2.101 +    by (subst pochhammer_rec) simp
   2.102 +  finally show ?case by simp
   2.103 +qed simp
   2.104 +
   2.105 +lemma pochhammer_product: 
   2.106 +  "m \<le> n \<Longrightarrow> pochhammer z n = pochhammer z m * pochhammer (z + of_nat m) (n - m)"
   2.107 +  using pochhammer_product'[of z m "n - m"] by simp
   2.108 +
   2.109 +lemma pochhammer_absorb_comp:
   2.110 +  "((r :: 'a :: comm_ring_1) - of_nat k) * pochhammer (- r) k = r * pochhammer (-r + 1) k" 
   2.111 +  (is "?lhs = ?rhs")
   2.112 +proof -
   2.113 +  have "?lhs = -pochhammer (-r) (Suc k)" by (subst pochhammer_rec') (simp add: algebra_simps)
   2.114 +  also have "\<dots> = ?rhs" by (subst pochhammer_rec) simp
   2.115 +  finally show ?thesis .
   2.116 +qed
   2.117 +
   2.118  
   2.119  subsection\<open>Generalized binomial coefficients\<close>
   2.120  
   2.121 @@ -729,6 +812,89 @@
   2.122    then show ?thesis using kn by simp
   2.123  qed
   2.124  
   2.125 +lemma choose_rising_sum:
   2.126 +  "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))"
   2.127 +  "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose m)"
   2.128 +proof -
   2.129 +  show "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose (n + 1))" by (induction m) simp_all
   2.130 +  also have "... = ((n + m + 1) choose m)" by (subst binomial_symmetric) simp_all
   2.131 +  finally show "(\<Sum>j\<le>m. ((n + j) choose n)) = ((n + m + 1) choose m)" .
   2.132 +qed
   2.133 +
   2.134 +lemma choose_linear_sum:
   2.135 +  "(\<Sum>i\<le>n. i * (n choose i)) = n * 2 ^ (n - 1)"
   2.136 +proof (cases n)
   2.137 +  case (Suc m)
   2.138 +  have "(\<Sum>i\<le>n. i * (n choose i)) = (\<Sum>i\<le>Suc m. i * (Suc m choose i))" by (simp add: Suc)
   2.139 +  also have "... = Suc m * 2 ^ m"
   2.140 +    by (simp only: setsum_atMost_Suc_shift Suc_times_binomial setsum_right_distrib[symmetric]) 
   2.141 +       (simp add: choose_row_sum')
   2.142 +  finally show ?thesis using Suc by simp
   2.143 +qed simp_all
   2.144 +
   2.145 +lemma choose_alternating_linear_sum:
   2.146 +  assumes "n \<noteq> 1"
   2.147 +  shows   "(\<Sum>i\<le>n. (-1)^i * of_nat i * of_nat (n choose i) :: 'a :: comm_ring_1) = 0"
   2.148 +proof (cases n)
   2.149 +  case (Suc m)
   2.150 +  with assms have "m > 0" by simp
   2.151 +  have "(\<Sum>i\<le>n. (-1) ^ i * of_nat i * of_nat (n choose i) :: 'a) = 
   2.152 +            (\<Sum>i\<le>Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))" by (simp add: Suc)
   2.153 +  also have "... = (\<Sum>i\<le>m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))"
   2.154 +    by (simp only: setsum_atMost_Suc_shift setsum_right_distrib[symmetric] of_nat_mult mult_ac) simp
   2.155 +  also have "... = -of_nat (Suc m) * (\<Sum>i\<le>m. (-1) ^ i * of_nat ((m choose i)))"
   2.156 +    by (subst setsum_right_distrib, rule setsum.cong[OF refl], subst Suc_times_binomial)
   2.157 +       (simp add: algebra_simps of_nat_mult)
   2.158 +  also have "(\<Sum>i\<le>m. (-1 :: 'a) ^ i * of_nat ((m choose i))) = 0"
   2.159 +    using choose_alternating_sum[OF `m > 0`] by simp
   2.160 +  finally show ?thesis by simp
   2.161 +qed simp
   2.162 +
   2.163 +lemma vandermonde:
   2.164 +  "(\<Sum>k\<le>r. (m choose k) * (n choose (r - k))) = (m + n) choose r"
   2.165 +proof (induction n arbitrary: r)
   2.166 +  case 0
   2.167 +  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)"
   2.168 +    by (intro setsum.cong) simp_all
   2.169 +  also have "... = m choose r" by (simp add: setsum.delta)
   2.170 +  finally show ?case by simp
   2.171 +next
   2.172 +  case (Suc n r)
   2.173 +  show ?case by (cases r) (simp_all add: Suc [symmetric] algebra_simps setsum.distrib Suc_diff_le)
   2.174 +qed
   2.175 +
   2.176 +lemma choose_square_sum:
   2.177 +  "(\<Sum>k\<le>n. (n choose k)^2) = ((2*n) choose n)"
   2.178 +  using vandermonde[of n n n] by (simp add: power2_eq_square mult_2 binomial_symmetric [symmetric])
   2.179 +
   2.180 +lemma pochhammer_binomial_sum:
   2.181 +  fixes a b :: "'a :: comm_ring_1"
   2.182 +  shows "pochhammer (a + b) n = (\<Sum>k\<le>n. of_nat (n choose k) * pochhammer a k * pochhammer b (n - k))"
   2.183 +proof (induction n arbitrary: a b)
   2.184 +  case (Suc n a b)
   2.185 +  have "(\<Sum>k\<le>Suc n. of_nat (Suc n choose k) * pochhammer a k * pochhammer b (Suc n - k)) =
   2.186 +            (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
   2.187 +            ((\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
   2.188 +            pochhammer b (Suc n))"
   2.189 +    by (subst setsum_atMost_Suc_shift) (simp add: ring_distribs setsum.distrib)
   2.190 +  also have "(\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) =
   2.191 +               a * pochhammer ((a + 1) + b) n"
   2.192 +    by (subst Suc) (simp add: setsum_right_distrib pochhammer_rec mult_ac)
   2.193 +  also have "(\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) + pochhammer b (Suc n) = 
   2.194 +               (\<Sum>i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
   2.195 +    by (subst setsum_head_Suc, simp, subst setsum_shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost)
   2.196 +  also have "... = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
   2.197 +    using Suc by (intro setsum.mono_neutral_right) (auto simp: not_le binomial_eq_0)
   2.198 +  also have "... = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc (n - i)))"
   2.199 +    by (intro setsum.cong) (simp_all add: Suc_diff_le)
   2.200 +  also have "... = b * pochhammer (a + (b + 1)) n"
   2.201 +    by (subst Suc) (simp add: setsum_right_distrib mult_ac pochhammer_rec)
   2.202 +  also have "a * pochhammer ((a + 1) + b) n + b * pochhammer (a + (b + 1)) n =
   2.203 +               pochhammer (a + b) (Suc n)" by (simp add: pochhammer_rec algebra_simps)
   2.204 +  finally show ?case ..
   2.205 +qed simp_all
   2.206 +
   2.207 +
   2.208  text\<open>Contributed by Manuel Eberl, generalised by LCP.
   2.209    Alternative definition of the binomial coefficient as @{term "\<Prod>i<k. (n - i) / (k - i)"}\<close>
   2.210  lemma gbinomial_altdef_of_nat:
   2.211 @@ -774,6 +940,285 @@
   2.212    finally show ?thesis .
   2.213  qed
   2.214  
   2.215 +lemma gbinomial_negated_upper: "(a gchoose b) = (-1) ^ b * ((of_nat b - a - 1) gchoose b)"
   2.216 +  by (simp add: gbinomial_pochhammer pochhammer_minus algebra_simps)
   2.217 +
   2.218 +lemma gbinomial_minus: "((-a) gchoose b) = (-1) ^ b * ((a + of_nat b - 1) gchoose b)"
   2.219 +  by (subst gbinomial_negated_upper) (simp add: add_ac)
   2.220 +
   2.221 +lemma Suc_times_gbinomial:
   2.222 +  "of_nat (Suc b) * ((a + 1) gchoose (Suc b)) = (a + 1) * (a gchoose b)"
   2.223 +proof (cases b)
   2.224 +  case (Suc b)
   2.225 +  hence "((a + 1) gchoose (Suc (Suc b))) = 
   2.226 +             (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
   2.227 +    by (simp add: field_simps gbinomial_def)
   2.228 +  also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
   2.229 +    by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
   2.230 +  also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
   2.231 +    by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
   2.232 +  finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc)
   2.233 +qed simp
   2.234 +
   2.235 +lemma gbinomial_factors:
   2.236 +  "((a + 1) gchoose (Suc b)) = (a + 1) / of_nat (Suc b) * (a gchoose b)"
   2.237 +proof (cases b)
   2.238 +  case (Suc b)
   2.239 +  hence "((a + 1) gchoose (Suc (Suc b))) = 
   2.240 +             (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
   2.241 +    by (simp add: field_simps gbinomial_def)
   2.242 +  also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
   2.243 +    by (simp add: setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
   2.244 +  also have "... / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
   2.245 +    by (simp_all add: gbinomial_def setprod_nat_ivl_1_Suc setprod_shift_bounds_cl_Suc_ivl)
   2.246 +  finally show ?thesis by (simp add: Suc)
   2.247 +qed simp
   2.248 +
   2.249 +lemma gbinomial_rec: "((r + 1) gchoose (Suc k)) = (r gchoose k) * ((r + 1) / of_nat (Suc k))"
   2.250 +  using gbinomial_mult_1[of r k]
   2.251 +  by (subst gbinomial_Suc_Suc) (simp add: field_simps del: of_nat_Suc, simp add: algebra_simps)
   2.252 +
   2.253 +lemma gbinomial_of_nat_symmetric: "k \<le> n \<Longrightarrow> (of_nat n) gchoose k = (of_nat n) gchoose (n - k)"
   2.254 +  using binomial_symmetric[of k n] by (simp add: binomial_gbinomial [symmetric])
   2.255 +
   2.256 +
   2.257 +text \<open>The absorption identity (equation 5.5 \cite[p.~157]{GKP}):\[
   2.258 +{r \choose k} = \frac{r}{k}{r - 1 \choose k - 1},\quad \textnormal{integer } k \neq 0.
   2.259 +\]\<close>
   2.260 +lemma gbinomial_absorption': 
   2.261 +  "k > 0 \<Longrightarrow> (r gchoose k) = (r / of_nat(k)) * (r - 1 gchoose (k - 1))"
   2.262 +  using gbinomial_rec[of "r - 1" "k - 1"] 
   2.263 +  by (simp_all add: gbinomial_rec field_simps del: of_nat_Suc)
   2.264 +
   2.265 +text \<open>The absorption identity is written in the following form to avoid
   2.266 +division by $k$ (the lower index) and therefore remove the $k \neq 0$
   2.267 +restriction\cite[p.~157]{GKP}:\[
   2.268 +k{r \choose k} = r{r - 1 \choose k - 1}, \quad \textnormal{integer } k.
   2.269 +\]\<close>
   2.270 +lemma gbinomial_absorption:
   2.271 +  "of_nat (Suc k) * (r gchoose Suc k) = r * ((r - 1) gchoose k)"
   2.272 +  using gbinomial_absorption'[of "Suc k" r] by (simp add: field_simps del: of_nat_Suc)
   2.273 +
   2.274 +text \<open>The absorption identity for natural number binomial coefficients:\<close>
   2.275 +lemma binomial_absorption:
   2.276 +  "Suc k * (n choose Suc k) = n * ((n - 1) choose k)"
   2.277 +  by (cases n) (simp_all add: binomial_eq_0 Suc_times_binomial del: binomial_Suc_Suc mult_Suc)
   2.278 +
   2.279 +text \<open>The absorption companion identity for natural number coefficients,
   2.280 +following the proof by GKP \cite[p.~157]{GKP}:\<close>
   2.281 +lemma binomial_absorb_comp:
   2.282 +  "(n - k) * (n choose k) = n * ((n - 1) choose k)" (is "?lhs = ?rhs")
   2.283 +proof (cases "n \<le> k")
   2.284 +  case False
   2.285 +  then have "?rhs = Suc ((n - 1) - k) * (n choose Suc ((n - 1) - k))"
   2.286 +    using binomial_symmetric[of k "n - 1"] binomial_absorption[of "(n - 1) - k" n]
   2.287 +    by simp
   2.288 +  also from False have "Suc ((n - 1) - k) = n - k" by simp
   2.289 +  also from False have "n choose \<dots> = n choose k" by (intro binomial_symmetric [symmetric]) simp_all
   2.290 +  finally show ?thesis ..
   2.291 +qed auto
   2.292 +
   2.293 +text \<open>The generalised absorption companion identity:\<close>
   2.294 +lemma gbinomial_absorb_comp: "(r - of_nat k) * (r gchoose k) = r * ((r - 1) gchoose k)"
   2.295 +  using pochhammer_absorb_comp[of r k] by (simp add: gbinomial_pochhammer)
   2.296 +
   2.297 +lemma gbinomial_addition_formula:
   2.298 +  "r gchoose (Suc k) = ((r - 1) gchoose (Suc k)) + ((r - 1) gchoose k)"
   2.299 +  using gbinomial_Suc_Suc[of "r - 1" k] by (simp add: algebra_simps)
   2.300 +
   2.301 +lemma binomial_addition_formula:
   2.302 +  "0 < n \<Longrightarrow> n choose (Suc k) = ((n - 1) choose (Suc k)) + ((n - 1) choose k)"
   2.303 +  by (subst choose_reduce_nat) simp_all
   2.304 +
   2.305 +
   2.306 +text \<open>
   2.307 +  Equation 5.9 of the reference material \cite[p.~159]{GKP} is a useful
   2.308 +  summation formula, operating on both indices:\[
   2.309 +  \sum\limits_{k \leq n}{r + k \choose k} = {r + n + 1 \choose n},
   2.310 +   \quad \textnormal{integer } n.
   2.311 +  \] 
   2.312 +\<close>
   2.313 +lemma gbinomial_parallel_sum:
   2.314 +"(\<Sum>k\<le>n. (r + of_nat k) gchoose k) = (r + of_nat n + 1) gchoose n"
   2.315 +proof (induction n)
   2.316 +  case (Suc m)
   2.317 +  thus ?case using gbinomial_Suc_Suc[of "(r + of_nat m + 1)" m] by (simp add: add_ac)
   2.318 +qed auto
   2.319 +
   2.320 +subsection \<open>Summation on the upper index\<close>
   2.321 +text \<open>
   2.322 +  Another summation formula is equation 5.10 of the reference material \cite[p.~160]{GKP},
   2.323 +  aptly named \emph{summation on the upper index}:\[\sum_{0 \leq k \leq n} {k \choose m} = 
   2.324 +  {n + 1 \choose m + 1}, \quad \textnormal{integers } m, n \geq 0.\]
   2.325 +\<close>
   2.326 +lemma gbinomial_sum_up_index:
   2.327 +  "(\<Sum>k = 0..n. (of_nat k gchoose m) :: 'a :: field_char_0) = (of_nat n + 1) gchoose (m + 1)"
   2.328 +proof (induction n)
   2.329 +  case 0
   2.330 +  show ?case using gbinomial_Suc_Suc[of 0 m] by (cases m) auto
   2.331 +next
   2.332 +  case (Suc n)
   2.333 +  thus ?case using gbinomial_Suc_Suc[of "of_nat (Suc n) :: 'a" m] by (simp add: add_ac)
   2.334 +qed
   2.335 +
   2.336 +lemma gbinomial_index_swap: 
   2.337 +  "((-1) ^ m) * ((- (of_nat n) - 1) gchoose m) = ((-1) ^ n) * ((- (of_nat m) - 1) gchoose n)"
   2.338 +  (is "?lhs = ?rhs")
   2.339 +proof -
   2.340 +  have "?lhs = (of_nat (m + n) gchoose m)"
   2.341 +    by (subst gbinomial_negated_upper) (simp add: power_mult_distrib [symmetric])
   2.342 +  also have "\<dots> = (of_nat (m + n) gchoose n)" by (subst gbinomial_of_nat_symmetric) simp_all
   2.343 +  also have "\<dots> = ?rhs" by (subst gbinomial_negated_upper) simp
   2.344 +  finally show ?thesis .
   2.345 +qed
   2.346 +
   2.347 +lemma gbinomial_sum_lower_neg: 
   2.348 +  "(\<Sum>k\<le>m. (r gchoose k) * (- 1) ^ k) = (- 1) ^ m * (r - 1 gchoose m)" (is "?lhs = ?rhs")
   2.349 +proof -
   2.350 +  have "?lhs = (\<Sum>k\<le>m. -(r + 1) + of_nat k gchoose k)"
   2.351 +    by (intro setsum.cong[OF refl]) (subst gbinomial_negated_upper, simp add: power_mult_distrib)
   2.352 +  also have "\<dots>  = -r + of_nat m gchoose m" by (subst gbinomial_parallel_sum) simp
   2.353 +  also have "\<dots> = ?rhs" by (subst gbinomial_negated_upper) (simp add: power_mult_distrib)
   2.354 +  finally show ?thesis .
   2.355 +qed
   2.356 +
   2.357 +lemma gbinomial_partial_row_sum:
   2.358 +"(\<Sum>k\<le>m. (r gchoose k) * ((r / 2) - of_nat k)) = ((of_nat m + 1)/2) * (r gchoose (m + 1))"
   2.359 +proof (induction m)
   2.360 +  case (Suc mm)
   2.361 +  hence "(\<Sum>k\<le>Suc mm. (r gchoose k) * (r / 2 - of_nat k)) = 
   2.362 +             (r - of_nat (Suc mm)) * (r gchoose Suc mm) / 2" by (simp add: algebra_simps)
   2.363 +  also have "\<dots> = r * (r - 1 gchoose Suc mm) / 2" by (subst gbinomial_absorb_comp) (rule refl)
   2.364 +  also have "\<dots> = (of_nat (Suc mm) + 1) / 2 * (r gchoose (Suc mm + 1))"
   2.365 +    by (subst gbinomial_absorption [symmetric]) simp
   2.366 +  finally show ?case .
   2.367 +qed simp_all
   2.368 +
   2.369 +lemma setsum_bounds_lt_plus1: "(\<Sum>k<mm. f (Suc k)) = (\<Sum>k=1..mm. f k)"
   2.370 +  by (induction mm) simp_all
   2.371 +
   2.372 +lemma gbinomial_partial_sum_poly:
   2.373 +  "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) =
   2.374 +       (\<Sum>k\<le>m. (-r gchoose k) * (-x)^k * (x + y)^(m-k))" (is "?lhs m = ?rhs m")
   2.375 +proof (induction m)
   2.376 +  case (Suc mm)
   2.377 +  def G \<equiv> "\<lambda>i k. (of_nat i + r gchoose k) * x^k * y^(i-k)" and S \<equiv> ?lhs
   2.378 +  have SG_def: "S = (\<lambda>i. (\<Sum>k\<le>i. (G i k)))" unfolding S_def G_def ..
   2.379 +
   2.380 +  have "S (Suc mm) = G (Suc mm) 0 + (\<Sum>k=Suc 0..Suc mm. G (Suc mm) k)"
   2.381 +    using SG_def by (simp add: setsum_head_Suc atLeast0AtMost [symmetric])
   2.382 +  also have "(\<Sum>k=Suc 0..Suc mm. G (Suc mm) k) = (\<Sum>k=0..mm. G (Suc mm) (Suc k))"
   2.383 +    by (subst setsum_shift_bounds_cl_Suc_ivl) simp
   2.384 +  also have "\<dots> = (\<Sum>k=0..mm. ((of_nat mm + r gchoose (Suc k))
   2.385 +                    + (of_nat mm + r gchoose k)) * x^(Suc k) * y^(mm - k))"
   2.386 +    unfolding G_def by (subst gbinomial_addition_formula) simp
   2.387 +  also have "\<dots> = (\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))
   2.388 +                  + (\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k))"
   2.389 +    by (subst setsum.distrib [symmetric]) (simp add: algebra_simps)
   2.390 +  also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k)) = 
   2.391 +               (\<Sum>k<Suc mm. (of_nat mm + r gchoose (Suc k)) * x^(Suc k) * y^(mm - k))"
   2.392 +    by (simp only: atLeast0AtMost lessThan_Suc_atMost)
   2.393 +  also have "\<dots> = (\<Sum>k<mm. (of_nat mm + r gchoose Suc k) * x^(Suc k) * y^(mm-k)) 
   2.394 +                      + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" (is "_ = ?A + ?B")
   2.395 +    by (subst setsum_lessThan_Suc) simp
   2.396 +  also have "?A = (\<Sum>k=1..mm. (of_nat mm + r gchoose k) * x^k * y^(mm - k + 1))"
   2.397 +  proof (subst setsum_bounds_lt_plus1 [symmetric], intro setsum.cong[OF refl], clarify)
   2.398 +    fix k assume "k < mm"
   2.399 +    hence "mm - k = mm - Suc k + 1" by linarith
   2.400 +    thus "(of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - k) =
   2.401 +            (of_nat mm + r gchoose Suc k) * x ^ Suc k * y ^ (mm - Suc k + 1)" by (simp only:)
   2.402 +  qed
   2.403 +  also have "\<dots> + ?B = y * (\<Sum>k=1..mm. (G mm k)) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" 
   2.404 +    unfolding G_def by (subst setsum_right_distrib) (simp add: algebra_simps)
   2.405 +  also have "(\<Sum>k=0..mm. (of_nat mm + r gchoose k) * x^(Suc k) * y^(mm - k)) = x * (S mm)"
   2.406 +      unfolding S_def by (subst setsum_right_distrib) (simp add: atLeast0AtMost algebra_simps)
   2.407 +  also have "(G (Suc mm) 0) = y * (G mm 0)" by (simp add: G_def)
   2.408 +  finally have "S (Suc mm) = y * ((G mm 0) + (\<Sum>k=1..mm. (G mm k))) 
   2.409 +                + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm) + x * (S mm)"
   2.410 +    by (simp add: ring_distribs)
   2.411 +  also have "(G mm 0) + (\<Sum>k=1..mm. (G mm k)) = S mm" 
   2.412 +    by (simp add: setsum_head_Suc[symmetric] SG_def atLeast0AtMost)
   2.413 +  finally have "S (Suc mm) = (x + y) * (S mm) + (of_nat mm + r gchoose (Suc mm)) * x^(Suc mm)" 
   2.414 +    by (simp add: algebra_simps)
   2.415 +  also have "(of_nat mm + r gchoose (Suc mm)) = (-1) ^ (Suc mm) * (-r gchoose (Suc mm))"
   2.416 +    by (subst gbinomial_negated_upper) simp
   2.417 +  also have "(-1) ^ Suc mm * (- r gchoose Suc mm) * x ^ Suc mm =
   2.418 +                 (-r gchoose (Suc mm)) * (-x) ^ Suc mm" by (simp add: power_minus[of x])
   2.419 +  also have "(x + y) * S mm + \<dots> = (x + y) * ?rhs mm + (-r gchoose (Suc mm)) * (-x)^Suc mm"
   2.420 +    unfolding S_def by (subst Suc.IH) simp
   2.421 +  also have "(x + y) * ?rhs mm = (\<Sum>n\<le>mm. ((- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n)))"
   2.422 +    by (subst setsum_right_distrib, rule setsum.cong) (simp_all add: Suc_diff_le)
   2.423 +  also have "\<dots> + (-r gchoose (Suc mm)) * (-x)^Suc mm = 
   2.424 +                 (\<Sum>n\<le>Suc mm. (- r gchoose n) * (- x) ^ n * (x + y) ^ (Suc mm - n))" by simp
   2.425 +  finally show ?case unfolding S_def .
   2.426 +qed simp_all
   2.427 +
   2.428 +lemma gbinomial_partial_sum_poly_xpos:
   2.429 +  "(\<Sum>k\<le>m. (of_nat m + r gchoose k) * x^k * y^(m-k)) = 
   2.430 +     (\<Sum>k\<le>m. (of_nat k + r - 1 gchoose k) * x^k * (x + y)^(m-k))"
   2.431 +  apply (subst gbinomial_partial_sum_poly)
   2.432 +  apply (subst gbinomial_negated_upper)
   2.433 +  apply (intro setsum.cong, rule refl)
   2.434 +  apply (simp add: power_mult_distrib [symmetric])
   2.435 +  done
   2.436 +
   2.437 +lemma setsum_nat_symmetry: 
   2.438 +  "(\<Sum>k = 0..(m::nat). f k) = (\<Sum>k = 0..m. f (m - k))"
   2.439 +  by (rule setsum.reindex_bij_witness[where i="\<lambda>i. m - i" and j="\<lambda>i. m - i"]) auto
   2.440 +
   2.441 +lemma binomial_r_part_sum: "(\<Sum>k\<le>m. (2 * m + 1 choose k)) = 2 ^ (2 * m)"
   2.442 +proof -
   2.443 +  have "2 * 2^(2*m) = (\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k))"
   2.444 +    using choose_row_sum[where n="2 * m + 1"] by simp
   2.445 +  also have "(\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k)) = (\<Sum>k = 0..m. (2 * m + 1 choose k))
   2.446 +                + (\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k))"
   2.447 +    using setsum_ub_add_nat[of 0 m "\<lambda>k. 2 * m + 1 choose k" "m+1"] by (simp add: mult_2)
   2.448 +  also have "(\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k)) =
   2.449 +                 (\<Sum>k = 0..m. (2 * m + 1 choose (k + (m + 1))))"
   2.450 +    by (subst setsum_shift_bounds_cl_nat_ivl [symmetric]) (simp add: mult_2)
   2.451 +  also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose (m - k)))"
   2.452 +    by (intro setsum.cong[OF refl], subst binomial_symmetric) simp_all
   2.453 +  also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose k))"
   2.454 +    by (subst (2) setsum_nat_symmetry) (rule refl)
   2.455 +  also have "\<dots> + \<dots> = 2 * \<dots>" by simp
   2.456 +  finally show ?thesis by (subst (asm) mult_cancel1) (simp add: atLeast0AtMost)
   2.457 +qed
   2.458 +
   2.459 +lemma gbinomial_r_part_sum:
   2.460 +  "(\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k)) = 2 ^ (2 * m)" (is "?lhs = ?rhs")
   2.461 +proof -
   2.462 +  have "?lhs = of_nat (\<Sum>k\<le>m. (2 * m + 1) choose k)" 
   2.463 +    by (simp add: binomial_gbinomial of_nat_mult add_ac of_nat_setsum)
   2.464 +  also have "\<dots> = of_nat (2 ^ (2 * m))" by (subst binomial_r_part_sum) (rule refl)
   2.465 +  finally show ?thesis by (simp add: of_nat_power)
   2.466 +qed
   2.467 +
   2.468 +lemma gbinomial_sum_nat_pow2:
   2.469 +   "(\<Sum>k\<le>m. (of_nat (m + k) gchoose k :: 'a :: field_char_0) / 2 ^ k) = 2 ^ m" (is "?lhs = ?rhs")
   2.470 +proof -
   2.471 +  have "2 ^ m * 2 ^ m = (2 ^ (2*m) :: 'a)" by (induction m) simp_all
   2.472 +  also have "\<dots> = (\<Sum>k\<le>m. (2 * (of_nat m) + 1 gchoose k))" using gbinomial_r_part_sum ..
   2.473 +  also have "\<dots> = (\<Sum>k\<le>m. (of_nat (m + k) gchoose k) * 2 ^ (m - k))"
   2.474 +    using gbinomial_partial_sum_poly_xpos[where x="1" and y="1" and r="of_nat m + 1" and m="m"]
   2.475 +    by (simp add: add_ac)
   2.476 +  also have "\<dots> = 2 ^ m * (\<Sum>k\<le>m. (of_nat (m + k) gchoose k) / 2 ^ k)"
   2.477 +    by (subst setsum_right_distrib) (simp add: algebra_simps power_diff)
   2.478 +  finally show ?thesis by (subst (asm) mult_left_cancel) simp_all
   2.479 +qed
   2.480 +
   2.481 +lemma gbinomial_trinomial_revision:
   2.482 +  assumes "k \<le> m"
   2.483 +  shows   "(r gchoose m) * (of_nat m gchoose k) = (r gchoose k) * (r - of_nat k gchoose (m - k))"
   2.484 +proof -
   2.485 +  have "(r gchoose m) * (of_nat m gchoose k) = 
   2.486 +            (r gchoose m) * fact m / (fact k * fact (m - k))"
   2.487 +    using assms by (simp add: binomial_gbinomial [symmetric] binomial_fact)
   2.488 +  also have "\<dots> = (r gchoose k) * (r - of_nat k gchoose (m - k))" using assms
   2.489 +    by (simp add: gbinomial_pochhammer power_diff pochhammer_product)
   2.490 +  finally show ?thesis .
   2.491 +qed
   2.492 +
   2.493 +
   2.494  text\<open>Versions of the theorems above for the natural-number version of "choose"\<close>
   2.495  lemma binomial_altdef_of_nat:
   2.496    fixes n k :: nat
     3.1 --- a/src/HOL/Complex.thy	Thu Oct 29 15:40:52 2015 +0100
     3.2 +++ b/src/HOL/Complex.thy	Mon Nov 02 11:56:28 2015 +0100
     3.3 @@ -171,6 +171,17 @@
     3.4      "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
     3.5    by (auto simp: Reals_def)
     3.6  
     3.7 +lemma complex_Re_fact [simp]: "Re (fact n) = fact n"
     3.8 +proof -
     3.9 +  have "(fact n :: complex) = of_real (fact n)" by simp
    3.10 +  also have "Re \<dots> = fact n" by (subst Re_complex_of_real) simp_all
    3.11 +  finally show ?thesis .
    3.12 +qed
    3.13 +
    3.14 +lemma complex_Im_fact [simp]: "Im (fact n) = 0"
    3.15 +  by (subst of_nat_fact [symmetric]) (simp only: complex_Im_of_nat)
    3.16 +
    3.17 +
    3.18  subsection \<open>The Complex Number $i$\<close>
    3.19  
    3.20  primcorec "ii" :: complex  ("\<i>") where
    3.21 @@ -497,6 +508,12 @@
    3.22  lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
    3.23    by simp
    3.24  
    3.25 +lemma complex_cnj_fact [simp]: "cnj (fact n) = fact n"
    3.26 +  by (subst of_nat_fact [symmetric], subst complex_cnj_of_nat) simp
    3.27 +
    3.28 +lemma complex_cnj_pochhammer [simp]: "cnj (pochhammer z n) = pochhammer (cnj z) n"
    3.29 +  by (induction n arbitrary: z) (simp_all add: pochhammer_rec)
    3.30 +
    3.31  lemma bounded_linear_cnj: "bounded_linear cnj"
    3.32    using complex_cnj_add complex_cnj_scaleR
    3.33    by (rule bounded_linear_intro [where K=1], simp)
     4.1 --- a/src/HOL/Filter.thy	Thu Oct 29 15:40:52 2015 +0100
     4.2 +++ b/src/HOL/Filter.thy	Mon Nov 02 11:56:28 2015 +0100
     4.3 @@ -393,6 +393,11 @@
     4.4  lemma eventually_happens: "eventually P net \<Longrightarrow> net = bot \<or> (\<exists>x. P x)"
     4.5    by (metis frequentlyE eventually_frequently)
     4.6  
     4.7 +lemma eventually_happens':
     4.8 +  assumes "F \<noteq> bot" "eventually P F"
     4.9 +  shows   "\<exists>x. P x"
    4.10 +  using assms eventually_frequently frequentlyE by blast
    4.11 +
    4.12  abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
    4.13    where "trivial_limit F \<equiv> F = bot"
    4.14  
    4.15 @@ -611,6 +616,15 @@
    4.16  lemma eventually_gt_at_top: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
    4.17    unfolding eventually_at_top_dense by auto
    4.18  
    4.19 +lemma eventually_all_ge_at_top:
    4.20 +  assumes "eventually P (at_top :: ('a :: linorder) filter)"
    4.21 +  shows   "eventually (\<lambda>x. \<forall>y\<ge>x. P y) at_top"
    4.22 +proof -
    4.23 +  from assms obtain x where "\<And>y. y \<ge> x \<Longrightarrow> P y" by (auto simp: eventually_at_top_linorder)
    4.24 +  hence "\<forall>z\<ge>y. P z" if "y \<ge> x" for y using that by simp
    4.25 +  thus ?thesis by (auto simp: eventually_at_top_linorder)
    4.26 +qed
    4.27 +
    4.28  definition at_bot :: "('a::order) filter"
    4.29    where "at_bot = (INF k. principal {.. k})"
    4.30  
     5.1 --- a/src/HOL/Int.thy	Thu Oct 29 15:40:52 2015 +0100
     5.2 +++ b/src/HOL/Int.thy	Mon Nov 02 11:56:28 2015 +0100
     5.3 @@ -225,6 +225,9 @@
     5.4  lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
     5.5    by (transfer fixing: times) (clarsimp simp add: algebra_simps of_nat_mult)
     5.6  
     5.7 +lemma mult_of_int_commute: "of_int x * y = y * of_int x"
     5.8 +  by (transfer fixing: times) (auto simp: algebra_simps mult_of_nat_commute)
     5.9 +
    5.10  text\<open>Collapse nested embeddings\<close>
    5.11  lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
    5.12  by (induct n) auto
     6.1 --- a/src/HOL/Library/Convex.thy	Thu Oct 29 15:40:52 2015 +0100
     6.2 +++ b/src/HOL/Library/Convex.thy	Mon Nov 02 11:56:28 2015 +0100
     6.3 @@ -304,6 +304,42 @@
     6.4    where "convex_on s f \<longleftrightarrow>
     6.5      (\<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)"
     6.6  
     6.7 +lemma convex_onI [intro?]:
     6.8 +  assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
     6.9 +             f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
    6.10 +  shows   "convex_on A f"
    6.11 +  unfolding convex_on_def
    6.12 +proof clarify
    6.13 +  fix x y u v assume A: "x \<in> A" "y \<in> A" "(u::real) \<ge> 0" "v \<ge> 0" "u + v = 1"
    6.14 +  from A(5) have [simp]: "v = 1 - u" by (simp add: algebra_simps)
    6.15 +  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]
    6.16 +    by (cases "u = 0 \<or> u = 1") (auto simp: algebra_simps)
    6.17 +qed
    6.18 +
    6.19 +lemma convex_on_linorderI [intro?]:
    6.20 +  fixes A :: "('a::{linorder,real_vector}) set"
    6.21 +  assumes "\<And>t x y. t > 0 \<Longrightarrow> t < 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x < y \<Longrightarrow>
    6.22 +             f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
    6.23 +  shows   "convex_on A f"
    6.24 +proof
    6.25 +  fix t x y assume A: "x \<in> A" "y \<in> A" "(t::real) > 0" "t < 1"
    6.26 +  case (goal1 t x y)
    6.27 +  with goal1 assms[of t x y] assms[of "1 - t" y x]
    6.28 +    show ?case by (cases x y rule: linorder_cases) (auto simp: algebra_simps)
    6.29 +qed
    6.30 +
    6.31 +lemma convex_onD:
    6.32 +  assumes "convex_on A f"
    6.33 +  shows   "\<And>t x y. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow>
    6.34 +             f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
    6.35 +  using assms unfolding convex_on_def by auto
    6.36 +
    6.37 +lemma convex_onD_Icc:
    6.38 +  assumes "convex_on {x..y} f" "x \<le> (y :: _ :: {real_vector,preorder})"
    6.39 +  shows   "\<And>t. t \<ge> 0 \<Longrightarrow> t \<le> 1 \<Longrightarrow>
    6.40 +             f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \<le> (1 - t) * f x + t * f y"
    6.41 +  using assms(2) by (intro convex_onD[OF assms(1)]) simp_all
    6.42 +
    6.43  lemma convex_on_subset: "convex_on t f \<Longrightarrow> s \<subseteq> t \<Longrightarrow> convex_on s f"
    6.44    unfolding convex_on_def by auto
    6.45  
    6.46 @@ -835,4 +871,91 @@
    6.47    show ?thesis by auto
    6.48  qed
    6.49  
    6.50 +
    6.51 +subsection \<open>Convexity of real functions\<close>
    6.52 +
    6.53 +lemma convex_on_realI:
    6.54 +  assumes "connected A"
    6.55 +  assumes "\<And>x. x \<in> A \<Longrightarrow> (f has_real_derivative f' x) (at x)"
    6.56 +  assumes "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<le> y \<Longrightarrow> f' x \<le> f' y"
    6.57 +  shows   "convex_on A f"
    6.58 +proof (rule convex_on_linorderI)
    6.59 +  fix t x y :: real
    6.60 +  assume t: "t > 0" "t < 1" and xy: "x \<in> A" "y \<in> A" "x < y"
    6.61 +  def z \<equiv> "(1 - t) * x + t * y"
    6.62 +  with `connected A` and xy have ivl: "{x..y} \<subseteq> A" using connected_contains_Icc by blast
    6.63 +  
    6.64 +  from xy t have xz: "z > x" by (simp add: z_def algebra_simps)
    6.65 +  have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps)
    6.66 +  also from xy t have "... > 0" by (intro mult_pos_pos) simp_all
    6.67 +  finally have yz: "z < y" by simp
    6.68 +    
    6.69 +  from assms xz yz ivl t have "\<exists>\<xi>. \<xi> > x \<and> \<xi> < z \<and> f z - f x = (z - x) * f' \<xi>"
    6.70 +    by (intro MVT2) (auto intro!: assms(2))
    6.71 +  then obtain \<xi> where \<xi>: "\<xi> > x" "\<xi> < z" "f' \<xi> = (f z - f x) / (z - x)" by auto
    6.72 +  from assms xz yz ivl t have "\<exists>\<eta>. \<eta> > z \<and> \<eta> < y \<and> f y - f z = (y - z) * f' \<eta>"
    6.73 +    by (intro MVT2) (auto intro!: assms(2))
    6.74 +  then obtain \<eta> where \<eta>: "\<eta> > z" "\<eta> < y" "f' \<eta> = (f y - f z) / (y - z)" by auto
    6.75 +  
    6.76 +  from \<eta>(3) have "(f y - f z) / (y - z) = f' \<eta>" ..
    6.77 +  also from \<xi> \<eta> ivl have "\<xi> \<in> A" "\<eta> \<in> A" by auto
    6.78 +  with \<xi> \<eta> have "f' \<eta> \<ge> f' \<xi>" by (intro assms(3)) auto
    6.79 +  also from \<xi>(3) have "f' \<xi> = (f z - f x) / (z - x)" .
    6.80 +  finally have "(f y - f z) * (z - x) \<ge> (f z - f x) * (y - z)"
    6.81 +    using xz yz by (simp add: field_simps)
    6.82 +  also have "z - x = t * (y - x)" by (simp add: z_def algebra_simps)
    6.83 +  also have "y - z = (1 - t) * (y - x)" by (simp add: z_def algebra_simps)
    6.84 +  finally have "(f y - f z) * t \<ge> (f z - f x) * (1 - t)" using xy by simp
    6.85 +  thus "(1 - t) * f x + t * f y \<ge> f ((1 - t) *\<^sub>R x + t *\<^sub>R y)"
    6.86 +    by (simp add: z_def algebra_simps)
    6.87 +qed
    6.88 +
    6.89 +lemma convex_on_inverse:
    6.90 +  assumes "A \<subseteq> {0<..}"
    6.91 +  shows   "convex_on A (inverse :: real \<Rightarrow> real)"
    6.92 +proof (rule convex_on_subset[OF _ assms], intro convex_on_realI[of _ _ "\<lambda>x. -inverse (x^2)"])
    6.93 +  fix u v :: real assume "u \<in> {0<..}" "v \<in> {0<..}" "u \<le> v"
    6.94 +  with assms show "-inverse (u^2) \<le> -inverse (v^2)"
    6.95 +    by (intro le_imp_neg_le le_imp_inverse_le power_mono) (simp_all)
    6.96 +qed (insert assms, auto intro!: derivative_eq_intros simp: divide_simps power2_eq_square)
    6.97 +
    6.98 +lemma convex_onD_Icc':
    6.99 +  assumes "convex_on {x..y} f" "c \<in> {x..y}"
   6.100 +  defines "d \<equiv> y - x"
   6.101 +  shows   "f c \<le> (f y - f x) / d * (c - x) + f x"
   6.102 +proof (cases y x rule: linorder_cases)
   6.103 +  assume less: "x < y"
   6.104 +  hence d: "d > 0" by (simp add: d_def)
   6.105 +  from assms(2) less have A: "0 \<le> (c - x) / d" "(c - x) / d \<le> 1" 
   6.106 +    by (simp_all add: d_def divide_simps)
   6.107 +  have "f c = f (x + (c - x) * 1)" by simp
   6.108 +  also from less have "1 = ((y - x) / d)" by (simp add: d_def)
   6.109 +  also from d have "x + (c - x) * \<dots> = (1 - (c - x) / d) *\<^sub>R x + ((c - x) / d) *\<^sub>R y" 
   6.110 +    by (simp add: field_simps)
   6.111 +  also have "f \<dots> \<le> (1 - (c - x) / d) * f x + (c - x) / d * f y" using assms less
   6.112 +    by (intro convex_onD_Icc) simp_all
   6.113 +  also from d have "\<dots> = (f y - f x) / d * (c - x) + f x" by (simp add: field_simps)
   6.114 +  finally show ?thesis .
   6.115 +qed (insert assms(2), simp_all)
   6.116 +
   6.117 +lemma convex_onD_Icc'':
   6.118 +  assumes "convex_on {x..y} f" "c \<in> {x..y}"
   6.119 +  defines "d \<equiv> y - x"
   6.120 +  shows   "f c \<le> (f x - f y) / d * (y - c) + f y"
   6.121 +proof (cases y x rule: linorder_cases)
   6.122 +  assume less: "x < y"
   6.123 +  hence d: "d > 0" by (simp add: d_def)
   6.124 +  from assms(2) less have A: "0 \<le> (y - c) / d" "(y - c) / d \<le> 1" 
   6.125 +    by (simp_all add: d_def divide_simps)
   6.126 +  have "f c = f (y - (y - c) * 1)" by simp
   6.127 +  also from less have "1 = ((y - x) / d)" by (simp add: d_def)
   6.128 +  also from d have "y - (y - c) * \<dots> = (1 - (1 - (y - c) / d)) *\<^sub>R x + (1 - (y - c) / d) *\<^sub>R y" 
   6.129 +    by (simp add: field_simps)
   6.130 +  also have "f \<dots> \<le> (1 - (1 - (y - c) / d)) * f x + (1 - (y - c) / d) * f y" using assms less
   6.131 +    by (intro convex_onD_Icc) (simp_all add: field_simps)
   6.132 +  also from d have "\<dots> = (f x - f y) / d * (y - c) + f y" by (simp add: field_simps)
   6.133 +  finally show ?thesis .
   6.134 +qed (insert assms(2), simp_all)
   6.135 +
   6.136 +
   6.137  end
     7.1 --- a/src/HOL/Limits.thy	Thu Oct 29 15:40:52 2015 +0100
     7.2 +++ b/src/HOL/Limits.thy	Mon Nov 02 11:56:28 2015 +0100
     7.3 @@ -137,12 +137,34 @@
     7.4      by (auto elim!: allE[of _ n])
     7.5  qed
     7.6  
     7.7 +lemma Bseq_bdd_above': 
     7.8 +  "Bseq (X::nat \<Rightarrow> 'a :: real_normed_vector) \<Longrightarrow> bdd_above (range (\<lambda>n. norm (X n)))"
     7.9 +proof (elim BseqE, intro bdd_aboveI2)
    7.10 +  fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "norm (X n) \<le> K"
    7.11 +    by (auto elim!: allE[of _ n])
    7.12 +qed
    7.13 +
    7.14  lemma Bseq_bdd_below: "Bseq (X::nat \<Rightarrow> real) \<Longrightarrow> bdd_below (range X)"
    7.15  proof (elim BseqE, intro bdd_belowI2)
    7.16    fix K n assume "0 < K" "\<forall>n. norm (X n) \<le> K" then show "- K \<le> X n"
    7.17      by (auto elim!: allE[of _ n])
    7.18  qed
    7.19  
    7.20 +lemma Bseq_eventually_mono:
    7.21 +  assumes "eventually (\<lambda>n. norm (f n) \<le> norm (g n)) sequentially" "Bseq g"
    7.22 +  shows   "Bseq f" 
    7.23 +proof -
    7.24 +  from assms(1) obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> norm (f n) \<le> norm (g n)"
    7.25 +    by (auto simp: eventually_at_top_linorder)
    7.26 +  moreover from assms(2) obtain K where K: "\<And>n. norm (g n) \<le> K" by (blast elim!: BseqE)
    7.27 +  ultimately have "norm (f n) \<le> max K (Max {norm (f n) |n. n < N})" for n
    7.28 +    apply (cases "n < N")
    7.29 +    apply (rule max.coboundedI2, rule Max.coboundedI, auto) []
    7.30 +    apply (rule max.coboundedI1, force intro: order.trans[OF N K])
    7.31 +    done
    7.32 +  thus ?thesis by (blast intro: BseqI') 
    7.33 +qed
    7.34 +
    7.35  lemma lemma_NBseq_def:
    7.36    "(\<exists>K > 0. \<forall>n. norm (X n) \<le> K) = (\<exists>N. \<forall>n. norm (X n) \<le> real(Suc N))"
    7.37  proof safe
    7.38 @@ -218,6 +240,73 @@
    7.39  lemma Bseq_minus_iff: "Bseq (%n. -(X n) :: 'a :: real_normed_vector) = Bseq X"
    7.40    by (simp add: Bseq_def)
    7.41  
    7.42 +lemma Bseq_add: 
    7.43 +  assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
    7.44 +  shows   "Bseq (\<lambda>x. f x + c)"
    7.45 +proof -
    7.46 +  from assms obtain K where K: "\<And>x. norm (f x) \<le> K" unfolding Bseq_def by blast
    7.47 +  {
    7.48 +    fix x :: nat
    7.49 +    have "norm (f x + c) \<le> norm (f x) + norm c" by (rule norm_triangle_ineq)
    7.50 +    also have "norm (f x) \<le> K" by (rule K)
    7.51 +    finally have "norm (f x + c) \<le> K + norm c" by simp
    7.52 +  }
    7.53 +  thus ?thesis by (rule BseqI')
    7.54 +qed
    7.55 +
    7.56 +lemma Bseq_add_iff: "Bseq (\<lambda>x. f x + c) \<longleftrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
    7.57 +  using Bseq_add[of f c] Bseq_add[of "\<lambda>x. f x + c" "-c"] by auto
    7.58 +
    7.59 +lemma Bseq_mult: 
    7.60 +  assumes "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_field)"
    7.61 +  assumes "Bseq (g :: nat \<Rightarrow> 'a :: real_normed_field)"
    7.62 +  shows   "Bseq (\<lambda>x. f x * g x)"
    7.63 +proof -
    7.64 +  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" 
    7.65 +    unfolding Bseq_def by blast
    7.66 +  hence "\<And>x. norm (f x * g x) \<le> K1 * K2" by (auto simp: norm_mult intro!: mult_mono)
    7.67 +  thus ?thesis by (rule BseqI')
    7.68 +qed
    7.69 +
    7.70 +lemma Bfun_const [simp]: "Bfun (\<lambda>_. c) F"
    7.71 +  unfolding Bfun_metric_def by (auto intro!: exI[of _ c] exI[of _ "1::real"])
    7.72 +
    7.73 +lemma Bseq_cmult_iff: "(c :: 'a :: real_normed_field) \<noteq> 0 \<Longrightarrow> Bseq (\<lambda>x. c * f x) \<longleftrightarrow> Bseq f"
    7.74 +proof
    7.75 +  assume "c \<noteq> 0" "Bseq (\<lambda>x. c * f x)"
    7.76 +  find_theorems "Bfun (\<lambda>_. ?c) _"
    7.77 +  from Bfun_const this(2) have "Bseq (\<lambda>x. inverse c * (c * f x))" by (rule Bseq_mult)
    7.78 +  with `c \<noteq> 0` show "Bseq f" by (simp add: divide_simps)
    7.79 +qed (intro Bseq_mult Bfun_const)
    7.80 +
    7.81 +lemma Bseq_subseq: "Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector) \<Longrightarrow> Bseq (\<lambda>x. f (g x))"
    7.82 +  unfolding Bseq_def by auto
    7.83 +
    7.84 +lemma Bseq_Suc_iff: "Bseq (\<lambda>n. f (Suc n)) \<longleftrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
    7.85 +  using Bseq_offset[of f 1] by (auto intro: Bseq_subseq)
    7.86 +
    7.87 +lemma increasing_Bseq_subseq_iff:
    7.88 +  assumes "\<And>x y. x \<le> y \<Longrightarrow> norm (f x :: 'a :: real_normed_vector) \<le> norm (f y)" "subseq g"
    7.89 +  shows   "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f"
    7.90 +proof
    7.91 +  assume "Bseq (\<lambda>x. f (g x))"
    7.92 +  then obtain K where K: "\<And>x. norm (f (g x)) \<le> K" unfolding Bseq_def by auto
    7.93 +  {
    7.94 +    fix x :: nat
    7.95 +    from filterlim_subseq[OF assms(2)] obtain y where "g y \<ge> x"
    7.96 +      by (auto simp: filterlim_at_top eventually_at_top_linorder)
    7.97 +    hence "norm (f x) \<le> norm (f (g y))" using assms(1) by blast
    7.98 +    also have "norm (f (g y)) \<le> K" by (rule K)
    7.99 +    finally have "norm (f x) \<le> K" .
   7.100 +  }
   7.101 +  thus "Bseq f" by (rule BseqI')
   7.102 +qed (insert Bseq_subseq[of f g], simp_all)
   7.103 +
   7.104 +lemma nonneg_incseq_Bseq_subseq_iff:
   7.105 +  assumes "\<And>x. f x \<ge> 0" "incseq (f :: nat \<Rightarrow> real)" "subseq g"
   7.106 +  shows   "Bseq (\<lambda>x. f (g x)) \<longleftrightarrow> Bseq f"
   7.107 +  using assms by (intro increasing_Bseq_subseq_iff) (auto simp: incseq_def)
   7.108 +
   7.109  lemma Bseq_eq_bounded: "range f \<subseteq> {a .. b::real} \<Longrightarrow> Bseq f"
   7.110    apply (simp add: subset_eq)
   7.111    apply (rule BseqI'[where K="max (norm a) (norm b)"])
   7.112 @@ -679,6 +768,16 @@
   7.113    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)"
   7.114    unfolding continuous_on_def by (auto intro: tendsto_setprod)
   7.115  
   7.116 +lemma tendsto_of_real_iff:
   7.117 +  "((\<lambda>x. of_real (f x) :: 'a :: real_normed_div_algebra) ---> of_real c) F \<longleftrightarrow> (f ---> c) F"
   7.118 +  unfolding tendsto_iff by simp
   7.119 +
   7.120 +lemma tendsto_add_const_iff:
   7.121 +  "((\<lambda>x. c + f x :: 'a :: real_normed_vector) ---> c + d) F \<longleftrightarrow> (f ---> d) F"
   7.122 +  using tendsto_add[OF tendsto_const[of c], of f d] 
   7.123 +        tendsto_add[OF tendsto_const[of "-c"], of "\<lambda>x. c + f x" "c + d"] by auto
   7.124 +
   7.125 +
   7.126  subsubsection \<open>Inverse and division\<close>
   7.127  
   7.128  lemma (in bounded_bilinear) Zfun_prod_Bfun:
   7.129 @@ -892,6 +991,55 @@
   7.130    qed
   7.131  qed force
   7.132  
   7.133 +lemma not_tendsto_and_filterlim_at_infinity:
   7.134 +  assumes "F \<noteq> bot"
   7.135 +  assumes "(f ---> (c :: 'a :: real_normed_vector)) F" 
   7.136 +  assumes "filterlim f at_infinity F"
   7.137 +  shows   False
   7.138 +proof -
   7.139 +  from tendstoD[OF assms(2), of "1/2"] 
   7.140 +    have "eventually (\<lambda>x. dist (f x) c < 1/2) F" by simp
   7.141 +  moreover from filterlim_at_infinity[of "norm c" f F] assms(3)
   7.142 +    have "eventually (\<lambda>x. norm (f x) \<ge> norm c + 1) F" by simp
   7.143 +  ultimately have "eventually (\<lambda>x. False) F"
   7.144 +  proof eventually_elim
   7.145 +    fix x assume A: "dist (f x) c < 1/2" and B: "norm (f x) \<ge> norm c + 1"
   7.146 +    note B
   7.147 +    also have "norm (f x) = dist (f x) 0" by (simp add: norm_conv_dist)
   7.148 +    also have "... \<le> dist (f x) c + dist c 0" by (rule dist_triangle)
   7.149 +    also note A
   7.150 +    finally show False by (simp add: norm_conv_dist)
   7.151 +  qed
   7.152 +  with assms show False by simp
   7.153 +qed
   7.154 +
   7.155 +lemma filterlim_at_infinity_imp_not_convergent:
   7.156 +  assumes "filterlim f at_infinity sequentially"
   7.157 +  shows   "\<not>convergent f"
   7.158 +  by (rule notI, rule not_tendsto_and_filterlim_at_infinity[OF _ _ assms])
   7.159 +     (simp_all add: convergent_LIMSEQ_iff)
   7.160 +
   7.161 +lemma filterlim_at_infinity_imp_eventually_ne:
   7.162 +  assumes "filterlim f at_infinity F"
   7.163 +  shows   "eventually (\<lambda>z. f z \<noteq> c) F"
   7.164 +proof -
   7.165 +  have "norm c + 1 > 0" by (intro add_nonneg_pos) simp_all
   7.166 +  with filterlim_at_infinity[OF order.refl, of f F] assms
   7.167 +    have "eventually (\<lambda>z. norm (f z) \<ge> norm c + 1) F" by blast
   7.168 +  thus ?thesis by eventually_elim auto
   7.169 +qed
   7.170 +
   7.171 +lemma tendsto_of_nat [tendsto_intros]: 
   7.172 +  "filterlim (of_nat :: nat \<Rightarrow> 'a :: real_normed_algebra_1) at_infinity sequentially"
   7.173 +proof (subst filterlim_at_infinity[OF order.refl], intro allI impI)
   7.174 +  fix r :: real assume r: "r > 0"
   7.175 +  def n \<equiv> "nat \<lceil>r\<rceil>"
   7.176 +  from r have n: "\<forall>m\<ge>n. of_nat m \<ge> r" unfolding n_def by linarith
   7.177 +  from eventually_ge_at_top[of n] show "eventually (\<lambda>m. norm (of_nat m :: 'a) \<ge> r) sequentially"
   7.178 +    by eventually_elim (insert n, simp_all)
   7.179 +qed
   7.180 +
   7.181 +
   7.182  subsection \<open>Relate @{const at}, @{const at_left} and @{const at_right}\<close>
   7.183  
   7.184  text \<open>
   7.185 @@ -1075,9 +1223,27 @@
   7.186      by (auto intro: order_trans simp: filterlim_def filtermap_filtermap)
   7.187  qed
   7.188  
   7.189 +lemma tendsto_mult_filterlim_at_infinity:
   7.190 +  assumes "F \<noteq> bot" "(f ---> (c :: 'a :: real_normed_field)) F" "c \<noteq> 0"
   7.191 +  assumes "filterlim g at_infinity F"
   7.192 +  shows   "filterlim (\<lambda>x. f x * g x) at_infinity F"
   7.193 +proof -
   7.194 +  have "((\<lambda>x. inverse (f x) * inverse (g x)) ---> inverse c * 0) F"
   7.195 +    by (intro tendsto_mult tendsto_inverse assms filterlim_compose[OF tendsto_inverse_0])
   7.196 +  hence "filterlim (\<lambda>x. inverse (f x) * inverse (g x)) (at (inverse c * 0)) F"
   7.197 +    unfolding filterlim_at using assms
   7.198 +    by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
   7.199 +  thus ?thesis by (subst filterlim_inverse_at_iff[symmetric]) simp_all
   7.200 +qed
   7.201 +
   7.202  lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) ---> 0) F"
   7.203   by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
   7.204  
   7.205 +lemma mult_nat_left_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. c * x :: nat) at_top sequentially"
   7.206 +  by (rule filterlim_subseq) (auto simp: subseq_def)
   7.207 +
   7.208 +lemma mult_nat_right_at_top: "c > 0 \<Longrightarrow> filterlim (\<lambda>x. x * c :: nat) at_top sequentially"
   7.209 +  by (rule filterlim_subseq) (auto simp: subseq_def)
   7.210  
   7.211  lemma at_to_infinity:
   7.212    fixes x :: "'a :: {real_normed_field,field}"
   7.213 @@ -1471,6 +1637,23 @@
   7.214  
   7.215  subsection \<open>Convergence on sequences\<close>
   7.216  
   7.217 +lemma convergent_cong:
   7.218 +  assumes "eventually (\<lambda>x. f x = g x) sequentially"
   7.219 +  shows   "convergent f \<longleftrightarrow> convergent g"
   7.220 +  unfolding convergent_def by (subst filterlim_cong[OF refl refl assms]) (rule refl)
   7.221 +
   7.222 +lemma convergent_Suc_iff: "convergent (\<lambda>n. f (Suc n)) \<longleftrightarrow> convergent f"
   7.223 +  by (auto simp: convergent_def LIMSEQ_Suc_iff)
   7.224 +
   7.225 +lemma convergent_ignore_initial_segment: "convergent (\<lambda>n. f (n + m)) = convergent f"
   7.226 +proof (induction m arbitrary: f)
   7.227 +  case (Suc m)
   7.228 +  have "convergent (\<lambda>n. f (n + Suc m)) \<longleftrightarrow> convergent (\<lambda>n. f (Suc n + m))" by simp
   7.229 +  also have "\<dots> \<longleftrightarrow> convergent (\<lambda>n. f (n + m))" by (rule convergent_Suc_iff)
   7.230 +  also have "\<dots> \<longleftrightarrow> convergent f" by (rule Suc)
   7.231 +  finally show ?case .
   7.232 +qed simp_all
   7.233 +
   7.234  lemma convergent_add:
   7.235    fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
   7.236    assumes "convergent (\<lambda>n. X n)"
   7.237 @@ -1505,6 +1688,71 @@
   7.238  apply (drule tendsto_minus, auto)
   7.239  done
   7.240  
   7.241 +lemma convergent_diff:
   7.242 +  fixes X Y :: "nat \<Rightarrow> 'a::real_normed_vector"
   7.243 +  assumes "convergent (\<lambda>n. X n)"
   7.244 +  assumes "convergent (\<lambda>n. Y n)"
   7.245 +  shows "convergent (\<lambda>n. X n - Y n)"
   7.246 +  using assms unfolding convergent_def by (fast intro: tendsto_diff)
   7.247 +
   7.248 +lemma convergent_norm:
   7.249 +  assumes "convergent f"
   7.250 +  shows   "convergent (\<lambda>n. norm (f n))"
   7.251 +proof -
   7.252 +  from assms have "f ----> lim f" by (simp add: convergent_LIMSEQ_iff)
   7.253 +  hence "(\<lambda>n. norm (f n)) ----> norm (lim f)" by (rule tendsto_norm)
   7.254 +  thus ?thesis by (auto simp: convergent_def)
   7.255 +qed
   7.256 +
   7.257 +lemma convergent_of_real: 
   7.258 +  "convergent f \<Longrightarrow> convergent (\<lambda>n. of_real (f n) :: 'a :: real_normed_algebra_1)"
   7.259 +  unfolding convergent_def by (blast intro!: tendsto_of_real)
   7.260 +
   7.261 +lemma convergent_add_const_iff: 
   7.262 +  "convergent (\<lambda>n. c + f n :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
   7.263 +proof
   7.264 +  assume "convergent (\<lambda>n. c + f n)"
   7.265 +  from convergent_diff[OF this convergent_const[of c]] show "convergent f" by simp
   7.266 +next
   7.267 +  assume "convergent f"
   7.268 +  from convergent_add[OF convergent_const[of c] this] show "convergent (\<lambda>n. c + f n)" by simp
   7.269 +qed
   7.270 +
   7.271 +lemma convergent_add_const_right_iff: 
   7.272 +  "convergent (\<lambda>n. f n + c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
   7.273 +  using convergent_add_const_iff[of c f] by (simp add: add_ac)
   7.274 +
   7.275 +lemma convergent_diff_const_right_iff: 
   7.276 +  "convergent (\<lambda>n. f n - c :: 'a :: real_normed_vector) \<longleftrightarrow> convergent f"
   7.277 +  using convergent_add_const_right_iff[of f "-c"] by (simp add: add_ac)
   7.278 +
   7.279 +lemma convergent_mult:
   7.280 +  fixes X Y :: "nat \<Rightarrow> 'a::real_normed_field"
   7.281 +  assumes "convergent (\<lambda>n. X n)"
   7.282 +  assumes "convergent (\<lambda>n. Y n)"
   7.283 +  shows "convergent (\<lambda>n. X n * Y n)"
   7.284 +  using assms unfolding convergent_def by (fast intro: tendsto_mult)
   7.285 +
   7.286 +lemma convergent_mult_const_iff:
   7.287 +  assumes "c \<noteq> 0"
   7.288 +  shows   "convergent (\<lambda>n. c * f n :: 'a :: real_normed_field) \<longleftrightarrow> convergent f"
   7.289 +proof
   7.290 +  assume "convergent (\<lambda>n. c * f n)"
   7.291 +  from assms convergent_mult[OF this convergent_const[of "inverse c"]] 
   7.292 +    show "convergent f" by (simp add: field_simps)
   7.293 +next
   7.294 +  assume "convergent f"
   7.295 +  from convergent_mult[OF convergent_const[of c] this] show "convergent (\<lambda>n. c * f n)" by simp
   7.296 +qed
   7.297 +
   7.298 +lemma convergent_mult_const_right_iff:
   7.299 +  assumes "c \<noteq> 0"
   7.300 +  shows   "convergent (\<lambda>n. (f n :: 'a :: real_normed_field) * c) \<longleftrightarrow> convergent f"
   7.301 +  using convergent_mult_const_iff[OF assms, of f] by (simp add: mult_ac)
   7.302 +
   7.303 +lemma convergent_imp_Bseq: "convergent f \<Longrightarrow> Bseq f"
   7.304 +  by (simp add: Cauchy_Bseq convergent_Cauchy)
   7.305 +
   7.306  
   7.307  text \<open>A monotone sequence converges to its least upper bound.\<close>
   7.308  
   7.309 @@ -1532,6 +1780,19 @@
   7.310  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)"
   7.311    by (auto intro!: Bseq_monoseq_convergent incseq_imp_monoseq simp: incseq_def)
   7.312  
   7.313 +lemma monoseq_imp_convergent_iff_Bseq: "monoseq (f :: nat \<Rightarrow> real) \<Longrightarrow> convergent f \<longleftrightarrow> Bseq f"
   7.314 +  using Bseq_monoseq_convergent[of f] convergent_imp_Bseq[of f] by blast
   7.315 +
   7.316 +lemma Bseq_monoseq_convergent'_inc:
   7.317 +  "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"
   7.318 +  by (subst convergent_ignore_initial_segment [symmetric, of _ M])
   7.319 +     (auto intro!: Bseq_monoseq_convergent simp: monoseq_def)
   7.320 +
   7.321 +lemma Bseq_monoseq_convergent'_dec:
   7.322 +  "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"
   7.323 +  by (subst convergent_ignore_initial_segment [symmetric, of _ M])
   7.324 +     (auto intro!: Bseq_monoseq_convergent simp: monoseq_def)
   7.325 +
   7.326  lemma Cauchy_iff:
   7.327    fixes X :: "nat \<Rightarrow> 'a::real_normed_vector"
   7.328    shows "Cauchy X \<longleftrightarrow> (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. norm (X m - X n) < e)"
     8.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Thu Oct 29 15:40:52 2015 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Mon Nov 02 11:56:28 2015 +0100
     8.3 @@ -819,6 +819,7 @@
     8.4  
     8.5  subsection\<open>Complex differentiation of sequences and series\<close>
     8.6  
     8.7 +(* TODO: Could probably be simplified using Uniform_Limit *)
     8.8  lemma has_complex_derivative_sequence:
     8.9    fixes s :: "complex set"
    8.10    assumes cvs: "convex s"
    8.11 @@ -899,6 +900,41 @@
    8.12    qed
    8.13  qed
    8.14  
    8.15 +
    8.16 +lemma complex_differentiable_series:
    8.17 +  fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
    8.18 +  assumes "convex s" "open s"
    8.19 +  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
    8.20 +  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
    8.21 +  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
    8.22 +  shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)"
    8.23 +proof -
    8.24 +  from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
    8.25 +    unfolding uniformly_convergent_on_def by blast
    8.26 +  from x and `open s` have s: "at x within s = at x" by (rule at_within_open)
    8.27 +  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)"
    8.28 +    by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
    8.29 +  then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
    8.30 +    "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
    8.31 +  from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
    8.32 +  from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
    8.33 +    by (simp add: has_field_derivative_def s)
    8.34 +  have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
    8.35 +    by (rule has_derivative_transform_within_open[OF `open s` x _ g'])
    8.36 +       (insert g, auto simp: sums_iff)
    8.37 +  thus "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x)" unfolding differentiable_def
    8.38 +    by (auto simp: summable_def complex_differentiable_def has_field_derivative_def)
    8.39 +qed
    8.40 +
    8.41 +lemma complex_differentiable_series':
    8.42 +  fixes f :: "nat \<Rightarrow> complex \<Rightarrow> complex"
    8.43 +  assumes "convex s" "open s"
    8.44 +  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
    8.45 +  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
    8.46 +  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
    8.47 +  shows   "(\<lambda>x. \<Sum>n. f n x) complex_differentiable (at x0)"
    8.48 +  using complex_differentiable_series[OF assms, of x0] `x0 \<in> s` by blast+
    8.49 +
    8.50  subsection\<open>Bound theorem\<close>
    8.51  
    8.52  lemma complex_differentiable_bound:
     9.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Oct 29 15:40:52 2015 +0100
     9.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Mon Nov 02 11:56:28 2015 +0100
     9.3 @@ -1788,14 +1788,6 @@
     9.4  
     9.5  subsubsection \<open>Another formulation from Lars Schewe\<close>
     9.6  
     9.7 -lemma setsum_constant_scaleR:
     9.8 -  fixes y :: "'a::real_vector"
     9.9 -  shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
    9.10 -  apply (cases "finite A")
    9.11 -  apply (induct set: finite)
    9.12 -  apply (simp_all add: algebra_simps)
    9.13 -  done
    9.14 -
    9.15  lemma convex_hull_explicit:
    9.16    fixes p :: "'a::real_vector set"
    9.17    shows "convex hull p =
    10.1 --- a/src/HOL/Multivariate_Analysis/Derivative.thy	Thu Oct 29 15:40:52 2015 +0100
    10.2 +++ b/src/HOL/Multivariate_Analysis/Derivative.thy	Mon Nov 02 11:56:28 2015 +0100
    10.3 @@ -6,7 +6,7 @@
    10.4  section \<open>Multivariate calculus in Euclidean space\<close>
    10.5  
    10.6  theory Derivative
    10.7 -imports Brouwer_Fixpoint Operator_Norm
    10.8 +imports Brouwer_Fixpoint Operator_Norm "~~/src/HOL/Multivariate_Analysis/Uniform_Limit"
    10.9  begin
   10.10  
   10.11  lemma netlimit_at_vector: (* TODO: move *)
   10.12 @@ -2202,6 +2202,92 @@
   10.13    apply auto
   10.14    done
   10.15  
   10.16 +lemma has_field_derivative_series:
   10.17 +  fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
   10.18 +  assumes "convex s"
   10.19 +  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
   10.20 +  assumes "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
   10.21 +  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
   10.22 +  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)"
   10.23 +unfolding has_field_derivative_def
   10.24 +proof (rule has_derivative_series)
   10.25 +  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"
   10.26 +  proof (intro allI impI)
   10.27 +    fix e :: real assume "e > 0"
   10.28 +    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"
   10.29 +      unfolding uniform_limit_iff eventually_at_top_linorder dist_norm by blast
   10.30 +    {
   10.31 +      fix n :: nat and x h :: 'a assume nx: "n \<ge> N" "x \<in> s"
   10.32 +      have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) = norm ((\<Sum>i<n. f' i x) - g' x) * norm h"
   10.33 +        by (simp add: norm_mult [symmetric] ring_distribs setsum_left_distrib)
   10.34 +      also from N[OF nx] have "norm ((\<Sum>i<n. f' i x) - g' x) \<le> e" by simp
   10.35 +      hence "norm ((\<Sum>i<n. f' i x) - g' x) * norm h \<le> e * norm h" 
   10.36 +        by (intro mult_right_mono) simp_all
   10.37 +      finally have "norm ((\<Sum>i<n. f' i x * h) - g' x * h) \<le> e * norm h" .
   10.38 +    }
   10.39 +    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
   10.40 +  qed
   10.41 +qed (insert assms, auto simp: has_field_derivative_def)
   10.42 +
   10.43 +lemma has_field_derivative_series':
   10.44 +  fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
   10.45 +  assumes "convex s"
   10.46 +  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x within s)"
   10.47 +  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
   10.48 +  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" "x \<in> interior s"
   10.49 +  shows   "summable (\<lambda>n. f n x)" "((\<lambda>x. \<Sum>n. f n x) has_field_derivative (\<Sum>n. f' n x)) (at x)"
   10.50 +proof -
   10.51 +  from \<open>x \<in> interior s\<close> have "x \<in> s" using interior_subset by blast
   10.52 +  def g' \<equiv> "\<lambda>x. \<Sum>i. f' i x"
   10.53 +  from assms(3) have "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
   10.54 +    by (simp add: uniformly_convergent_uniform_limit_iff suminf_eq_lim g'_def)
   10.55 +  from has_field_derivative_series[OF assms(1,2) this assms(4,5)] obtain g where g:
   10.56 +    "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
   10.57 +    "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
   10.58 +  from g(1)[OF \<open>x \<in> s\<close>] show "summable (\<lambda>n. f n x)" by (simp add: sums_iff)
   10.59 +  from g(2)[OF \<open>x \<in> s\<close>] \<open>x \<in> interior s\<close> have "(g has_field_derivative g' x) (at x)" 
   10.60 +    by (simp add: at_within_interior[of x s])
   10.61 +  also have "(g has_field_derivative g' x) (at x) \<longleftrightarrow> 
   10.62 +                ((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)"
   10.63 +    using eventually_nhds_in_nhd[OF \<open>x \<in> interior s\<close>] interior_subset[of s] g(1)
   10.64 +    by (intro DERIV_cong_ev) (auto elim!: eventually_elim1 simp: sums_iff)
   10.65 +  finally show "((\<lambda>x. \<Sum>n. f n x) has_field_derivative g' x) (at x)" .
   10.66 +qed
   10.67 +
   10.68 +lemma differentiable_series:
   10.69 +  fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
   10.70 +  assumes "convex s" "open s"
   10.71 +  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   10.72 +  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
   10.73 +  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)" and x: "x \<in> s"
   10.74 +  shows   "summable (\<lambda>n. f n x)" and "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)"
   10.75 +proof -
   10.76 +  from assms(4) obtain g' where A: "uniform_limit s (\<lambda>n x. \<Sum>i<n. f' i x) g' sequentially"
   10.77 +    unfolding uniformly_convergent_on_def by blast
   10.78 +  from x and `open s` have s: "at x within s = at x" by (rule at_within_open)
   10.79 +  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)"
   10.80 +    by (intro has_field_derivative_series[of s f f' g' x0] assms A has_field_derivative_at_within)
   10.81 +  then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
   10.82 +    "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
   10.83 +  from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
   10.84 +  from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
   10.85 +    by (simp add: has_field_derivative_def s)
   10.86 +  have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
   10.87 +    by (rule has_derivative_transform_within_open[OF `open s` x _ g'])
   10.88 +       (insert g, auto simp: sums_iff)
   10.89 +  thus "(\<lambda>x. \<Sum>n. f n x) differentiable (at x)" unfolding differentiable_def
   10.90 +    by (auto simp: summable_def differentiable_def has_field_derivative_def)
   10.91 +qed
   10.92 +
   10.93 +lemma differentiable_series':
   10.94 +  fixes f :: "nat \<Rightarrow> ('a :: {real_normed_field,banach}) \<Rightarrow> 'a"
   10.95 +  assumes "convex s" "open s"
   10.96 +  assumes "\<And>n x. x \<in> s \<Longrightarrow> (f n has_field_derivative f' n x) (at x)"
   10.97 +  assumes "uniformly_convergent_on s (\<lambda>n x. \<Sum>i<n. f' i x)"
   10.98 +  assumes "x0 \<in> s" "summable (\<lambda>n. f n x0)"
   10.99 +  shows   "(\<lambda>x. \<Sum>n. f n x) differentiable (at x0)"
  10.100 +  using differentiable_series[OF assms, of x0] `x0 \<in> s` by blast+
  10.101 +
  10.102  text \<open>Considering derivative @{typ "real \<Rightarrow> 'b::real_normed_vector"} as a vector.\<close>
  10.103  
  10.104  definition "vector_derivative f net = (SOME f'. (f has_vector_derivative f') net)"
  10.105 @@ -2445,4 +2531,61 @@
  10.106           vector_derivative f (at x) *\<^sub>R vector_derivative g (at (f x))"
  10.107  by (metis vector_diff_chain_at vector_derivative_at vector_derivative_works assms)
  10.108  
  10.109 +
  10.110 +subsection \<open>Relation between convexity and derivative\<close>
  10.111 +
  10.112 +(* TODO: Generalise to real vector spaces? *)
  10.113 +lemma convex_on_imp_above_tangent:
  10.114 +  assumes convex: "convex_on A f" and connected: "connected A"
  10.115 +  assumes c: "c \<in> interior A" and x : "x \<in> A"
  10.116 +  assumes deriv: "(f has_field_derivative f') (at c within A)"
  10.117 +  shows   "f x - f c \<ge> f' * (x - c)"
  10.118 +proof (cases x c rule: linorder_cases)
  10.119 +  assume xc: "x > c"
  10.120 +  let ?A' = "interior A \<inter> {c<..}"
  10.121 +  from c have "c \<in> interior A \<inter> closure {c<..}" by auto
  10.122 +  also have "\<dots> \<subseteq> closure (interior A \<inter> {c<..})" by (intro open_inter_closure_subset) auto
  10.123 +  finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
  10.124 +  moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) ---> f') (at c within ?A')"
  10.125 +    unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
  10.126 +  moreover from eventually_at_right_real[OF xc]
  10.127 +    have "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at_right c)"
  10.128 +  proof eventually_elim
  10.129 +    fix y assume y: "y \<in> {c<..<x}"
  10.130 +    with convex connected x c have "f y \<le> (f x - f c) / (x - c) * (y - c) + f c"
  10.131 +      using interior_subset[of A]
  10.132 +      by (intro convex_onD_Icc' convex_on_subset[OF convex] connected_contains_Icc) auto
  10.133 +    hence "f y - f c \<le> (f x - f c) / (x - c) * (y - c)" by simp
  10.134 +    thus "(f y - f c) / (y - c) \<le> (f x - f c) / (x - c)" using y xc by (simp add: divide_simps)
  10.135 +  qed
  10.136 +  hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at c within ?A')"
  10.137 +    by (blast intro: filter_leD at_le)
  10.138 +  ultimately have "f' \<le> (f x - f c) / (x - c)" by (rule tendsto_ge_const)
  10.139 +  thus ?thesis using xc by (simp add: field_simps)
  10.140 +next
  10.141 +  assume xc: "x < c"
  10.142 +  let ?A' = "interior A \<inter> {..<c}"
  10.143 +  from c have "c \<in> interior A \<inter> closure {..<c}" by auto
  10.144 +  also have "\<dots> \<subseteq> closure (interior A \<inter> {..<c})" by (intro open_inter_closure_subset) auto
  10.145 +  finally have "at c within ?A' \<noteq> bot" by (subst at_within_eq_bot_iff) auto
  10.146 +  moreover from deriv have "((\<lambda>y. (f y - f c) / (y - c)) ---> f') (at c within ?A')"
  10.147 +    unfolding DERIV_within_iff using interior_subset[of A] by (blast intro: tendsto_mono at_le)
  10.148 +  moreover from eventually_at_left_real[OF xc]
  10.149 +    have "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at_left c)"
  10.150 +  proof eventually_elim
  10.151 +    fix y assume y: "y \<in> {x<..<c}"
  10.152 +    with convex connected x c have "f y \<le> (f x - f c) / (c - x) * (c - y) + f c"
  10.153 +      using interior_subset[of A]
  10.154 +      by (intro convex_onD_Icc'' convex_on_subset[OF convex] connected_contains_Icc) auto
  10.155 +    hence "f y - f c \<le> (f x - f c) * ((c - y) / (c - x))" by simp
  10.156 +    also have "(c - y) / (c - x) = (y - c) / (x - c)" using y xc by (simp add: field_simps)
  10.157 +    finally show "(f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)" using y xc 
  10.158 +      by (simp add: divide_simps)
  10.159 +  qed
  10.160 +  hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at c within ?A')"
  10.161 +    by (blast intro: filter_leD at_le)
  10.162 +  ultimately have "f' \<ge> (f x - f c) / (x - c)" by (rule tendsto_le_const)
  10.163 +  thus ?thesis using xc by (simp add: field_simps)
  10.164 +qed simp_all
  10.165 +
  10.166  end
    11.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Oct 29 15:40:52 2015 +0100
    11.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Nov 02 11:56:28 2015 +0100
    11.3 @@ -896,6 +896,15 @@
    11.4    unfolding dist_norm norm_eq_sqrt_inner setL2_def
    11.5    by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
    11.6  
    11.7 +lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
    11.8 +  by (rule eventually_nhds_in_open) simp_all
    11.9 +
   11.10 +lemma eventually_at_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<in> A) (at z within A)"
   11.11 +  unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
   11.12 +
   11.13 +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)"
   11.14 +  unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
   11.15 +
   11.16  
   11.17  subsection \<open>Boxes\<close>
   11.18  
   11.19 @@ -1582,6 +1591,9 @@
   11.20    using open_contains_ball_eq [where S="interior S"]
   11.21    by (simp add: open_subset_interior)
   11.22  
   11.23 +lemma eventually_nhds_in_nhd: "x \<in> interior s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
   11.24 +  using interior_subset[of s] by (subst eventually_nhds) blast
   11.25 +
   11.26  lemma interior_limit_point [intro]:
   11.27    fixes x :: "'a::perfect_space"
   11.28    assumes x: "x \<in> interior S"
   11.29 @@ -1832,6 +1844,7 @@
   11.30      "closed s \<Longrightarrow> (closedin (subtopology euclidean s) t \<longleftrightarrow> closed t \<and> t \<subseteq> s)"
   11.31    by (meson closed_in_limpt closed_subset closedin_closed_trans)
   11.32  
   11.33 +
   11.34  subsection\<open>Connected components, considered as a connectedness relation or a set\<close>
   11.35  
   11.36  definition
   11.37 @@ -2258,6 +2271,9 @@
   11.38    using islimpt_in_closure
   11.39    by (metis trivial_limit_within)
   11.40  
   11.41 +lemma at_within_eq_bot_iff: "(at c within A = bot) \<longleftrightarrow> (c \<notin> closure (A - {c}))"
   11.42 +  using not_trivial_limit_within[of c A] by blast
   11.43 +
   11.44  text \<open>Some property holds "sufficiently close" to the limit point.\<close>
   11.45  
   11.46  lemma trivial_limit_eventually: "trivial_limit net \<Longrightarrow> eventually P net"
    12.1 --- a/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Thu Oct 29 15:40:52 2015 +0100
    12.2 +++ b/src/HOL/Multivariate_Analysis/Uniform_Limit.thy	Mon Nov 02 11:56:28 2015 +0100
    12.3 @@ -15,6 +15,12 @@
    12.4  abbreviation
    12.5    "uniform_limit S f l \<equiv> filterlim f (uniformly_on S l)"
    12.6  
    12.7 +definition uniformly_convergent_on where
    12.8 +  "uniformly_convergent_on X f \<longleftrightarrow> (\<exists>l. uniform_limit X f l sequentially)"
    12.9 +
   12.10 +definition uniformly_Cauchy_on where 
   12.11 +  "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)"
   12.12 +  
   12.13  lemma uniform_limit_iff:
   12.14    "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)"
   12.15    unfolding filterlim_iff uniformly_on_def
   12.16 @@ -114,9 +120,115 @@
   12.17      by (rule swap_uniform_limit) fact+
   12.18  qed
   12.19  
   12.20 -lemma weierstrass_m_test:
   12.21 +lemma uniformly_Cauchy_onI:
   12.22 +  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"
   12.23 +  shows   "uniformly_Cauchy_on X f"
   12.24 +  using assms unfolding uniformly_Cauchy_on_def by blast
   12.25 +
   12.26 +lemma uniformly_Cauchy_onI':
   12.27 +  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"
   12.28 +  shows   "uniformly_Cauchy_on X f"
   12.29 +proof (rule uniformly_Cauchy_onI)
   12.30 +  fix e :: real assume e: "e > 0"
   12.31 +  from assms[OF this] obtain M 
   12.32 +    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
   12.33 +  {
   12.34 +    fix x m n assume x: "x \<in> X" and m: "m \<ge> M" and n: "n \<ge> M"
   12.35 +    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"
   12.36 +      by (cases m n rule: linorder_cases) (simp_all add: dist_commute)
   12.37 +  }
   12.38 +  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
   12.39 +qed
   12.40 +
   12.41 +lemma uniformly_Cauchy_imp_Cauchy: 
   12.42 +  "uniformly_Cauchy_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> Cauchy (\<lambda>n. f n x)"
   12.43 +  unfolding Cauchy_def uniformly_Cauchy_on_def by fast
   12.44 +
   12.45 +lemma uniform_limit_cong:
   12.46 +  fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ('c :: metric_space)" and h i :: "'b \<Rightarrow> 'c"
   12.47 +  assumes "eventually (\<lambda>y. \<forall>x\<in>X. f y x = g y x) F"
   12.48 +  assumes "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
   12.49 +  shows   "uniform_limit X f h F \<longleftrightarrow> uniform_limit X g i F"
   12.50 +proof -
   12.51 +  {
   12.52 +    fix f g :: "'a \<Rightarrow> 'b \<Rightarrow> 'c" and h i :: "'b \<Rightarrow> 'c"
   12.53 +    assume C: "uniform_limit X f h F" and A: "eventually (\<lambda>y. \<forall>x\<in>X. f y x = g y x) F"
   12.54 +       and B: "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
   12.55 +    {
   12.56 +      fix e ::real assume "e > 0"
   12.57 +      with C have "eventually (\<lambda>y. \<forall>x\<in>X. dist (f y x) (h x) < e) F" 
   12.58 +        unfolding uniform_limit_iff by blast
   12.59 +      with A have "eventually (\<lambda>y. \<forall>x\<in>X. dist (g y x) (i x) < e) F"
   12.60 +        by eventually_elim (insert B, simp_all)
   12.61 +    }
   12.62 +    hence "uniform_limit X g i F" unfolding uniform_limit_iff by blast
   12.63 +  } note A = this
   12.64 +  show ?thesis by (rule iffI) (erule A; insert assms; simp add: eq_commute)+
   12.65 +qed
   12.66 +
   12.67 +lemma uniform_limit_cong':
   12.68 +  fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ('c :: metric_space)" and h i :: "'b \<Rightarrow> 'c"
   12.69 +  assumes "\<And>y x. x \<in> X \<Longrightarrow> f y x = g y x"
   12.70 +  assumes "\<And>x. x \<in> X \<Longrightarrow> h x = i x"
   12.71 +  shows   "uniform_limit X f h F \<longleftrightarrow> uniform_limit X g i F"
   12.72 +  using assms by (intro uniform_limit_cong always_eventually) blast+
   12.73 +
   12.74 +lemma uniformly_convergent_uniform_limit_iff:
   12.75 +  "uniformly_convergent_on X f \<longleftrightarrow> uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially"
   12.76 +proof
   12.77 +  assume "uniformly_convergent_on X f"
   12.78 +  then obtain l where l: "uniform_limit X f l sequentially" 
   12.79 +    unfolding uniformly_convergent_on_def by blast
   12.80 +  from l have "uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially \<longleftrightarrow>
   12.81 +                      uniform_limit X f l sequentially"
   12.82 +    by (intro uniform_limit_cong' limI tendsto_uniform_limitI[of f X l]) simp_all
   12.83 +  also note l
   12.84 +  finally show "uniform_limit X f (\<lambda>x. lim (\<lambda>n. f n x)) sequentially" .
   12.85 +qed (auto simp: uniformly_convergent_on_def)
   12.86 +
   12.87 +lemma uniformly_convergentI: "uniform_limit X f l sequentially \<Longrightarrow> uniformly_convergent_on X f"
   12.88 +  unfolding uniformly_convergent_on_def by blast
   12.89 +
   12.90 +lemma Cauchy_uniformly_convergent:
   12.91 +  fixes f :: "nat \<Rightarrow> 'a \<Rightarrow> 'b :: complete_space"
   12.92 +  assumes "uniformly_Cauchy_on X f"
   12.93 +  shows   "uniformly_convergent_on X f"
   12.94 +unfolding uniformly_convergent_uniform_limit_iff uniform_limit_iff
   12.95 +proof safe
   12.96 +  let ?f = "\<lambda>x. lim (\<lambda>n. f n x)"
   12.97 +  fix e :: real assume e: "e > 0"
   12.98 +  hence "e/2 > 0" by simp
   12.99 +  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"
  12.100 +    unfolding uniformly_Cauchy_on_def by fast
  12.101 +  show "eventually (\<lambda>n. \<forall>x\<in>X. dist (f n x) (?f x) < e) sequentially"
  12.102 +    using eventually_ge_at_top[of N]
  12.103 +  proof eventually_elim
  12.104 +    fix n assume n: "n \<ge> N"
  12.105 +    show "\<forall>x\<in>X. dist (f n x) (?f x) < e"
  12.106 +    proof
  12.107 +      fix x assume x: "x \<in> X"
  12.108 +      with assms have "(\<lambda>n. f n x) ----> ?f x" 
  12.109 +        by (auto dest!: Cauchy_convergent uniformly_Cauchy_imp_Cauchy simp: convergent_LIMSEQ_iff)
  12.110 +      with `e/2 > 0` have "eventually (\<lambda>m. m \<ge> N \<and> dist (f m x) (?f x) < e/2) sequentially"
  12.111 +        by (intro tendstoD eventually_conj eventually_ge_at_top)
  12.112 +      then obtain m where m: "m \<ge> N" "dist (f m x) (?f x) < e/2" 
  12.113 +        unfolding eventually_at_top_linorder by blast
  12.114 +      have "dist (f n x) (?f x) \<le> dist (f n x) (f m x) + dist (f m x) (?f x)"
  12.115 +          by (rule dist_triangle)
  12.116 +      also from x n have "... < e/2 + e/2" by (intro add_strict_mono N m)
  12.117 +      finally show "dist (f n x) (?f x) < e" by simp
  12.118 +    qed
  12.119 +  qed
  12.120 +qed
  12.121 +
  12.122 +lemma uniformly_convergent_imp_convergent:
  12.123 +  "uniformly_convergent_on X f \<Longrightarrow> x \<in> X \<Longrightarrow> convergent (\<lambda>n. f n x)"
  12.124 +  unfolding uniformly_convergent_on_def convergent_def
  12.125 +  by (auto dest: tendsto_uniform_limitI)
  12.126 +
  12.127 +lemma weierstrass_m_test_ev:
  12.128  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
  12.129 -assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
  12.130 +assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially"
  12.131  assumes "summable M"
  12.132  shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
  12.133  proof (rule uniform_limitI)
  12.134 @@ -125,14 +237,15 @@
  12.135    from suminf_exist_split[OF \<open>0 < e\<close> \<open>summable M\<close>]
  12.136    have "\<forall>\<^sub>F k in sequentially. norm (\<Sum>i. M (i + k)) < e"
  12.137      by (auto simp: eventually_sequentially)
  12.138 -  thus "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. dist (\<Sum>i<n. f i x) (\<Sum>i. f i x) < e"
  12.139 +  with eventually_all_ge_at_top[OF assms(1)]
  12.140 +    show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>A. dist (\<Sum>i<n. f i x) (\<Sum>i. f i x) < e"
  12.141    proof eventually_elim
  12.142      case (elim k)
  12.143      show ?case
  12.144      proof safe
  12.145        fix x assume "x \<in> A"
  12.146        have "\<exists>N. \<forall>n\<ge>N. norm (f n x) \<le> M n"
  12.147 -        using assms(1)[OF \<open>x \<in> A\<close>] by simp
  12.148 +        using assms(1) \<open>x \<in> A\<close> by (force simp: eventually_at_top_linorder)
  12.149        hence summable_norm_f: "summable (\<lambda>n. norm (f n x))"
  12.150          by(rule summable_norm_comparison_test[OF _ \<open>summable M\<close>])
  12.151        have summable_f: "summable (\<lambda>n. f n x)"
  12.152 @@ -152,13 +265,32 @@
  12.153          using summable_norm[OF summable_norm_f_plus_k] .
  12.154        also have "... \<le> (\<Sum>i. M (i + k))"
  12.155          by (rule suminf_le[OF _ summable_norm_f_plus_k summable_M_plus_k])
  12.156 -           (simp add: assms(1)[OF \<open>x \<in> A\<close>])
  12.157 +           (insert elim(1) \<open>x \<in> A\<close>, simp)
  12.158        finally show "dist (\<Sum>i<k. f i x) (\<Sum>i. f i x) < e"
  12.159          using elim by auto
  12.160      qed
  12.161    qed
  12.162  qed
  12.163  
  12.164 +lemma weierstrass_m_test:
  12.165 +fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
  12.166 +assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n"
  12.167 +assumes "summable M"
  12.168 +shows "uniform_limit A (\<lambda>n x. \<Sum>i<n. f i x) (\<lambda>x. suminf (\<lambda>i. f i x)) sequentially"
  12.169 +  using assms by (intro weierstrass_m_test_ev always_eventually) auto
  12.170 +  
  12.171 +lemma weierstrass_m_test'_ev:
  12.172 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
  12.173 +  assumes "eventually (\<lambda>n. \<forall>x\<in>A. norm (f n x) \<le> M n) sequentially" "summable M" 
  12.174 +  shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
  12.175 +  unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test_ev[OF assms])
  12.176 +
  12.177 +lemma weierstrass_m_test':
  12.178 +  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: banach"
  12.179 +  assumes "\<And>n x. x \<in> A \<Longrightarrow> norm (f n x) \<le> M n" "summable M" 
  12.180 +  shows   "uniformly_convergent_on A (\<lambda>n x. \<Sum>i<n. f i x)"
  12.181 +  unfolding uniformly_convergent_on_def by (rule exI, rule weierstrass_m_test[OF assms])
  12.182 +
  12.183  lemma uniform_limit_eq_rhs: "uniform_limit X f l F \<Longrightarrow> l = m \<Longrightarrow> uniform_limit X f m F"
  12.184    by simp
  12.185  
    13.1 --- a/src/HOL/Nat.thy	Thu Oct 29 15:40:52 2015 +0100
    13.2 +++ b/src/HOL/Nat.thy	Mon Nov 02 11:56:28 2015 +0100
    13.3 @@ -1472,6 +1472,9 @@
    13.4  lemma of_nat_mult: "of_nat (m * n) = of_nat m * of_nat n"
    13.5    by (induct m) (simp_all add: ac_simps distrib_right)
    13.6  
    13.7 +lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"
    13.8 +  by (induction x) (simp_all add: algebra_simps)
    13.9 +
   13.10  primrec of_nat_aux :: "('a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a" where
   13.11    "of_nat_aux inc 0 i = i"
   13.12  | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" -- \<open>tail recursive\<close>
    14.1 --- a/src/HOL/Parity.thy	Thu Oct 29 15:40:52 2015 +0100
    14.2 +++ b/src/HOL/Parity.thy	Mon Nov 02 11:56:28 2015 +0100
    14.3 @@ -233,7 +233,7 @@
    14.4  
    14.5  subsection \<open>Parity and powers\<close>
    14.6  
    14.7 -context comm_ring_1
    14.8 +context ring_1
    14.9  begin
   14.10  
   14.11  lemma power_minus_even [simp]:
    15.1 --- a/src/HOL/Power.thy	Thu Oct 29 15:40:52 2015 +0100
    15.2 +++ b/src/HOL/Power.thy	Mon Nov 02 11:56:28 2015 +0100
    15.3 @@ -283,6 +283,9 @@
    15.4      by (simp del: power_Suc add: power_Suc2 mult.assoc)
    15.5  qed
    15.6  
    15.7 +lemma power_minus': "NO_MATCH 1 x \<Longrightarrow> (-x) ^ n = (-1)^n * x ^ n"
    15.8 +  by (rule power_minus)
    15.9 +
   15.10  lemma power_minus_Bit0:
   15.11    "(- x) ^ numeral (Num.Bit0 k) = x ^ numeral (Num.Bit0 k)"
   15.12    by (induct k, simp_all only: numeral_class.numeral.simps power_add
   15.13 @@ -307,7 +310,7 @@
   15.14  lemma power_minus1_odd:
   15.15    "(- 1) ^ Suc (2*n) = -1"
   15.16    by simp
   15.17 -
   15.18 +  
   15.19  lemma power_minus_even [simp]:
   15.20    "(-a) ^ (2*n) = a ^ (2*n)"
   15.21    by (simp add: power_minus [of a])
    16.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Oct 29 15:40:52 2015 +0100
    16.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Mon Nov 02 11:56:28 2015 +0100
    16.3 @@ -228,6 +228,14 @@
    16.4  apply (erule (1) nonzero_inverse_scaleR_distrib)
    16.5  done
    16.6  
    16.7 +lemma setsum_constant_scaleR:
    16.8 +  fixes y :: "'a::real_vector"
    16.9 +  shows "(\<Sum>x\<in>A. y) = of_nat (card A) *\<^sub>R y"
   16.10 +  apply (cases "finite A")
   16.11 +  apply (induct set: finite)
   16.12 +  apply (simp_all add: algebra_simps)
   16.13 +  done
   16.14 +
   16.15  lemma real_vector_affinity_eq:
   16.16    fixes x :: "'a :: real_vector"
   16.17    assumes m0: "m \<noteq> 0"
   16.18 @@ -1614,6 +1622,12 @@
   16.19    apply auto
   16.20    done
   16.21  
   16.22 +lemma eventually_at_left_real: "a > (b :: real) \<Longrightarrow> eventually (\<lambda>x. x \<in> {b<..<a}) (at_left a)"
   16.23 +  by (subst eventually_at, rule exI[of _ "a - b"]) (force simp: dist_real_def)
   16.24 +
   16.25 +lemma eventually_at_right_real: "a < (b :: real) \<Longrightarrow> eventually (\<lambda>x. x \<in> {a<..<b}) (at_right a)"
   16.26 +  by (subst eventually_at, rule exI[of _ "b - a"]) (force simp: dist_real_def)
   16.27 +
   16.28  lemma metric_tendsto_imp_tendsto:
   16.29    fixes a :: "'a :: metric_space" and b :: "'b :: metric_space"
   16.30    assumes f: "(f ---> a) F"
   16.31 @@ -1709,12 +1723,36 @@
   16.32  definition (in metric_space) Cauchy :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   16.33    "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. dist (X m) (X n) < e)"
   16.34  
   16.35 -subsection \<open>Cauchy Sequences\<close>
   16.36 +lemma Cauchy_altdef:
   16.37 +  "Cauchy f = (\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e)"
   16.38 +proof
   16.39 +  assume A: "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e"
   16.40 +  show "Cauchy f" unfolding Cauchy_def
   16.41 +  proof (intro allI impI)
   16.42 +    fix e :: real assume e: "e > 0"
   16.43 +    with A obtain M where M: "\<And>m n. m \<ge> M \<Longrightarrow> n > m \<Longrightarrow> dist (f m) (f n) < e" by blast
   16.44 +    have "dist (f m) (f n) < e" if "m \<ge> M" "n \<ge> M" for m n
   16.45 +      using M[of m n] M[of n m] e that by (cases m n rule: linorder_cases) (auto simp: dist_commute)
   16.46 +    thus "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (f m) (f n) < e" by blast
   16.47 +  qed
   16.48 +next
   16.49 +  assume "Cauchy f"
   16.50 +  show "\<forall>e>0. \<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e" 
   16.51 +  proof (intro allI impI)
   16.52 +    fix e :: real assume e: "e > 0"
   16.53 +    with `Cauchy f` obtain M where "\<And>m n. m \<ge> M \<Longrightarrow> n \<ge> M \<Longrightarrow> dist (f m) (f n) < e"
   16.54 +      unfolding Cauchy_def by fast
   16.55 +    thus "\<exists>M. \<forall>m\<ge>M. \<forall>n>m. dist (f m) (f n) < e" by (intro exI[of _ M]) force
   16.56 +  qed
   16.57 +qed
   16.58  
   16.59  lemma metric_CauchyI:
   16.60    "(\<And>e. 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e) \<Longrightarrow> Cauchy X"
   16.61    by (simp add: Cauchy_def)
   16.62  
   16.63 +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"
   16.64 +  unfolding Cauchy_altdef by blast
   16.65 +
   16.66  lemma metric_CauchyD:
   16.67    "Cauchy X \<Longrightarrow> 0 < e \<Longrightarrow> \<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < e"
   16.68    by (simp add: Cauchy_def)
    17.1 --- a/src/HOL/Series.thy	Thu Oct 29 15:40:52 2015 +0100
    17.2 +++ b/src/HOL/Series.thy	Mon Nov 02 11:56:28 2015 +0100
    17.3 @@ -35,12 +35,20 @@
    17.4  lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
    17.5    by simp
    17.6  
    17.7 +lemma sums_cong: "(\<And>n. f n = g n) \<Longrightarrow> f sums c \<longleftrightarrow> g sums c"
    17.8 +  by (drule ext) simp
    17.9 +
   17.10  lemma sums_summable: "f sums l \<Longrightarrow> summable f"
   17.11    by (simp add: sums_def summable_def, blast)
   17.12  
   17.13  lemma summable_iff_convergent: "summable f \<longleftrightarrow> convergent (\<lambda>n. \<Sum>i<n. f i)"
   17.14    by (simp add: summable_def sums_def convergent_def)
   17.15  
   17.16 +lemma summable_iff_convergent':
   17.17 +  "summable f \<longleftrightarrow> convergent (\<lambda>n. setsum f {..n})"
   17.18 +  by (simp_all only: summable_iff_convergent convergent_def 
   17.19 +        lessThan_Suc_atMost [symmetric] LIMSEQ_Suc_iff[of "\<lambda>n. setsum f {..<n}"])
   17.20 +
   17.21  lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)"
   17.22    by (simp add: suminf_def sums_def lim_def)
   17.23  
   17.24 @@ -62,6 +70,34 @@
   17.25    apply simp
   17.26    done
   17.27  
   17.28 +lemma suminf_cong: "(\<And>n. f n = g n) \<Longrightarrow> suminf f = suminf g"
   17.29 +  by (rule arg_cong[of f g], rule ext) simp
   17.30 +
   17.31 +lemma summable_cong:
   17.32 +  assumes "eventually (\<lambda>x. f x = (g x :: 'a :: real_normed_vector)) sequentially"
   17.33 +  shows   "summable f = summable g"
   17.34 +proof -
   17.35 +  from assms obtain N where N: "\<forall>n\<ge>N. f n = g n" by (auto simp: eventually_at_top_linorder)
   17.36 +  def C \<equiv> "(\<Sum>k<N. f k - g k)"
   17.37 +  from eventually_ge_at_top[of N] 
   17.38 +    have "eventually (\<lambda>n. setsum f {..<n} = C + setsum g {..<n}) sequentially"
   17.39 +  proof eventually_elim
   17.40 +    fix n assume n: "n \<ge> N"
   17.41 +    from n have "{..<n} = {..<N} \<union> {N..<n}" by auto
   17.42 +    also have "setsum f ... = setsum f {..<N} + setsum f {N..<n}"
   17.43 +      by (intro setsum.union_disjoint) auto
   17.44 +    also from N have "setsum f {N..<n} = setsum g {N..<n}" by (intro setsum.cong) simp_all
   17.45 +    also have "setsum f {..<N} + setsum g {N..<n} = C + (setsum g {..<N} + setsum g {N..<n})" 
   17.46 +      unfolding C_def by (simp add: algebra_simps setsum_subtractf)
   17.47 +    also have "setsum g {..<N} + setsum g {N..<n} = setsum g ({..<N} \<union> {N..<n})"
   17.48 +      by (intro setsum.union_disjoint [symmetric]) auto
   17.49 +    also from n have "{..<N} \<union> {N..<n} = {..<n}" by auto
   17.50 +    finally show "setsum f {..<n} = C + setsum g {..<n}" .
   17.51 +  qed
   17.52 +  from convergent_cong[OF this] show ?thesis
   17.53 +    by (simp add: summable_iff_convergent convergent_add_const_iff)
   17.54 +qed
   17.55 +
   17.56  lemma sums_finite:
   17.57    assumes [simp]: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
   17.58    shows "f sums (\<Sum>n\<in>N. f n)"
   17.59 @@ -125,6 +161,10 @@
   17.60  lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
   17.61    by (metis summable_sums sums_summable sums_unique)
   17.62  
   17.63 +lemma summable_sums_iff: 
   17.64 +  "summable (f :: nat \<Rightarrow> 'a :: {comm_monoid_add,t2_space}) \<longleftrightarrow> f sums suminf f"
   17.65 +  by (auto simp: sums_iff summable_sums)
   17.66 +
   17.67  lemma sums_unique2:
   17.68    fixes a b :: "'a::{comm_monoid_add,t2_space}"
   17.69    shows "f sums a \<Longrightarrow> f sums b \<Longrightarrow> a = b"
   17.70 @@ -221,6 +261,7 @@
   17.71        by (auto intro: le_less_trans simp: eventually_sequentially) }
   17.72  qed
   17.73  
   17.74 +
   17.75  subsection \<open>Infinite summability on real normed vector spaces\<close>
   17.76  
   17.77  lemma sums_Suc_iff:
   17.78 @@ -241,6 +282,14 @@
   17.79    finally show ?thesis ..
   17.80  qed
   17.81  
   17.82 +lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n) :: 'a :: real_normed_vector) = summable f"
   17.83 +proof
   17.84 +  assume "summable f"
   17.85 +  hence "f sums suminf f" by (rule summable_sums)
   17.86 +  hence "(\<lambda>n. f (Suc n)) sums (suminf f - f 0)" by (simp add: sums_Suc_iff)
   17.87 +  thus "summable (\<lambda>n. f (Suc n))" unfolding summable_def by blast
   17.88 +qed (auto simp: sums_Suc_iff summable_def)
   17.89 +
   17.90  context
   17.91    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   17.92  begin
   17.93 @@ -299,6 +348,9 @@
   17.94  lemma suminf_split_initial_segment: "summable f \<Longrightarrow> suminf f = (\<Sum>n. f(n + k)) + (\<Sum>i<k. f i)"
   17.95    by (auto simp add: suminf_minus_initial_segment)
   17.96  
   17.97 +lemma suminf_split_head: "summable f \<Longrightarrow> (\<Sum>n. f (Suc n)) = suminf f - f 0"
   17.98 +  using suminf_split_initial_segment[of 1] by simp
   17.99 +
  17.100  lemma suminf_exist_split: 
  17.101    fixes r :: real assumes "0 < r" and "summable f"
  17.102    shows "\<exists>N. \<forall>n\<ge>N. norm (\<Sum>i. f (i + n)) < r"
  17.103 @@ -319,6 +371,14 @@
  17.104    apply (drule_tac x="n" in spec, simp)
  17.105    done
  17.106  
  17.107 +lemma summable_imp_convergent:
  17.108 +  "summable (f :: nat \<Rightarrow> 'a) \<Longrightarrow> convergent f"
  17.109 +  by (force dest!: summable_LIMSEQ_zero simp: convergent_def)
  17.110 +
  17.111 +lemma summable_imp_Bseq:
  17.112 +  "summable f \<Longrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
  17.113 +  by (simp add: convergent_imp_Bseq summable_imp_convergent)
  17.114 +
  17.115  end
  17.116  
  17.117  lemma summable_minus_iff:
  17.118 @@ -363,6 +423,23 @@
  17.119  lemmas summable_scaleR_right = bounded_linear.summable[OF bounded_linear_scaleR_right]
  17.120  lemmas suminf_scaleR_right = bounded_linear.suminf[OF bounded_linear_scaleR_right]
  17.121  
  17.122 +lemma summable_const_iff: "summable (\<lambda>_. c) \<longleftrightarrow> (c :: 'a :: real_normed_vector) = 0"
  17.123 +proof -
  17.124 +  {
  17.125 +    assume "c \<noteq> 0"
  17.126 +    hence "filterlim (\<lambda>n. of_nat n * norm c) at_top sequentially"
  17.127 +      unfolding real_of_nat_def[symmetric]
  17.128 +      by (subst mult.commute)
  17.129 +         (auto intro!: filterlim_tendsto_pos_mult_at_top filterlim_real_sequentially)
  17.130 +    hence "\<not>convergent (\<lambda>n. norm (\<Sum>k<n. c))"
  17.131 +      by (intro filterlim_at_infinity_imp_not_convergent filterlim_at_top_imp_at_infinity) 
  17.132 +         (simp_all add: setsum_constant_scaleR)
  17.133 +    hence "\<not>summable (\<lambda>_. c)" unfolding summable_iff_convergent using convergent_norm by blast
  17.134 +  }
  17.135 +  thus ?thesis by auto
  17.136 +qed
  17.137 +
  17.138 +
  17.139  subsection \<open>Infinite summability on real normed algebras\<close>
  17.140  
  17.141  context
  17.142 @@ -389,6 +466,22 @@
  17.143  
  17.144  end
  17.145  
  17.146 +lemma sums_mult_iff:
  17.147 +  assumes "c \<noteq> 0"
  17.148 +  shows   "(\<lambda>n. c * f n :: 'a :: {real_normed_algebra,field}) sums (c * d) \<longleftrightarrow> f sums d"
  17.149 +  using sums_mult[of f d c] sums_mult[of "\<lambda>n. c * f n" "c * d" "inverse c"]
  17.150 +  by (force simp: field_simps assms)
  17.151 +
  17.152 +lemma sums_mult2_iff:
  17.153 +  assumes "c \<noteq> (0 :: 'a :: {real_normed_algebra, field})"
  17.154 +  shows   "(\<lambda>n. f n * c) sums (d * c) \<longleftrightarrow> f sums d"
  17.155 +  using sums_mult_iff[OF assms, of f d] by (simp add: mult.commute)
  17.156 +
  17.157 +lemma sums_of_real_iff:
  17.158 +  "(\<lambda>n. of_real (f n) :: 'a :: real_normed_div_algebra) sums of_real c \<longleftrightarrow> f sums c"
  17.159 +  by (simp add: sums_def of_real_setsum[symmetric] tendsto_of_real_iff del: of_real_setsum)
  17.160 +
  17.161 +
  17.162  subsection \<open>Infinite summability on real normed fields\<close>
  17.163  
  17.164  context
  17.165 @@ -427,6 +520,16 @@
  17.166  lemma suminf_geometric: "norm c < 1 \<Longrightarrow> suminf (\<lambda>n. c^n) = 1 / (1 - c)"
  17.167    by (rule sums_unique[symmetric]) (rule geometric_sums)
  17.168  
  17.169 +lemma summable_geometric_iff: "summable (\<lambda>n. c ^ n) \<longleftrightarrow> norm c < 1"
  17.170 +proof
  17.171 +  assume "summable (\<lambda>n. c ^ n :: 'a :: real_normed_field)"
  17.172 +  hence "(\<lambda>n. norm c ^ n) ----> 0"
  17.173 +    by (simp add: norm_power [symmetric] tendsto_norm_zero_iff summable_LIMSEQ_zero)
  17.174 +  from order_tendstoD(2)[OF this zero_less_one] obtain n where "norm c ^ n < 1"
  17.175 +    by (auto simp: eventually_at_top_linorder)
  17.176 +  thus "norm c < 1" using one_le_power[of "norm c" n] by (cases "norm c \<ge> 1") (linarith, simp)
  17.177 +qed (rule summable_geometric)
  17.178 +  
  17.179  end
  17.180  
  17.181  lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
  17.182 @@ -439,6 +542,36 @@
  17.183      by simp
  17.184  qed
  17.185  
  17.186 +
  17.187 +subsection \<open>Telescoping\<close>
  17.188 +
  17.189 +lemma telescope_sums:
  17.190 +  assumes "f ----> (c :: 'a :: real_normed_vector)"
  17.191 +  shows   "(\<lambda>n. f (Suc n) - f n) sums (c - f 0)"
  17.192 +  unfolding sums_def
  17.193 +proof (subst LIMSEQ_Suc_iff [symmetric])
  17.194 +  have "(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)"
  17.195 +    by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setsum_Suc_diff)
  17.196 +  also have "\<dots> ----> c - f 0" by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const)
  17.197 +  finally show "(\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) ----> c - f 0" .
  17.198 +qed
  17.199 +
  17.200 +lemma telescope_sums':
  17.201 +  assumes "f ----> (c :: 'a :: real_normed_vector)"
  17.202 +  shows   "(\<lambda>n. f n - f (Suc n)) sums (f 0 - c)"
  17.203 +  using sums_minus[OF telescope_sums[OF assms]] by (simp add: algebra_simps)
  17.204 +
  17.205 +lemma telescope_summable:
  17.206 +  assumes "f ----> (c :: 'a :: real_normed_vector)"
  17.207 +  shows   "summable (\<lambda>n. f (Suc n) - f n)"
  17.208 +  using telescope_sums[OF assms] by (simp add: sums_iff)
  17.209 +
  17.210 +lemma telescope_summable':
  17.211 +  assumes "f ----> (c :: 'a :: real_normed_vector)"
  17.212 +  shows   "summable (\<lambda>n. f n - f (Suc n))"
  17.213 +  using summable_minus[OF telescope_summable[OF assms]] by (simp add: algebra_simps)
  17.214 +
  17.215 +
  17.216  subsection \<open>Infinite summability on Banach spaces\<close>
  17.217  
  17.218  text\<open>Cauchy-type criterion for convergence of series (c.f. Harrison)\<close>
  17.219 @@ -463,7 +596,7 @@
  17.220  
  17.221  context
  17.222    fixes f :: "nat \<Rightarrow> 'a::banach"
  17.223 -begin  
  17.224 +begin
  17.225  
  17.226  text\<open>Absolute convergence imples normal convergence\<close>
  17.227  
  17.228 @@ -495,6 +628,10 @@
  17.229    apply (auto intro: setsum_mono simp add: abs_less_iff)
  17.230    done
  17.231  
  17.232 +lemma summable_comparison_test_ev:
  17.233 +  shows "eventually (\<lambda>n. norm (f n) \<le> g n) sequentially \<Longrightarrow> summable g \<Longrightarrow> summable f"
  17.234 +  by (rule summable_comparison_test) (auto simp: eventually_at_top_linorder)
  17.235 +
  17.236  (*A better argument order*)
  17.237  lemma summable_comparison_test': "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm(f n) \<le> g n) \<Longrightarrow> summable f"
  17.238    by (rule summable_comparison_test) auto
  17.239 @@ -669,6 +806,21 @@
  17.240  lemma summable_rabs: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
  17.241    by (fold real_norm_def) (rule summable_norm)
  17.242  
  17.243 +lemma summable_zero_power [simp]: "summable (\<lambda>n. 0 ^ n :: 'a :: {comm_ring_1,topological_space})"
  17.244 +proof -
  17.245 +  have "(\<lambda>n. 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then 0^0 else 0)" by (intro ext) (simp add: zero_power)
  17.246 +  moreover have "summable \<dots>" by simp
  17.247 +  ultimately show ?thesis by simp
  17.248 +qed
  17.249 +
  17.250 +lemma summable_zero_power' [simp]: "summable (\<lambda>n. f n * 0 ^ n :: 'a :: {ring_1,topological_space})"
  17.251 +proof -
  17.252 +  have "(\<lambda>n. f n * 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then f 0 * 0^0 else 0)" 
  17.253 +    by (intro ext) (simp add: zero_power)
  17.254 +  moreover have "summable \<dots>" by simp
  17.255 +  ultimately show ?thesis by simp
  17.256 +qed
  17.257 +
  17.258  lemma summable_power_series:
  17.259    fixes z :: real
  17.260    assumes le_1: "\<And>i. f i \<le> 1" and nonneg: "\<And>i. 0 \<le> f i" and z: "0 \<le> z" "z < 1"
  17.261 @@ -679,6 +831,79 @@
  17.262      using z by (auto intro!: exI[of _ 0] mult_left_le_one_le simp: abs_mult nonneg power_abs less_imp_le le_1)
  17.263  qed
  17.264  
  17.265 +lemma summable_0_powser:
  17.266 +  "summable (\<lambda>n. f n * 0 ^ n :: 'a :: real_normed_div_algebra)"
  17.267 +proof -
  17.268 +  have A: "(\<lambda>n. f n * 0 ^ n) = (\<lambda>n. if n = 0 then f n else 0)"
  17.269 +    by (intro ext) auto
  17.270 +  thus ?thesis by (subst A) simp_all
  17.271 +qed
  17.272 +
  17.273 +lemma summable_powser_split_head:
  17.274 +  "summable (\<lambda>n. f (Suc n) * z ^ n :: 'a :: real_normed_div_algebra) = summable (\<lambda>n. f n * z ^ n)"
  17.275 +proof -
  17.276 +  have "summable (\<lambda>n. f (Suc n) * z ^ n) \<longleftrightarrow> summable (\<lambda>n. f (Suc n) * z ^ Suc n)"
  17.277 +  proof
  17.278 +    assume "summable (\<lambda>n. f (Suc n) * z ^ n)"
  17.279 +    from summable_mult2[OF this, of z] show "summable (\<lambda>n. f (Suc n) * z ^ Suc n)" 
  17.280 +      by (simp add: power_commutes algebra_simps)
  17.281 +  next
  17.282 +    assume "summable (\<lambda>n. f (Suc n) * z ^ Suc n)"
  17.283 +    from summable_mult2[OF this, of "inverse z"] show "summable (\<lambda>n. f (Suc n) * z ^ n)"
  17.284 +      by (cases "z \<noteq> 0", subst (asm) power_Suc2) (simp_all add: algebra_simps)
  17.285 +  qed
  17.286 +  also have "\<dots> \<longleftrightarrow> summable (\<lambda>n. f n * z ^ n)" by (rule summable_Suc_iff)
  17.287 +  finally show ?thesis .
  17.288 +qed
  17.289 +
  17.290 +lemma powser_split_head:
  17.291 +  assumes "summable (\<lambda>n. f n * z ^ n :: 'a :: {real_normed_div_algebra,banach})"
  17.292 +  shows   "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z"
  17.293 +          "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n) - f 0"
  17.294 +          "summable (\<lambda>n. f (Suc n) * z ^ n)"
  17.295 +proof -
  17.296 +  from assms show "summable (\<lambda>n. f (Suc n) * z ^ n)" by (subst summable_powser_split_head)
  17.297 +
  17.298 +  from suminf_mult2[OF this, of z] 
  17.299 +    have "(\<Sum>n. f (Suc n) * z ^ n) * z = (\<Sum>n. f (Suc n) * z ^ Suc n)"
  17.300 +    by (simp add: power_commutes algebra_simps)
  17.301 +  also from assms have "\<dots> = suminf (\<lambda>n. f n * z ^ n) - f 0"
  17.302 +    by (subst suminf_split_head) simp_all
  17.303 +  finally show "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z" by simp
  17.304 +  thus "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n) - f 0" by simp
  17.305 +qed
  17.306 +
  17.307 +lemma summable_partial_sum_bound:
  17.308 +  fixes f :: "nat \<Rightarrow> 'a :: banach"
  17.309 +  assumes summable: "summable f" and e: "e > (0::real)"
  17.310 +  obtains N where "\<And>m n. m \<ge> N \<Longrightarrow> norm (\<Sum>k=m..n. f k) < e"
  17.311 +proof -
  17.312 +  from summable have "Cauchy (\<lambda>n. \<Sum>k<n. f k)" 
  17.313 +    by (simp add: Cauchy_convergent_iff summable_iff_convergent)
  17.314 +  from CauchyD[OF this e] obtain N 
  17.315 +    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
  17.316 +  {
  17.317 +    fix m n :: nat assume m: "m \<ge> N"
  17.318 +    have "norm (\<Sum>k=m..n. f k) < e"
  17.319 +    proof (cases "n \<ge> m")
  17.320 +      assume n: "n \<ge> m"
  17.321 +      with m have "norm ((\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k)) < e" by (intro N) simp_all
  17.322 +      also from n have "(\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k) = (\<Sum>k=m..n. f k)"
  17.323 +        by (subst setsum_diff [symmetric]) (simp_all add: setsum_last_plus)
  17.324 +      finally show ?thesis .
  17.325 +    qed (insert e, simp_all)
  17.326 +  }
  17.327 +  thus ?thesis by (rule that)
  17.328 +qed
  17.329 +
  17.330 +lemma powser_sums_if: 
  17.331 +  "(\<lambda>n. (if n = m then (1 :: 'a :: {ring_1,topological_space}) else 0) * z^n) sums z^m"
  17.332 +proof -
  17.333 +  have "(\<lambda>n. (if n = m then 1 else 0) * z^n) = (\<lambda>n. if n = m then z^n else 0)" 
  17.334 +    by (intro ext) auto
  17.335 +  thus ?thesis by (simp add: sums_single)
  17.336 +qed
  17.337 +
  17.338  lemma
  17.339     fixes f :: "nat \<Rightarrow> real"
  17.340     assumes "summable f"
  17.341 @@ -742,4 +967,82 @@
  17.342    with le show "suminf (f \<circ> g) = suminf f" by(rule antisym)
  17.343  qed
  17.344  
  17.345 +lemma sums_mono_reindex:
  17.346 +  assumes subseq: "subseq g" and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
  17.347 +  shows   "(\<lambda>n. f (g n)) sums c \<longleftrightarrow> f sums c"
  17.348 +unfolding sums_def
  17.349 +proof
  17.350 +  assume lim: "(\<lambda>n. \<Sum>k<n. f k) ----> c"
  17.351 +  have "(\<lambda>n. \<Sum>k<n. f (g k)) = (\<lambda>n. \<Sum>k<g n. f k)"
  17.352 +  proof
  17.353 +    fix n :: nat
  17.354 +    from subseq have "(\<Sum>k<n. f (g k)) = (\<Sum>k\<in>g`{..<n}. f k)"
  17.355 +      by (subst setsum.reindex) (auto intro: subseq_imp_inj_on)
  17.356 +    also from subseq have "\<dots> = (\<Sum>k<g n. f k)"
  17.357 +      by (intro setsum.mono_neutral_left ballI zero)
  17.358 +         (auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq)
  17.359 +    finally show "(\<Sum>k<n. f (g k)) = (\<Sum>k<g n. f k)" .
  17.360 +  qed
  17.361 +  also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> ----> c" unfolding o_def .
  17.362 +  finally show "(\<lambda>n. \<Sum>k<n. f (g k)) ----> c" .
  17.363 +next
  17.364 +  assume lim: "(\<lambda>n. \<Sum>k<n. f (g k)) ----> c"
  17.365 +  def g_inv \<equiv> "\<lambda>n. LEAST m. g m \<ge> n"
  17.366 +  from filterlim_subseq[OF subseq] have g_inv_ex: "\<exists>m. g m \<ge> n" for n
  17.367 +    by (auto simp: filterlim_at_top eventually_at_top_linorder)
  17.368 +  hence g_inv: "g (g_inv n) \<ge> n" for n unfolding g_inv_def by (rule LeastI_ex)
  17.369 +  have g_inv_least: "m \<ge> g_inv n" if "g m \<ge> n" for m n using that 
  17.370 +    unfolding g_inv_def by (rule Least_le)
  17.371 +  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  
  17.372 +  have "(\<lambda>n. \<Sum>k<n. f k) = (\<lambda>n. \<Sum>k<g_inv n. f (g k))"
  17.373 +  proof
  17.374 +    fix n :: nat
  17.375 +    {
  17.376 +      fix k assume k: "k \<in> {..<n} - g`{..<g_inv n}"
  17.377 +      have "k \<notin> range g"
  17.378 +      proof (rule notI, elim imageE)
  17.379 +        fix l assume l: "k = g l"
  17.380 +        have "g l < g (g_inv n)" by (rule less_le_trans[OF _ g_inv]) (insert k l, simp_all)
  17.381 +        with subseq have "l < g_inv n" by (simp add: subseq_strict_mono strict_mono_less)
  17.382 +        with k l show False by simp
  17.383 +      qed
  17.384 +      hence "f k = 0" by (rule zero)
  17.385 +    }
  17.386 +    with g_inv_least' g_inv have "(\<Sum>k<n. f k) = (\<Sum>k\<in>g`{..<g_inv n}. f k)"
  17.387 +      by (intro setsum.mono_neutral_right) auto
  17.388 +    also from subseq have "\<dots> = (\<Sum>k<g_inv n. f (g k))" using subseq_imp_inj_on 
  17.389 +      by (subst setsum.reindex) simp_all
  17.390 +    finally show "(\<Sum>k<n. f k) = (\<Sum>k<g_inv n. f (g k))" .
  17.391 +  qed
  17.392 +  also {
  17.393 +    fix K n :: nat assume "g K \<le> n"
  17.394 +    also have "n \<le> g (g_inv n)" by (rule g_inv)
  17.395 +    finally have "K \<le> g_inv n" using subseq by (simp add: strict_mono_less_eq subseq_strict_mono)
  17.396 +  }
  17.397 +  hence "filterlim g_inv at_top sequentially" 
  17.398 +    by (auto simp: filterlim_at_top eventually_at_top_linorder)
  17.399 +  from lim and this have "(\<lambda>n. \<Sum>k<g_inv n. f (g k)) ----> c" by (rule filterlim_compose)
  17.400 +  finally show "(\<lambda>n. \<Sum>k<n. f k) ----> c" .
  17.401 +qed
  17.402 +
  17.403 +lemma summable_mono_reindex:
  17.404 +  assumes subseq: "subseq g" and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0"
  17.405 +  shows   "summable (\<lambda>n. f (g n)) \<longleftrightarrow> summable f"
  17.406 +  using sums_mono_reindex[of g f, OF assms] by (simp add: summable_def)
  17.407 +
  17.408 +lemma suminf_mono_reindex:                                                                 
  17.409 +  assumes "subseq g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = (0 :: 'a :: {t2_space,comm_monoid_add})"
  17.410 +  shows   "suminf (\<lambda>n. f (g n)) = suminf f"
  17.411 +proof (cases "summable f")
  17.412 +  case False
  17.413 +  hence "\<not>(\<exists>c. f sums c)" unfolding summable_def by blast
  17.414 +  hence "suminf f = The (\<lambda>_. False)" by (simp add: suminf_def)
  17.415 +  moreover from False have "\<not>summable (\<lambda>n. f (g n))"
  17.416 +    using summable_mono_reindex[of g f, OF assms] by simp
  17.417 +  hence "\<not>(\<exists>c. (\<lambda>n. f (g n)) sums c)" unfolding summable_def by blast
  17.418 +  hence "suminf (\<lambda>n. f (g n)) = The (\<lambda>_. False)" by (simp add: suminf_def)
  17.419 +  ultimately show ?thesis by simp
  17.420 +qed (insert sums_mono_reindex[of g f, OF assms] summable_mono_reindex[of g f, OF assms], 
  17.421 +     simp_all add: sums_iff)
  17.422 +
  17.423  end
    18.1 --- a/src/HOL/Topological_Spaces.thy	Thu Oct 29 15:40:52 2015 +0100
    18.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Nov 02 11:56:28 2015 +0100
    18.3 @@ -353,6 +353,10 @@
    18.4    "eventually P (nhds a) \<longleftrightarrow> (\<exists>S. open S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
    18.5    unfolding nhds_def by (subst eventually_INF_base) (auto simp: eventually_principal)
    18.6  
    18.7 +lemma (in topological_space) eventually_nhds_in_open: 
    18.8 +  "open s \<Longrightarrow> x \<in> s \<Longrightarrow> eventually (\<lambda>y. y \<in> s) (nhds x)"
    18.9 +  by (subst eventually_nhds) blast
   18.10 +
   18.11  lemma nhds_neq_bot [simp]: "nhds a \<noteq> bot"
   18.12    unfolding trivial_limit_def eventually_nhds by simp
   18.13  
   18.14 @@ -497,6 +501,12 @@
   18.15     "(f ---> l) F \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) F)"
   18.16     unfolding nhds_def filterlim_INF filterlim_principal by auto
   18.17  
   18.18 +lemma tendsto_cong:
   18.19 +  assumes "eventually (\<lambda>x. f x = g x) F"
   18.20 +  shows   "(f ---> c) F \<longleftrightarrow> (g ---> c) F"
   18.21 +  by (rule filterlim_cong[OF refl refl assms])
   18.22 +
   18.23 +
   18.24  lemma tendsto_mono: "F \<le> F' \<Longrightarrow> (f ---> l) F' \<Longrightarrow> (f ---> l) F"
   18.25    unfolding tendsto_def le_filter_def by fast
   18.26  
   18.27 @@ -625,6 +635,28 @@
   18.28      using order_tendstoD[OF lim(2), of a] ev by (auto elim: eventually_elim2)
   18.29  qed
   18.30  
   18.31 +lemma limit_frequently_eq:
   18.32 +  assumes "F \<noteq> bot"
   18.33 +  assumes "frequently (\<lambda>x. f x = c) F"
   18.34 +  assumes "(f ---> d) F"
   18.35 +  shows   "d = (c :: 'a :: t1_space)"
   18.36 +proof (rule ccontr)
   18.37 +  assume "d \<noteq> c"
   18.38 +  from t1_space[OF this] obtain U where "open U" "d \<in> U" "c \<notin> U" by blast
   18.39 +  from this assms have "eventually (\<lambda>x. f x \<in> U) F" unfolding tendsto_def by blast
   18.40 +  hence "eventually (\<lambda>x. f x \<noteq> c) F" by eventually_elim (insert `c \<notin> U`, blast)
   18.41 +  with assms(2) show False unfolding frequently_def by contradiction
   18.42 +qed
   18.43 +
   18.44 +lemma tendsto_imp_eventually_ne:
   18.45 +  assumes "F \<noteq> bot" "(f ---> c) F" "c \<noteq> (c' :: 'a :: t1_space)"
   18.46 +  shows   "eventually (\<lambda>z. f z \<noteq> c') F"
   18.47 +proof (rule ccontr)
   18.48 +  assume "\<not>eventually (\<lambda>z. f z \<noteq> c') F"
   18.49 +  hence "frequently (\<lambda>z. f z = c') F" by (simp add: frequently_def)
   18.50 +  from limit_frequently_eq[OF assms(1) this assms(2)] and assms(3) show False by contradiction
   18.51 +qed
   18.52 +
   18.53  lemma tendsto_le:
   18.54    fixes f g :: "'a \<Rightarrow> 'b::linorder_topology"
   18.55    assumes F: "\<not> trivial_limit F"
   18.56 @@ -657,6 +689,9 @@
   18.57    shows "a \<ge> x"
   18.58    by (rule tendsto_le [OF F tendsto_const x a])
   18.59  
   18.60 +
   18.61 +
   18.62 +
   18.63  subsubsection \<open>Rules about @{const Lim}\<close>
   18.64  
   18.65  lemma tendsto_Lim:
   18.66 @@ -924,6 +959,17 @@
   18.67  lemma subseq_mono: assumes "subseq r" "m < n" shows "r m < r n"
   18.68    using assms by (auto simp: subseq_def)
   18.69  
   18.70 +lemma subseq_imp_inj_on: "subseq g \<Longrightarrow> inj_on g A"
   18.71 +proof (rule inj_onI)
   18.72 +  assume g: "subseq g"
   18.73 +  fix x y assume "g x = g y"
   18.74 +  with subseq_mono[OF g, of x y] subseq_mono[OF g, of y x] show "x = y" 
   18.75 +    by (cases x y rule: linorder_cases) simp_all
   18.76 +qed
   18.77 +
   18.78 +lemma subseq_strict_mono: "subseq g \<Longrightarrow> strict_mono g"
   18.79 +  by (intro strict_monoI subseq_mono[of g])
   18.80 +
   18.81  lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
   18.82    by (simp add: incseq_def monoseq_def)
   18.83  
   18.84 @@ -2142,6 +2188,15 @@
   18.85    assumes A: "connected A" "a \<in> A" "b \<in> A" shows "{a <..< b} \<subseteq> A"
   18.86    using connectedD_interval[OF A] by (simp add: subset_eq Ball_def less_imp_le)
   18.87  
   18.88 +lemma connected_contains_Icc:
   18.89 +  assumes "connected (A :: ('a :: {linorder_topology}) set)" "a \<in> A" "b \<in> A"
   18.90 +  shows   "{a..b} \<subseteq> A"
   18.91 +proof
   18.92 +  fix x assume "x \<in> {a..b}"
   18.93 +  hence "x = a \<or> x = b \<or> x \<in> {a<..<b}" by auto
   18.94 +  thus "x \<in> A" using assms connected_contains_Ioo[of A a b] by auto
   18.95 +qed
   18.96 +
   18.97  subsection \<open>Intermediate Value Theorem\<close>
   18.98  
   18.99  lemma IVT':
    19.1 --- a/src/HOL/Transcendental.thy	Thu Oct 29 15:40:52 2015 +0100
    19.2 +++ b/src/HOL/Transcendental.thy	Mon Nov 02 11:56:28 2015 +0100
    19.3 @@ -16,6 +16,11 @@
    19.4    using floor_correct [of "x/y"] assms
    19.5    by (auto simp: Real.real_of_nat_Suc field_simps intro: that [of "nat (floor (x/y))"])
    19.6  
    19.7 +lemma fact_in_Reals: "fact n \<in> \<real>" by (induction n) auto
    19.8 +
    19.9 +lemma pochhammer_of_real: "pochhammer (of_real x) n = of_real (pochhammer x n)"
   19.10 +  by (simp add: pochhammer_def)
   19.11 +
   19.12  lemma of_real_fact [simp]: "of_real (fact n) = fact n"
   19.13    by (metis of_nat_fact of_real_of_nat_eq)
   19.14  
   19.15 @@ -1081,6 +1086,15 @@
   19.16  qed
   19.17  
   19.18  
   19.19 +lemma isCont_pochhammer [continuous_intros]: "isCont (\<lambda>z::'a::real_normed_field. pochhammer z n) z"
   19.20 +  by (induction n) (auto intro!: continuous_intros simp: pochhammer_rec')
   19.21 +
   19.22 +lemma continuous_on_pochhammer [continuous_intros]: 
   19.23 +  fixes A :: "'a :: real_normed_field set"
   19.24 +  shows "continuous_on A (\<lambda>z. pochhammer z n)"
   19.25 +  by (intro continuous_at_imp_continuous_on ballI isCont_pochhammer)
   19.26 +
   19.27 +
   19.28  subsection \<open>Exponential Function\<close>
   19.29  
   19.30  definition exp :: "'a \<Rightarrow> 'a::{real_normed_algebra_1,banach}"
   19.31 @@ -4227,6 +4241,93 @@
   19.32  lemma tan_cot: "tan(pi/2 - x) = inverse(tan x)"
   19.33    by (simp add: tan_def sin_diff cos_diff)
   19.34  
   19.35 +subsection \<open>Cotangent\<close>
   19.36 +
   19.37 +definition cot :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
   19.38 +  where "cot = (\<lambda>x. cos x / sin x)"
   19.39 +
   19.40 +lemma cot_of_real:
   19.41 +  "of_real (cot x) = (cot (of_real x) :: 'a::{real_normed_field,banach})"
   19.42 +  by (simp add: cot_def sin_of_real cos_of_real)
   19.43 +
   19.44 +lemma cot_in_Reals [simp]:
   19.45 +  fixes z :: "'a::{real_normed_field,banach}"
   19.46 +  shows "z \<in> \<real> \<Longrightarrow> cot z \<in> \<real>"
   19.47 +  by (simp add: cot_def)
   19.48 +
   19.49 +lemma cot_zero [simp]: "cot 0 = 0"
   19.50 +  by (simp add: cot_def)
   19.51 +
   19.52 +lemma cot_pi [simp]: "cot pi = 0"
   19.53 +  by (simp add: cot_def)
   19.54 +
   19.55 +lemma cot_npi [simp]: "cot (real (n::nat) * pi) = 0"
   19.56 +  by (simp add: cot_def)
   19.57 +
   19.58 +lemma cot_minus [simp]: "cot (-x) = - cot x"
   19.59 +  by (simp add: cot_def)
   19.60 +
   19.61 +lemma cot_periodic [simp]: "cot (x + 2*pi) = cot x"
   19.62 +  by (simp add: cot_def)
   19.63 +  
   19.64 +lemma cot_altdef: "cot x = inverse (tan x)"
   19.65 +  by (simp add: cot_def tan_def)
   19.66 +
   19.67 +lemma tan_altdef: "tan x = inverse (cot x)"
   19.68 +  by (simp add: cot_def tan_def)
   19.69 +
   19.70 +lemma tan_cot': "tan(pi/2 - x) = cot x"
   19.71 +  by (simp add: tan_cot cot_altdef)
   19.72 +
   19.73 +lemma cot_gt_zero: "\<lbrakk>0 < x; x < pi/2\<rbrakk> \<Longrightarrow> 0 < cot x"
   19.74 +  by (simp add: cot_def zero_less_divide_iff sin_gt_zero2 cos_gt_zero_pi)
   19.75 +
   19.76 +lemma cot_less_zero:
   19.77 +  assumes lb: "- pi/2 < x" and "x < 0"
   19.78 +  shows "cot x < 0"
   19.79 +proof -
   19.80 +  have "0 < cot (- x)" using assms by (simp only: cot_gt_zero)
   19.81 +  thus ?thesis by simp
   19.82 +qed
   19.83 +
   19.84 +lemma DERIV_cot [simp]:
   19.85 +  fixes x :: "'a::{real_normed_field,banach}"
   19.86 +  shows "sin x \<noteq> 0 \<Longrightarrow> DERIV cot x :> -inverse ((sin x)\<^sup>2)"
   19.87 +  unfolding cot_def using cos_squared_eq[of x]
   19.88 +  by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
   19.89 +
   19.90 +lemma isCont_cot:
   19.91 +  fixes x :: "'a::{real_normed_field,banach}"
   19.92 +  shows "sin x \<noteq> 0 \<Longrightarrow> isCont cot x"
   19.93 +  by (rule DERIV_cot [THEN DERIV_isCont])
   19.94 +
   19.95 +lemma isCont_cot' [simp,continuous_intros]:
   19.96 +  fixes a :: "'a::{real_normed_field,banach}" and f :: "'a \<Rightarrow> 'a"
   19.97 +  shows "\<lbrakk>isCont f a; sin (f a) \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. cot (f x)) a"
   19.98 +  by (rule isCont_o2 [OF _ isCont_cot])
   19.99 +
  19.100 +lemma tendsto_cot [tendsto_intros]:
  19.101 +  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  19.102 +  shows "\<lbrakk>(f ---> a) F; sin a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. cot (f x)) ---> cot a) F"
  19.103 +  by (rule isCont_tendsto_compose [OF isCont_cot])
  19.104 +
  19.105 +lemma continuous_cot:
  19.106 +  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  19.107 +  shows "continuous F f \<Longrightarrow> sin (f (Lim F (\<lambda>x. x))) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. cot (f x))"
  19.108 +  unfolding continuous_def by (rule tendsto_cot)
  19.109 +
  19.110 +lemma continuous_on_cot [continuous_intros]:
  19.111 +  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  19.112 +  shows "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. sin (f x) \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. cot (f x))"
  19.113 +  unfolding continuous_on_def by (auto intro: tendsto_cot)
  19.114 +
  19.115 +lemma continuous_within_cot [continuous_intros]:
  19.116 +  fixes f :: "'a \<Rightarrow> 'a::{real_normed_field,banach}"
  19.117 +  shows
  19.118 +  "continuous (at x within s) f \<Longrightarrow> sin (f x) \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. cot (f x))"
  19.119 +  unfolding continuous_within by (rule tendsto_cot)
  19.120 +
  19.121 +
  19.122  subsection \<open>Inverse Trigonometric Functions\<close>
  19.123  
  19.124  definition arcsin :: "real => real"