# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1493134794 -3600
# Node ID e4997c181ccef3dc8b96ddf7ee60933d0189d3ea
# Parent  32d4117ad6e8070a813a393bb40da97732af4f60
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series

diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -1727,8 +1727,7 @@
 next
   case False
   then have k: "0 < k" "k < 1" "complex_of_real k \<noteq> 1"
-    using assms apply auto
-    using of_real_eq_iff by fastforce
+    using assms by auto
   have c': "c = k *\<^sub>R (b - a) + a"
     by (metis diff_add_cancel c)
   have bc: "(b - c) = (1 - k) *\<^sub>R (b - a)"
@@ -3871,7 +3870,7 @@
   shows
   "\<lbrakk>valid_path \<gamma>; z \<notin> path_image \<gamma>; w \<noteq> z;
     \<And>a::real. 0 < a \<Longrightarrow> z + a*(w - z) \<notin> path_image \<gamma>\<rbrakk>
-   \<Longrightarrow> \<bar>Re(winding_number \<gamma> z)\<bar> < 1"
+   \<Longrightarrow> Re(winding_number \<gamma> z) < 1"
    by (auto simp: not_less dest: winding_number_big_meets)
 
 text\<open>One way of proving that WN=1 for a loop.\<close>
@@ -6532,6 +6531,21 @@
 apply (force simp add: summable_Re o_def nonneg_Reals_cmod_eq_Re image_subset_iff)
 done
 
+text\<open>Sometimes convenient to compare with a complex series of positive reals. (?)\<close>
+lemma series_differentiable_comparison_complex:
+  fixes S :: "complex set"
+  assumes S: "open S"
+    and hfd: "\<And>n x. x \<in> S \<Longrightarrow> f n field_differentiable (at x)"
+    and to_g: "\<And>x. x \<in> S \<Longrightarrow> \<exists>d h. 0 < d \<and> summable h \<and> range h \<subseteq> \<real>\<^sub>\<ge>\<^sub>0 \<and> (\<forall>\<^sub>F n in sequentially. \<forall>y\<in>ball x d \<inter> S. cmod(f n y) \<le> cmod (h n))"
+  obtains g where "\<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> g field_differentiable (at x)"
+proof -
+  have hfd': "\<And>n x. x \<in> S \<Longrightarrow> (f n has_field_derivative deriv (f n) x) (at x)"
+    using hfd field_differentiable_derivI by blast
+  have "\<exists>g g'. \<forall>x \<in> S. ((\<lambda>n. f n x) sums g x) \<and> ((\<lambda>n. deriv (f n) x) sums g' x) \<and> (g has_field_derivative g' x) (at x)"
+    by (metis series_and_derivative_comparison_complex [OF S hfd' to_g])
+  then show ?thesis
+    using field_differentiable_def that by blast
+qed
 
 text\<open>In particular, a power series is analytic inside circle of convergence.\<close>
 
@@ -7441,5 +7455,4 @@
                          homotopic_paths_imp_homotopic_loops)
 using valid_path_imp_path by blast
 
-
 end
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -709,6 +709,7 @@
   apply (simp only: pos_le_divide_eq [symmetric], linarith)
   done
 
+text\<open>An odd contrast with the much more easily proved @{thm exp_le}\<close>
 lemma e_less_3: "exp 1 < (3::real)"
   using e_approx_32
   by (simp add: abs_if split: if_split_asm)
@@ -1752,7 +1753,7 @@
 declare has_field_derivative_powr[THEN DERIV_chain2, derivative_intros]
 
 
-lemma has_field_derivative_powr_right:
+lemma has_field_derivative_powr_right [derivative_intros]:
     "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
   apply (simp add: powr_def)
   apply (intro derivative_eq_intros | simp)+
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -1244,7 +1244,7 @@
         by (meson Tsb min.cobounded1 order_trans r subset_ball)
       ultimately have False
         using inj_onD [OF injf, of y0 y1] \<open>y0 \<in> T\<close> \<open>y1 \<in> T\<close>
-        using fd [of y0] fd [of y1] complex_root_unity [of n 1]
+        using fd [of y0] fd [of y1] complex_root_unity [of n 1] n_ne
         apply (simp add: y0 y1 power_mult_distrib)
         apply (force simp: algebra_simps)
         done
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -1880,7 +1880,7 @@
   show "G x \<ge> Gamma x"
   proof (rule tendsto_upperbound)
     from G_lower[of x] show "eventually (\<lambda>n. Gamma_series x n \<le> G x) sequentially"
-      using eventually_ge_at_top[of "1::nat"] x by (auto elim!: eventually_mono)
+      using  x by (auto intro: eventually_mono[OF eventually_ge_at_top[of "1::nat"]])
   qed (simp_all add: Gamma_series_LIMSEQ)
 next
   show "G x \<le> Gamma x"
@@ -1891,7 +1891,7 @@
     thus "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x" by simp
   next
     from G_upper[of x] show "eventually (\<lambda>n. Gamma_series x n * (1 + x / real n) \<ge> G x) sequentially"
-      using eventually_ge_at_top[of "2::nat"] x by (auto elim!: eventually_mono)
+      using x by (auto intro: eventually_mono[OF eventually_ge_at_top[of "2::nat"]])
   qed simp_all
 qed
 
@@ -2472,9 +2472,9 @@
   let ?r' = "\<lambda>n. exp (z * of_real (ln (of_nat (Suc n) / of_nat n)))"
   from z have z': "z \<noteq> 0" by auto
 
-  have "eventually (\<lambda>n. ?r' n = ?r n) sequentially" using eventually_gt_at_top[of "0::nat"]
+  have "eventually (\<lambda>n. ?r' n = ?r n) sequentially" 
     using z by (auto simp: divide_simps Gamma_series_def ring_distribs exp_diff ln_div add_ac
-                     elim!: eventually_mono dest: pochhammer_eq_0_imp_nonpos_Int)
+                     intro: eventually_mono eventually_gt_at_top[of "0::nat"] dest: pochhammer_eq_0_imp_nonpos_Int)
   moreover have "?r' \<longlonglongrightarrow> exp (z * of_real (ln 1))"
     by (intro tendsto_intros LIMSEQ_Suc_n_over_n) simp_all
   ultimately show "?r \<longlonglongrightarrow> 1" by (force dest!: Lim_transform_eventually)
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -2578,36 +2578,38 @@
 proof (rule integrable_uniform_limit, safe)
   fix e :: real
   assume e: "e > 0"
-  from compact_uniformly_continuous[OF assms compact_cbox,unfolded uniformly_continuous_on_def,rule_format,OF e] guess d ..
-  note d=conjunctD2[OF this,rule_format]
-  from fine_division_exists[OF gauge_ball[OF d(1)], of a b] guess p . note p=this
-  note p' = tagged_division_ofD[OF p(1)]
+  then obtain d where "0 < d" and d: "\<And>x x'. \<lbrakk>x \<in> cbox a b; x' \<in> cbox a b; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
+    using compact_uniformly_continuous[OF assms compact_cbox] unfolding uniformly_continuous_on_def by metis
+  obtain p where ptag: "p tagged_division_of cbox a b" and finep: "(\<lambda>x. ball x d) fine p"
+    using fine_division_exists[OF gauge_ball[OF \<open>0 < d\<close>], of a b] .
   have *: "\<forall>i\<in>snd ` p. \<exists>g. (\<forall>x\<in>i. norm (f x - g x) \<le> e) \<and> g integrable_on i"
   proof (safe, unfold snd_conv)
     fix x l
     assume as: "(x, l) \<in> p"
-    from p'(4)[OF this] guess a b by (elim exE) note l=this
+    obtain a b where l: "l = cbox a b"
+      using as ptag by blast
+    then have x: "x \<in> cbox a b"
+      using as ptag by auto
     show "\<exists>g. (\<forall>x\<in>l. norm (f x - g x) \<le> e) \<and> g integrable_on l"
       apply (rule_tac x="\<lambda>y. f x" in exI)
     proof safe
       show "(\<lambda>y. f x) integrable_on l"
-        unfolding integrable_on_def l
-        apply rule
-        apply (rule has_integral_const)
-        done
+        unfolding integrable_on_def l by blast
+    next
       fix y
       assume y: "y \<in> l"
-      note fineD[OF p(2) as,unfolded subset_eq,rule_format,OF this]
-      note d(2)[OF _ _ this[unfolded mem_ball]]
+      then have "y \<in> ball x d"
+        using as finep by fastforce
       then show "norm (f y - f x) \<le> e"
-        using y p'(2-3)[OF as] unfolding dist_norm l norm_minus_commute by fastforce
+        using d x y as l
+        by (metis dist_commute dist_norm less_imp_le mem_ball ptag subsetCE tagged_division_ofD(3))
     qed
   qed
   from e have "e \<ge> 0"
     by auto
-  from approximable_on_division[OF this division_of_tagged_division[OF p(1)] *] guess g .
-  then show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
-    by auto
+  from approximable_on_division[OF this division_of_tagged_division[OF ptag] *]
+  show "\<exists>g. (\<forall>x\<in>cbox a b. norm (f x - g x) \<le> e) \<and> g integrable_on cbox a b"
+    by metis
 qed
 
 lemma integrable_continuous_interval:
@@ -6278,89 +6280,6 @@
 qed
 
 
-subsection \<open>Geometric progression\<close>
-
-text \<open>FIXME: Should one or more of these theorems be moved to
-  \<^file>\<open>~~/src/HOL/Set_Interval.thy\<close>, alongside \<open>geometric_sum\<close>?\<close>
-
-lemma sum_gp_basic:
-  fixes x :: "'a::ring_1"
-  shows "(1 - x) * sum (\<lambda>i. x^i) {0 .. n} = (1 - x^(Suc n))"
-proof -
-  define y where "y = 1 - x"
-  have "y * (\<Sum>i=0..n. (1 - y) ^ i) = 1 - (1 - y) ^ Suc n"
-    by (induct n) (simp_all add: algebra_simps)
-  then show ?thesis
-    unfolding y_def by simp
-qed
-
-lemma sum_gp_multiplied:
-  assumes mn: "m \<le> n"
-  shows "((1::'a::{field}) - x) * sum (op ^ x) {m..n} = x^m - x^ Suc n"
-  (is "?lhs = ?rhs")
-proof -
-  let ?S = "{0..(n - m)}"
-  from mn have mn': "n - m \<ge> 0"
-    by arith
-  let ?f = "op + m"
-  have i: "inj_on ?f ?S"
-    unfolding inj_on_def by auto
-  have f: "?f ` ?S = {m..n}"
-    using mn
-    apply (auto simp add: image_iff Bex_def)
-    apply presburger
-    done
-  have th: "op ^ x \<circ> op + m = (\<lambda>i. x^m * x^i)"
-    by (rule ext) (simp add: power_add power_mult)
-  from sum.reindex[OF i, of "op ^ x", unfolded f th sum_distrib_left[symmetric]]
-  have "?lhs = x^m * ((1 - x) * sum (op ^ x) {0..n - m})"
-    by simp
-  then show ?thesis
-    unfolding sum_gp_basic
-    using mn
-    by (simp add: field_simps power_add[symmetric])
-qed
-
-lemma sum_gp:
-  "sum (op ^ (x::'a::{field})) {m .. n} =
-    (if n < m then 0
-     else if x = 1 then of_nat ((n + 1) - m)
-     else (x^ m - x^ (Suc n)) / (1 - x))"
-proof -
-  {
-    assume nm: "n < m"
-    then have ?thesis by simp
-  }
-  moreover
-  {
-    assume "\<not> n < m"
-    then have nm: "m \<le> n"
-      by arith
-    {
-      assume x: "x = 1"
-      then have ?thesis
-        by simp
-    }
-    moreover
-    {
-      assume x: "x \<noteq> 1"
-      then have nz: "1 - x \<noteq> 0"
-        by simp
-      from sum_gp_multiplied[OF nm, of x] nz have ?thesis
-        by (simp add: field_simps)
-    }
-    ultimately have ?thesis by blast
-  }
-  ultimately show ?thesis by blast
-qed
-
-lemma sum_gp_offset:
-  "sum (op ^ (x::'a::{field})) {m .. m+n} =
-    (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
-  unfolding sum_gp[of x m "m + n"] power_Suc
-  by (simp add: field_simps power_add)
-
-
 subsection \<open>Monotone convergence (bounded interval first)\<close>
 
 lemma monotone_convergence_interval:
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Poly_Roots.thy
--- a/src/HOL/Analysis/Poly_Roots.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Poly_Roots.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -8,73 +8,6 @@
 imports Complex_Main
 begin
 
-subsection\<open>Geometric progressions\<close>
-
-lemma sum_gp_basic:
-  fixes x :: "'a::{comm_ring,monoid_mult}"
-  shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
-  by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
-
-lemma sum_gp0:
-  fixes x :: "'a::{comm_ring,division_ring}"
-  shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
-  using sum_gp_basic[of x n]
-  by (simp add: mult.commute divide_simps)
-
-lemma sum_power_add:
-  fixes x :: "'a::{comm_ring,monoid_mult}"
-  shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
-  by (simp add: sum_distrib_left power_add)
-
-lemma sum_power_shift:
-  fixes x :: "'a::{comm_ring,monoid_mult}"
-  assumes "m \<le> n"
-  shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
-proof -
-  have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
-    by (simp add: sum_distrib_left power_add [symmetric])
-  also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
-    using \<open>m \<le> n\<close> by (intro sum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto
-  finally show ?thesis .
-qed
-
-lemma sum_gp_multiplied:
-  fixes x :: "'a::{comm_ring,monoid_mult}"
-  assumes "m \<le> n"
-  shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
-proof -
-  have  "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
-    by (metis mult.assoc mult.commute assms sum_power_shift)
-  also have "... =x^m * (1 - x^Suc(n-m))"
-    by (metis mult.assoc sum_gp_basic)
-  also have "... = x^m - x^Suc n"
-    using assms
-    by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
-  finally show ?thesis .
-qed
-
-lemma sum_gp:
-  fixes x :: "'a::{comm_ring,division_ring}"
-  shows   "(\<Sum>i=m..n. x^i) =
-               (if n < m then 0
-                else if x = 1 then of_nat((n + 1) - m)
-                else (x^m - x^Suc n) / (1 - x))"
-using sum_gp_multiplied [of m n x]
-apply auto
-by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
-
-lemma sum_gp_offset:
-  fixes x :: "'a::{comm_ring,division_ring}"
-  shows   "(\<Sum>i=m..m+n. x^i) =
-       (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
-  using sum_gp [of x m "m+n"]
-  by (auto simp: power_add algebra_simps)
-
-lemma sum_gp_strict:
-  fixes x :: "'a::{comm_ring,division_ring}"
-  shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
-  by (induct n) (auto simp: algebra_simps divide_simps)
-
 subsection\<open>Basics about polynomial functions: extremal behaviour and root counts.\<close>
 
 lemma sub_polyfun:
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Summation_Tests.thy
--- a/src/HOL/Analysis/Summation_Tests.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Summation_Tests.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -246,9 +246,9 @@
 proof (cases "Re s \<le> 0")
   let ?l = "\<lambda>n. complex_of_real (ln (of_nat n))"
   case False
-  with eventually_gt_at_top[of "0::nat"]
-    have "eventually (\<lambda>n. norm (1 :: real) \<le> norm (exp (?l n * s))) sequentially"
-    by (auto intro!: ge_one_powr_ge_zero elim!: eventually_mono)
+  have "eventually (\<lambda>n. norm (1 :: real) \<le> norm (exp (?l n * s))) sequentially"
+    apply (rule eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
+    using False ge_one_powr_ge_zero by auto
   from summable_comparison_test_ev[OF this] False show ?thesis by (auto simp: summable_const_iff)
 next
   let ?l = "\<lambda>n. complex_of_real (ln (of_nat n))"
@@ -387,11 +387,11 @@
     by (auto simp: eventually_at_top_linorder)
   hence A: "p n * f n < p (Suc n) * f (Suc n)" if "n \<ge> N" for n using that N[of n] N[of "Suc n"]
     by (simp add: field_simps)
-  have "p n * f n \<ge> p N * f N" if "n \<ge> N" for n using that and A
-      by (induction n rule: dec_induct) (auto intro!: less_imp_le elim!: order.trans)
-  from eventually_ge_at_top[of N] N this
-    have "eventually (\<lambda>n. norm (p N * f N * inverse (p n)) \<le> f n) sequentially"
-    by (auto elim!: eventually_mono simp: field_simps abs_of_pos)
+  have B: "p n * f n \<ge> p N * f N" if "n \<ge> N" for n using that and A
+    by (induction n rule: dec_induct) (auto intro!: less_imp_le elim!: order.trans)
+  have "eventually (\<lambda>n. norm (p N * f N * inverse (p n)) \<le> f n) sequentially"
+    apply (rule eventually_mono [OF eventually_ge_at_top[of N]])
+    using B N  by (auto  simp: field_simps abs_of_pos)
   from this and \<open>summable f\<close> have "summable (\<lambda>n. p N * f N * inverse (p n))"
     by (rule summable_comparison_test_ev)
   from summable_mult[OF this, of "inverse (p N * f N)"] N[OF le_refl]
@@ -779,9 +779,8 @@
 proof -
   have "limsup (\<lambda>n. ereal (root n (norm (c ^ n * f n)))) =
           limsup (\<lambda>n. ereal (norm c) * ereal (root n (norm (f n))))"
-    using eventually_gt_at_top[of "0::nat"]
-    by (intro Limsup_eq)
-       (auto elim!: eventually_mono simp: norm_mult norm_power real_root_mult real_root_power)
+    by (intro Limsup_eq eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
+       (auto simp: norm_mult norm_power real_root_mult real_root_power)
   also have "\<dots> = ereal (norm c) * limsup (\<lambda>n. ereal (root n (norm (f n))))"
     using assms by (subst Limsup_ereal_mult_left[symmetric]) simp_all
   finally have A: "limsup (\<lambda>n. ereal (root n (norm (c ^ n * f n)))) =
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -398,12 +398,17 @@
     using \<open>k>0\<close> \<open>\<delta>>0\<close> NN  k\<delta>
     apply (force simp add: field_simps)+
     done
-  have NN0: "\<And>e. e>0 \<Longrightarrow> (1/(k*\<delta>))^NN e < e"
-    apply (subst Transcendental.ln_less_cancel_iff [symmetric])
-      prefer 3 apply (subst ln_realpow)
-    using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta>
-    apply (force simp add: field_simps ln_div)+
-    done
+  have NN0: "(1/(k*\<delta>)) ^ (NN e) < e" if "e>0" for e
+  proof -
+    have "0 < ln (real k) + ln \<delta>"
+      using \<delta>01(1) \<open>0 < k\<close> k\<delta>(1) ln_gt_zero by fastforce
+    then have "real (NN e) * ln (1 / (real k * \<delta>)) < ln e"
+      using k\<delta>(1) NN(2) [of e] that by (simp add: ln_div divide_simps)
+    then have "exp (real (NN e) * ln (1 / (real k * \<delta>))) < e"
+      by (metis exp_less_mono exp_ln that)
+    then show ?thesis
+      by (simp add: \<delta>01(1) \<open>0 < k\<close>)
+  qed
   { fix t and e::real
     assume "e>0"
     have "t \<in> S \<inter> V \<Longrightarrow> 1 - q (NN e) t < e" "t \<in> S - U \<Longrightarrow> q (NN e) t < e"
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Complex.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -138,7 +138,7 @@
 end
 
 
-subsection \<open>Numerals, Arithmetic, and Embedding from Reals\<close>
+subsection \<open>Numerals, Arithmetic, and Embedding from \<real>\<close>
 
 abbreviation complex_of_real :: "real \<Rightarrow> complex"
   where "complex_of_real \<equiv> of_real"
@@ -649,10 +649,10 @@
 lemma Im_divide_of_real [simp]: "Im (z / of_real r) = Im z / r"
   by (simp add: Im_divide power2_eq_square)
 
-lemma Re_divide_Reals: "r \<in> Reals \<Longrightarrow> Re (z / r) = Re z / Re r"
+lemma Re_divide_Reals [simp]: "r \<in> \<real> \<Longrightarrow> Re (z / r) = Re z / Re r"
   by (metis Re_divide_of_real of_real_Re)
 
-lemma Im_divide_Reals: "r \<in> Reals \<Longrightarrow> Im (z / r) = Im z / Re r"
+lemma Im_divide_Reals [simp]: "r \<in> \<real> \<Longrightarrow> Im (z / r) = Im z / Re r"
   by (metis Im_divide_of_real of_real_Re)
 
 lemma Re_sum[simp]: "Re (sum f s) = (\<Sum>x\<in>s. Re (f x))"
@@ -691,6 +691,12 @@
 lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm z = \<bar>Re z\<bar>"
   by (simp add: complex_is_Real_iff norm_complex_def)
 
+lemma Re_Reals_divide: "r \<in> \<real> \<Longrightarrow> Re (r / z) = Re r * Re z / (norm z)\<^sup>2"
+  by (simp add: Re_divide complex_is_Real_iff cmod_power2)
+
+lemma Im_Reals_divide: "r \<in> \<real> \<Longrightarrow> Im (r / z) = -Re r * Im z / (norm z)\<^sup>2"
+  by (simp add: Im_divide complex_is_Real_iff cmod_power2)
+
 lemma series_comparison_complex:
   fixes f:: "nat \<Rightarrow> 'a::banach"
   assumes sg: "summable g"
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -913,7 +913,7 @@
   then have "exp (real k * ln y + ln x) > exp 0"
     by (simp add: ac_simps)
   then have "y ^ k * x > 1"
-    unfolding exp_zero exp_add exp_real_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
+    unfolding exp_zero exp_add exp_of_nat_mult exp_ln [OF xp] exp_ln [OF yp]
     by simp
   then have "x > (1 / y)^k" using yp
     by (simp add: field_simps)
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -1987,7 +1987,7 @@
       have "exp x = exp (?num * (x / ?num))"
         using \<open>real ?num \<noteq> 0\<close> by auto
       also have "\<dots> = exp (x / ?num) ^ ?num"
-        unfolding exp_real_of_nat_mult ..
+        unfolding exp_of_nat_mult ..
       also have "\<dots> \<le> exp (float_divr prec x (- floor_fl x)) ^ ?num"
         unfolding num_eq fl_eq
         by (rule power_mono, rule exp_le_cancel_iff[THEN iffD2], rule float_divr) auto
@@ -2023,7 +2023,7 @@
           unfolding num_eq fl_eq
           using float_divl by (auto intro!: power_mono simp del: uminus_float.rep_eq)
         also have "\<dots> = exp (?num * (x / ?num))"
-          unfolding exp_real_of_nat_mult ..
+          unfolding exp_of_nat_mult ..
         also have "\<dots> = exp x"
           using \<open>real ?num \<noteq> 0\<close> by auto
         finally show ?thesis
@@ -2050,7 +2050,7 @@
         hence "real_of_float (Float 1 (- 2)) ^ ?num \<le> exp (x / (- floor_fl x)) ^ ?num"
           by (metis Float_num(5) power_mono zero_le_divide_1_iff zero_le_numeral)
         also have "\<dots> = exp x"
-          unfolding num_eq fl_eq exp_real_of_nat_mult[symmetric]
+          unfolding num_eq fl_eq exp_of_nat_mult[symmetric]
           using \<open>real_of_float (floor_fl x) \<noteq> 0\<close> by auto
         finally show ?thesis
           unfolding lb_exp.simps if_not_P[OF \<open>\<not> 0 < x\<close>] if_P[OF \<open>x < - 1\<close>]
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Filter.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -624,7 +624,7 @@
   shows "eventually P at_top"
   using assms by (auto simp: eventually_at_top_linorder)
 
-lemma eventually_ge_at_top:
+lemma eventually_ge_at_top [simp]:
   "eventually (\<lambda>x. (c::_::linorder) \<le> x) at_top"
   unfolding eventually_at_top_linorder by auto
 
@@ -638,10 +638,10 @@
   finally show ?thesis .
 qed
 
-lemma eventually_at_top_not_equal: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
+lemma eventually_at_top_not_equal [simp]: "eventually (\<lambda>x::'a::{no_top, linorder}. x \<noteq> c) at_top"
   unfolding eventually_at_top_dense by auto
 
-lemma eventually_gt_at_top: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
+lemma eventually_gt_at_top [simp]: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
   unfolding eventually_at_top_dense by auto
 
 lemma eventually_all_ge_at_top:
@@ -664,7 +664,7 @@
   unfolding at_bot_def
   by (subst eventually_INF_base) (auto simp: eventually_principal intro: min.cobounded1 min.cobounded2)
 
-lemma eventually_le_at_bot:
+lemma eventually_le_at_bot [simp]:
   "eventually (\<lambda>x. x \<le> (c::_::linorder)) at_bot"
   unfolding eventually_at_bot_linorder by auto
 
@@ -678,10 +678,10 @@
   finally show ?thesis .
 qed
 
-lemma eventually_at_bot_not_equal: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
+lemma eventually_at_bot_not_equal [simp]: "eventually (\<lambda>x::'a::{no_bot, linorder}. x \<noteq> c) at_bot"
   unfolding eventually_at_bot_dense by auto
 
-lemma eventually_gt_at_bot:
+lemma eventually_gt_at_bot [simp]:
   "eventually (\<lambda>x. x < (c::_::unbounded_dense_linorder)) at_bot"
   unfolding eventually_at_bot_dense by auto
 
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Limits.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -1799,10 +1799,12 @@
   using assms by simp
 
 text \<open>An unbounded sequence's inverse tends to 0.\<close>
-lemma LIMSEQ_inverse_zero: "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0"
+lemma LIMSEQ_inverse_zero:
+  assumes "\<And>r::real. \<exists>N. \<forall>n\<ge>N. r < X n"
+  shows "(\<lambda>n. inverse (X n)) \<longlonglongrightarrow> 0"
   apply (rule filterlim_compose[OF tendsto_inverse_0])
   apply (simp add: filterlim_at_infinity[OF order_refl] eventually_sequentially)
-  apply (metis abs_le_D1 linorder_le_cases linorder_not_le)
+  apply (metis assms abs_le_D1 linorder_le_cases linorder_not_le)
   done
 
 text \<open>The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity.\<close>
@@ -2189,16 +2191,16 @@
   using LIM_offset_zero_cancel[of f a L] LIM_offset_zero[of f L a] by auto
 
 lemma LIM_zero: "(f \<longlongrightarrow> l) F \<Longrightarrow> ((\<lambda>x. f x - l) \<longlongrightarrow> 0) F"
-  for f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+  for f :: "'a \<Rightarrow> 'b::real_normed_vector"
   unfolding tendsto_iff dist_norm by simp
 
 lemma LIM_zero_cancel:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
+  fixes f :: "'a \<Rightarrow> 'b::real_normed_vector"
   shows "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F \<Longrightarrow> (f \<longlongrightarrow> l) F"
 unfolding tendsto_iff dist_norm by simp
 
 lemma LIM_zero_iff: "((\<lambda>x. f x - l) \<longlongrightarrow> 0) F = (f \<longlongrightarrow> l) F"
-  for f :: "'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  for f :: "'a \<Rightarrow> 'b::real_normed_vector"
   unfolding tendsto_iff dist_norm by simp
 
 lemma LIM_imp_LIM:
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Probability/Sinc_Integral.thy
--- a/src/HOL/Probability/Sinc_Integral.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Probability/Sinc_Integral.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -219,12 +219,11 @@
     have *: "0 < x \<Longrightarrow> \<bar>x * sin t + cos t\<bar> / (1 + x\<^sup>2) \<le> (x * 1 + 1) / 1" for x t :: real
       by (intro frac_le abs_triangle_ineq[THEN order_trans] add_mono)
          (auto simp add: abs_mult simp del: mult_1_right intro!: mult_mono)
-    then have **: "1 \<le> t \<Longrightarrow> 0 < x \<Longrightarrow> \<bar>?F x t\<bar> \<le> exp (- x) * (x + 1)" for x t :: real
+    then have "1 \<le> t \<Longrightarrow> 0 < x \<Longrightarrow> \<bar>?F x t\<bar> \<le> exp (- x) * (x + 1)" for x t :: real
         by (auto simp add: abs_mult times_divide_eq_right[symmetric] simp del: times_divide_eq_right
                  intro!:  mult_mono)
-
-    show "\<forall>\<^sub>F i in at_top. AE x in lborel. 0 < x \<longrightarrow> \<bar>?F x i\<bar> \<le> exp (- x) * (x + 1)"
-      using eventually_ge_at_top[of "1::real"] ** by (auto elim: eventually_mono)
+    then show "\<forall>\<^sub>F i in at_top. AE x in lborel. 0 < x \<longrightarrow> \<bar>?F x i\<bar> \<le> exp (- x) * (x + 1)"
+      by (auto intro: eventually_mono eventually_ge_at_top[of "1::real"])
     show "AE x in lborel. 0 < x \<longrightarrow> (?F x \<longlongrightarrow> 0) at_top"
     proof (intro always_eventually impI allI)
       fix x :: real assume "0 < x"
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -364,6 +364,7 @@
   by (auto intro: injI)
 
 lemmas of_real_eq_0_iff [simp] = of_real_eq_iff [of _ 0, simplified]
+lemmas of_real_eq_1_iff [simp] = of_real_eq_iff [of _ 1, simplified]
 
 lemma of_real_eq_id [simp]: "of_real = (id :: real \<Rightarrow> real)"
   by (rule ext) (simp add: of_real_def)
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Set_Interval.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -1892,7 +1892,7 @@
   by (induction m) (simp_all add: algebra_simps)
 
 
-subsubsection \<open>The formula for geometric sums\<close>
+subsection \<open>The formula for geometric sums\<close>
 
 lemma geometric_sum:
   assumes "x \<noteq> 1"
@@ -1947,6 +1947,71 @@
   shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
 by (metis one_diff_power_eq' [of n x] nat_diff_sum_reindex)
 
+lemma sum_gp_basic:
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows "(1 - x) * (\<Sum>i\<le>n. x^i) = 1 - x^Suc n"
+  by (simp only: one_diff_power_eq [of "Suc n" x] lessThan_Suc_atMost)
+
+lemma sum_power_shift:
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  assumes "m \<le> n"
+  shows "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i\<le>n-m. x^i)"
+proof -
+  have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
+    by (simp add: sum_distrib_left power_add [symmetric])
+  also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
+    using \<open>m \<le> n\<close> by (intro sum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto
+  finally show ?thesis .
+qed
+
+lemma sum_gp_multiplied:
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  assumes "m \<le> n"
+  shows "(1 - x) * (\<Sum>i=m..n. x^i) = x^m - x^Suc n"
+proof -
+  have  "(1 - x) * (\<Sum>i=m..n. x^i) = x^m * (1 - x) * (\<Sum>i\<le>n-m. x^i)"
+    by (metis mult.assoc mult.commute assms sum_power_shift)
+  also have "... =x^m * (1 - x^Suc(n-m))"
+    by (metis mult.assoc sum_gp_basic)
+  also have "... = x^m - x^Suc n"
+    using assms
+    by (simp add: algebra_simps) (metis le_add_diff_inverse power_add)
+  finally show ?thesis .
+qed
+
+lemma sum_gp:
+  fixes x :: "'a::{comm_ring,division_ring}"
+  shows   "(\<Sum>i=m..n. x^i) =
+               (if n < m then 0
+                else if x = 1 then of_nat((n + 1) - m)
+                else (x^m - x^Suc n) / (1 - x))"
+using sum_gp_multiplied [of m n x] apply auto
+by (metis eq_iff_diff_eq_0 mult.commute nonzero_divide_eq_eq)
+
+subsection\<open>Geometric progressions\<close>
+
+lemma sum_gp0:
+  fixes x :: "'a::{comm_ring,division_ring}"
+  shows   "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
+  using sum_gp_basic[of x n]
+  by (simp add: mult.commute divide_simps)
+
+lemma sum_power_add:
+  fixes x :: "'a::{comm_ring,monoid_mult}"
+  shows "(\<Sum>i\<in>I. x^(m+i)) = x^m * (\<Sum>i\<in>I. x^i)"
+  by (simp add: sum_distrib_left power_add)
+
+lemma sum_gp_offset:
+  fixes x :: "'a::{comm_ring,division_ring}"
+  shows   "(\<Sum>i=m..m+n. x^i) =
+       (if x = 1 then of_nat n + 1 else x^m * (1 - x^Suc n) / (1 - x))"
+  using sum_gp [of x m "m+n"]
+  by (auto simp: power_add algebra_simps)
+
+lemma sum_gp_strict:
+  fixes x :: "'a::{comm_ring,division_ring}"
+  shows "(\<Sum>i<n. x^i) = (if x = 1 then of_nat n else (1 - x^n) / (1 - x))"
+  by (induct n) (auto simp: algebra_simps divide_simps)
 
 subsubsection \<open>The formula for arithmetic sums\<close>
 
diff -r 32d4117ad6e8 -r e4997c181cce src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Apr 25 08:38:23 2017 +0200
+++ b/src/HOL/Transcendental.thy	Tue Apr 25 16:39:54 2017 +0100
@@ -1506,7 +1506,7 @@
   finally show False by simp
 qed
 
-lemma exp_minus_inverse: "exp x * exp (- x) = 1"
+lemma exp_minus_inverse [simp]: "exp x * exp (- x) = 1"
   by (simp add: exp_add_commuting[symmetric])
 
 lemma exp_minus: "exp (- x) = inverse (exp x)"
@@ -1517,17 +1517,18 @@
   for x :: "'a::{real_normed_field,banach}"
   using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
 
-lemma exp_of_nat_mult: "exp (of_nat n * x) = exp x ^ n"
+lemma exp_of_nat_mult [simp]: "exp (of_nat n * x) = exp x ^ n"
   for x :: "'a::{real_normed_field,banach}"
   by (induct n) (auto simp add: distrib_left exp_add mult.commute)
 
-corollary exp_real_of_nat_mult: "exp (real n * x) = exp x ^ n"
-  by (simp add: exp_of_nat_mult)
+corollary exp_of_nat2_mult [simp]: "exp (x * of_nat n) = exp x ^ n"
+  for x :: "'a::{real_normed_field,banach}"
+  by (metis exp_of_nat_mult mult_of_nat_commute)
 
 lemma exp_sum: "finite I \<Longrightarrow> exp (sum f I) = prod (\<lambda>x. exp (f x)) I"
   by (induct I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
 
-lemma exp_divide_power_eq:
+lemma exp_divide_power_eq [simp]:
   fixes x :: "'a::{real_normed_field,banach}"
   assumes "n > 0"
   shows "exp (x / of_nat n) ^ n = exp x"
@@ -1742,7 +1743,7 @@
   for x :: real
   by (erule subst) (rule ln_exp)
 
-lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
+lemma ln_mult [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
   for x :: real
   by (rule ln_unique) (simp add: exp_add)
 
@@ -1750,7 +1751,7 @@
   for f :: "'a \<Rightarrow> real"
   by (induct I rule: finite_induct) (auto simp: ln_mult prod_pos)
 
-lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
+lemma ln_inverse [simp]: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
   for x :: real
   by (rule ln_unique) (simp add: exp_minus)
 
@@ -1758,8 +1759,8 @@
   for x :: real
   by (rule ln_unique) (simp add: exp_diff)
 
-lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
-  by (rule ln_unique) (simp add: exp_real_of_nat_mult)
+lemma ln_realpow [simp]: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
+  by (rule ln_unique) simp
 
 lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
   for x :: real
@@ -1781,6 +1782,9 @@
   for x :: real
   by (rule order_less_le_trans [where y = "ln (1 + x)"]) simp_all
 
+lemma ln_ge_iff: "\<And>x::real. 0 < x \<Longrightarrow> y \<le> ln x \<longleftrightarrow> exp y \<le> x"
+  using exp_le_cancel_iff exp_total by force
+
 lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
   for x :: real
   using ln_le_cancel_iff [of 1 x] by simp
@@ -2298,7 +2302,7 @@
   also from assms False have "ln (1 + x / real n) \<le> x / real n"
     by (intro ln_add_one_self_le_self2) (simp_all add: field_simps)
   with assms have "exp (of_nat n * ln (1 + x / of_nat n)) \<le> exp x"
-    by (simp add: field_simps)
+    by (simp add: field_simps del: exp_of_nat_mult)
   finally show ?thesis .
 next
   case True
@@ -2701,7 +2705,7 @@
 lemma powr_realpow: "0 < x \<Longrightarrow> x powr (real n) = x^n"
   by (induct n) (simp_all add: ac_simps powr_add)
 
-lemma powr_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
+lemma powr_numeral [simp]: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
   by (metis of_nat_numeral powr_realpow)
 
 lemma numeral_powr_numeral[simp]:
@@ -2841,14 +2845,26 @@
   for x :: real
   by (simp add: powr_def)
 
-lemma powr_mono2: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> x powr a \<le> y powr a"
+lemma powr_mono2: "x powr a \<le> y powr a" if "0 \<le> a" "0 \<le> x" "x \<le> y"
   for x :: real
-  apply (case_tac "a = 0")
-   apply simp
-  apply (case_tac "x = y")
-   apply simp
-  apply (metis dual_order.strict_iff_order powr_less_mono2)
-  done
+proof (cases "a = 0")
+  case True
+  with that show ?thesis by simp
+next
+  case False show ?thesis
+  proof (cases "x = y")
+    case True
+    then show ?thesis by simp
+  next
+    case False
+    then show ?thesis
+      by (metis dual_order.strict_iff_order powr_less_mono2 that \<open>a \<noteq> 0\<close>)
+  qed
+qed
+
+lemma powr_le1: "0 \<le> a \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> x powr a \<le> 1"
+  for x :: real
+  using powr_mono2 by fastforce
 
 lemma powr_mono2':
   fixes a x y :: real
@@ -2861,6 +2877,12 @@
     by (auto simp add: powr_minus field_simps)
 qed
 
+lemma powr_mono_both:
+  fixes x :: real
+  assumes "0 \<le> a" "a \<le> b" "1 \<le> x" "x \<le> y"
+    shows "x powr a \<le> y powr b"
+  by (meson assms order.trans powr_mono powr_mono2 zero_le_one)
+
 lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
   for x :: real
   unfolding powr_def exp_inj_iff by simp