# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1653405709 -3600
# Node ID 7448423e5dbaa63a6acc97828810bdd3af9f0874
# Parent  4c3bc0d2568f19fc11510010ff2cc53497715724
Renamed the misleading has_field_derivative_iff_has_vector_derivative. Inserted a number of minor lemmas

diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Tue May 24 16:21:49 2022 +0100
@@ -3388,7 +3388,7 @@
            integral S (\<lambda>x. \<bar>g' x\<bar> *\<^sub>R vec (f(g x))) = (vec b :: real ^ 1)
          \<longleftrightarrow> (\<lambda>x. vec (f x) :: real ^ 1) absolutely_integrable_on (g ` S) \<and>
            integral (g ` S) (\<lambda>x. vec (f x)) = (vec b :: real ^ 1)"
-    using assms unfolding has_field_derivative_iff_has_vector_derivative
+    using assms unfolding has_real_derivative_iff_has_vector_derivative
     by (intro has_absolute_integral_change_of_variables_1 assms) auto
   thus ?thesis
     by (simp add: absolutely_integrable_on_1_iff integral_on_1_eq)
diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Tue May 24 16:21:49 2022 +0100
@@ -3830,7 +3830,7 @@
 
   have "(f has_integral F b - F a) {a..b}"
     by (intro fundamental_theorem_of_calculus)
-       (auto simp: has_field_derivative_iff_has_vector_derivative[symmetric]
+       (auto simp: has_real_derivative_iff_has_vector_derivative[symmetric]
              intro: has_field_derivative_subset[OF f(1)] \<open>a \<le> b\<close>)
   then have i: "((\<lambda>x. f x * indicator {a .. b} x) has_integral F b - F a) UNIV"
     unfolding indicator_def of_bool_def if_distrib[where f="\<lambda>x. a * x" for a]
@@ -3881,7 +3881,7 @@
     and integral_FTC_Icc_real: "(\<integral>x. f x * indicator {a .. b} x \<partial>lborel) = F b - F a" (is ?eq)
 proof -
   have 1: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (F has_vector_derivative f x) (at x within {a .. b})"
-    unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+    unfolding has_real_derivative_iff_has_vector_derivative[symmetric]
     using deriv by (auto intro: DERIV_subset)
   have 2: "continuous_on {a .. b} f"
     using cont by (intro continuous_at_imp_continuous_on) auto
diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue May 24 16:21:49 2022 +0100
@@ -795,6 +795,11 @@
   using has_integral_eq[of s f g] has_integral_eq[of s g f] assms
   by auto
 
+lemma integrable_cong:
+  assumes "\<And>x. x \<in> A \<Longrightarrow> f x = g x"
+  shows   "f integrable_on A \<longleftrightarrow> g integrable_on A"
+  using has_integral_cong [OF assms] by fast
+
 lemma integral_cong:
   assumes "\<And>x. x \<in> s \<Longrightarrow> f x = g x"
   shows "integral s f = integral s g"
@@ -2712,6 +2717,13 @@
   qed
 qed
 
+lemma has_complex_derivative_imp_has_vector_derivative:
+  fixes f :: "complex \<Rightarrow> complex"
+  assumes "(f has_field_derivative f') (at (of_real a) within (cbox (of_real x) (of_real y)))"
+  shows "((f o of_real) has_vector_derivative f') (at a within {x..y})"
+  using has_derivative_in_compose[of of_real of_real a "{x..y}" f "(*) f'"] assms
+  by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def o_def cbox_complex_of_real)
+
 lemma ident_has_integral:
   fixes a::real
   assumes "a \<le> b"
@@ -2742,7 +2754,7 @@
   have "(sin has_integral (- cos b - - cos a)) {a..b}"
   proof (rule fundamental_theorem_of_calculus)
     show "((\<lambda>a. - cos a) has_vector_derivative sin x) (at x within {a..b})" for x
-      unfolding has_field_derivative_iff_has_vector_derivative [symmetric]
+      unfolding has_real_derivative_iff_has_vector_derivative [symmetric]
       by (rule derivative_eq_intros | force)+
   qed (use assms in auto)
   then show ?thesis
@@ -2756,13 +2768,20 @@
   have "(cos has_integral (sin b - sin a)) {a..b}"
   proof (rule fundamental_theorem_of_calculus)
     show "(sin has_vector_derivative cos x) (at x within {a..b})" for x
-      unfolding has_field_derivative_iff_has_vector_derivative [symmetric]
+      unfolding has_real_derivative_iff_has_vector_derivative [symmetric]
       by (rule derivative_eq_intros | force)+
   qed (use assms in auto)
   then show ?thesis
     by (simp add: integral_unique)
 qed
 
+lemma integral_exp [simp]:
+  fixes a::real
+  assumes "a \<le> b" shows "integral {a..b} exp = exp b - exp a"
+  by (meson DERIV_exp assms fundamental_theorem_of_calculus has_real_derivative_iff_has_vector_derivative
+       has_vector_derivative_at_within integral_unique)
+
+
 lemma has_integral_sin_nx: "((\<lambda>x. sin(real_of_int n * x)) has_integral 0) {-pi..pi}"
 proof (cases "n = 0")
   case False
@@ -3265,7 +3284,7 @@
   assumes "t \<in> {a..b}"
   shows "((\<lambda>x. integral {a..x} g) has_real_derivative g t) (at t within {a..b})"
   using integral_has_vector_derivative[of a b g t] assms
-  by (auto simp: has_field_derivative_iff_has_vector_derivative)
+  by (auto simp: has_real_derivative_iff_has_vector_derivative)
 
 lemma antiderivative_continuous:
   fixes q b :: real
@@ -3533,6 +3552,11 @@
   using assms has_integral_cmul[of f I A c]
         has_integral_cmul[of "\<lambda>x. c *\<^sub>R f x" "c *\<^sub>R I" A "inverse c"] by (auto simp: field_simps)
 
+lemma has_integral_cmul_iff':
+  assumes "c \<noteq> 0"
+  shows   "((\<lambda>x. c *\<^sub>R f x) has_integral I) A \<longleftrightarrow> (f has_integral I /\<^sub>R c) A"
+  using assms by (metis divideR_right has_integral_cmul_iff)
+
 lemma has_integral_affinity':
   fixes a :: "'a::euclidean_space"
   assumes "(f has_integral i) (cbox a b)" and "m > 0"
@@ -4369,7 +4393,7 @@
   assumes "t \<in> {a..b}"
   shows "((\<lambda>x. integral {x..b} g) has_real_derivative -g t) (at t within {a..b})"
   using integral_has_vector_derivative'[OF assms]
-  by (auto simp: has_field_derivative_iff_has_vector_derivative)
+  by (auto simp: has_real_derivative_iff_has_vector_derivative)
 
 
 subsection \<open>This doesn't directly involve integration, but that gives an easy proof\<close>
@@ -4990,6 +5014,21 @@
   shows "integral(box a b) f = integral(cbox a b) f"
   by (metis has_integral_integrable_integral has_integral_open_interval not_integrable_integral)
 
+lemma has_integral_Icc_iff_Ioo:
+  fixes f :: "real \<Rightarrow> 'a :: banach"
+  shows "(f has_integral I) {a..b} \<longleftrightarrow> (f has_integral I) {a<..<b}"
+proof (rule has_integral_spike_set_eq)
+  show "negligible {x \<in> {a..b} - {a<..<b}. f x \<noteq> 0}"
+    by (rule negligible_subset [of "{a,b}"]) auto
+  show "negligible {x \<in> {a<..<b} - {a..b}. f x \<noteq> 0}"
+    by (rule negligible_subset [of "{}"]) auto
+qed
+
+lemma integrable_on_Icc_iff_Ioo:
+  fixes f :: "real \<Rightarrow> 'a :: banach"
+  shows "f integrable_on {a..b} \<longleftrightarrow> f integrable_on {a<..<b}"
+  using has_integral_Icc_iff_Ioo by blast
+
 
 subsection \<open>More lemmas that are useful later\<close>
 
@@ -6458,7 +6497,7 @@
     have M': "M' \<ge> a" "M' \<ge> M" unfolding M'_def by linarith+
     have int_g: "(g has_integral (G (real n) - G (real m))) {real m..real n}"
       using 1 M' by (intro fundamental_theorem_of_calculus) 
-                    (auto simp: has_field_derivative_iff_has_vector_derivative [symmetric] 
+                    (auto simp: has_real_derivative_iff_has_vector_derivative [symmetric] 
                           intro!: DERIV_subset[OF deriv])
     have int_f: "f x integrable_on {a'..real n}" if "a' \<ge> a" for a'
       using that 1 by (cases "a' \<le> real n") (auto intro: integrable)
@@ -6907,7 +6946,7 @@
                  (at x within {a..b})" if "x \<in> {a..b} - s" for x
   proof (rule has_vector_derivative_eq_rhs [OF vector_diff_chain_within refl])
     show "(g has_vector_derivative g' x) (at x within {a..b})"
-      using deriv has_field_derivative_iff_has_vector_derivative that by blast
+      using deriv has_real_derivative_iff_has_vector_derivative that by blast
     show "((\<lambda>x. integral {c..x} f) has_vector_derivative f (g x)) 
           (at (g x) within g ` {a..b})"
       using that le subset
@@ -7320,7 +7359,7 @@
       have "((\<lambda>x. exp (-a*x)) has_integral (-exp (-a*real k)/a - (-exp (-a*c)/a))) {c..real k}"
       by (intro fundamental_theorem_of_calculus)
          (auto intro!: derivative_eq_intros
-               simp: has_field_derivative_iff_has_vector_derivative [symmetric])
+               simp: has_real_derivative_iff_has_vector_derivative [symmetric])
     hence "(f k has_integral (exp (-a*c)/a - exp (-a*real k)/a)) {c..}" unfolding f_def
       by (subst has_integral_restrict) simp_all
   } note has_integral_f = this
@@ -7409,7 +7448,7 @@
                inverse (real (Suc k)) powr (a + 1) / (a + 1)) {inverse (real (Suc k))..c}"
         using True a by (intro fundamental_theorem_of_calculus)
            (auto intro!: derivative_eq_intros continuous_on_powr' continuous_on_const
-              simp: has_field_derivative_iff_has_vector_derivative [symmetric])
+              simp: has_real_derivative_iff_has_vector_derivative [symmetric])
       with True show ?thesis unfolding f_def F_def by (subst has_integral_restrict) simp_all
     next
       case False
@@ -7494,7 +7533,7 @@
   proof -
     from n assms have "((\<lambda>x. x powr e) has_integral (F n - F a)) {a..n}"
       by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros
-            simp: has_field_derivative_iff_has_vector_derivative [symmetric] F_def)
+            simp: has_real_derivative_iff_has_vector_derivative [symmetric] F_def)
     hence "(f n has_integral (F n - F a)) {a..n}"
       by (rule has_integral_eq [rotated]) (simp add: f_def)
     thus "(f n has_integral (F n - F a)) {a..}"
diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Analysis/Infinite_Sum.thy
--- a/src/HOL/Analysis/Infinite_Sum.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Infinite_Sum.thy	Tue May 24 16:21:49 2022 +0100
@@ -696,11 +696,45 @@
   shows \<open>infsum f (A \<union> B) = infsum f A + infsum f B\<close>
   by (intro infsumI has_sum_Un_disjoint has_sum_infsum assms)  
 
-(* TODO move *)
-lemma (in uniform_space) cauchy_filter_complete_converges:
-  assumes "cauchy_filter F" "complete A" "F \<le> principal A" "F \<noteq> bot"
-  shows   "\<exists>c. F \<le> nhds c"
-  using assms unfolding complete_uniform by blast
+lemma norm_summable_imp_has_sum:
+  fixes f :: "nat \<Rightarrow> 'a :: banach"
+  assumes "summable (\<lambda>n. norm (f n))" and "f sums S"
+  shows   "has_sum f (UNIV :: nat set) S"
+  unfolding has_sum_def tendsto_iff eventually_finite_subsets_at_top
+proof (safe, goal_cases)
+  case (1 \<epsilon>)
+  from assms(1) obtain S' where S': "(\<lambda>n. norm (f n)) sums S'"
+    by (auto simp: summable_def)
+  with 1 obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> \<bar>S' - (\<Sum>i<n. norm (f i))\<bar> < \<epsilon>"
+    by (auto simp: tendsto_iff eventually_at_top_linorder sums_def dist_norm abs_minus_commute)
+  
+  show ?case
+  proof (rule exI[of _ "{..<N}"], safe, goal_cases)
+    case (2 Y)
+    from 2 have "(\<lambda>n. if n \<in> Y then 0 else f n) sums (S - sum f Y)"
+      by (intro sums_If_finite_set'[OF \<open>f sums S\<close>]) (auto simp: sum_negf)
+    hence "S - sum f Y = (\<Sum>n. if n \<in> Y then 0 else f n)"
+      by (simp add: sums_iff)
+    also have "norm \<dots> \<le> (\<Sum>n. norm (if n \<in> Y then 0 else f n))"
+      by (rule summable_norm[OF summable_comparison_test'[OF assms(1)]]) auto
+    also have "\<dots> \<le> (\<Sum>n. if n < N then 0 else norm (f n))"
+      using 2 by (intro suminf_le summable_comparison_test'[OF assms(1)]) auto
+    also have "(\<lambda>n. if n \<in> {..<N} then 0 else norm (f n)) sums (S' - (\<Sum>i<N. norm (f i)))" 
+      by (intro sums_If_finite_set'[OF S']) (auto simp: sum_negf)
+    hence "(\<Sum>n. if n < N then 0 else norm (f n)) = S' - (\<Sum>i<N. norm (f i))"
+      by (simp add: sums_iff)
+    also have "S' - (\<Sum>i<N. norm (f i)) \<le> \<bar>S' - (\<Sum>i<N. norm (f i))\<bar>" by simp
+    also have "\<dots> < \<epsilon>" by (rule N) auto
+    finally show ?case by (simp add: dist_norm norm_minus_commute)
+  qed auto
+qed
+
+lemma norm_summable_imp_summable_on:
+  fixes f :: "nat \<Rightarrow> 'a :: banach"
+  assumes "summable (\<lambda>n. norm (f n))"
+  shows   "f summable_on UNIV"
+  using norm_summable_imp_has_sum[OF assms, of "suminf f"] assms
+  by (auto simp: sums_iff summable_on_def dest: summable_norm_cancel)
 
 text \<open>The following lemma indeed needs a complete space (as formalized by the premise \<^term>\<open>complete UNIV\<close>).
   The following two counterexamples show this:
diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy	Tue May 24 16:21:49 2022 +0100
@@ -653,7 +653,7 @@
   have FTCi: "\<And>i. (LBINT x=l i..u i. f x) = F (u i) - F (l i)"
     using assms approx apply (intro interval_integral_FTC_finite)
     apply (auto simp: less_imp_le min_def max_def
-      has_field_derivative_iff_has_vector_derivative[symmetric])
+      has_real_derivative_iff_has_vector_derivative[symmetric])
     apply (rule continuous_at_imp_continuous_on, auto intro!: f)
     by (rule DERIV_subset [OF F], auto)
   have 1: "\<And>i. set_integrable lborel {l i..u i} f"
@@ -807,7 +807,7 @@
   shows "LBINT x=a..b. g' x *\<^sub>R f (g x) = LBINT y=g a..g b. f y"
 proof-
   have v_derivg: "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> (g has_vector_derivative (g' x)) (at x within {a..b})"
-    using derivg unfolding has_field_derivative_iff_has_vector_derivative .
+    using derivg unfolding has_real_derivative_iff_has_vector_derivative .
   then have contg [simp]: "continuous_on {a..b} g"
     by (rule continuous_on_vector_derivative) auto
   have 1: "\<exists>x\<in>{a..b}. u = g x" if "min (g a) (g b) \<le> u" "u \<le> max (g a) (g b)" for u
@@ -920,7 +920,7 @@
   (* finally, the main argument *)
   have eq1: "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)" for i
     apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
-    unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+    unfolding has_real_derivative_iff_has_vector_derivative[symmetric]
          apply (auto intro!: continuous_at_imp_continuous_on contf contg')
     done
   have "(\<lambda>i. LBINT x=l i..u i. g' x *\<^sub>R f (g x)) \<longlonglongrightarrow> (LBINT x=a..b. g' x *\<^sub>R f (g x))"
@@ -1023,7 +1023,7 @@
   proof -
     have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
       apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
-      unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
+      unfolding has_real_derivative_iff_has_vector_derivative[symmetric]
            apply (auto simp: less_imp_le intro!: continuous_at_imp_continuous_on contf contg')
       done
     then show ?thesis
@@ -1124,6 +1124,6 @@
 (* TODO: should we have a library of facts like these? *)
 lemma integral_cos: "t \<noteq> 0 \<Longrightarrow> LBINT x=a..b. cos (t * x) = sin (t * b) / t - sin (t * a) / t"
   apply (intro interval_integral_FTC_finite continuous_intros)
-  by (auto intro!: derivative_eq_intros simp: has_field_derivative_iff_has_vector_derivative[symmetric])
+  by (auto intro!: derivative_eq_intros simp: has_real_derivative_iff_has_vector_derivative[symmetric])
 
 end
diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Analysis/Lebesgue_Integral_Substitution.thy
--- a/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Lebesgue_Integral_Substitution.thy	Tue May 24 16:21:49 2022 +0100
@@ -30,7 +30,7 @@
                              Mg': "set_borel_measurable borel {a..b} g'"
       by (simp_all only: set_measurable_continuous_on_ivl)
   from derivg have derivg': "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative g' x) (at x)"
-    by (simp only: has_field_derivative_iff_has_vector_derivative)
+    by (simp only: has_real_derivative_iff_has_vector_derivative)
 
   have real_ind[simp]: "\<And>A x. enn2real (indicator A x) = indicator A x"
       by (auto split: split_indicator)
@@ -73,7 +73,7 @@
         hence B: "\<And>x. min u' v' \<le> x \<Longrightarrow> x \<le> max u' v' \<Longrightarrow>
                       (g has_vector_derivative g' x) (at x within {min u' v'..max u' v'})"
             by (simp only: u'v' max_absorb2 min_absorb1)
-               (auto simp: has_field_derivative_iff_has_vector_derivative)
+               (auto simp: has_real_derivative_iff_has_vector_derivative)
           have "integrable lborel (\<lambda>x. indicator ({a..b} \<inter> g -` {u..v}) x *\<^sub>R g' x)"
             using set_integrable_subset borel_integrable_atLeastAtMost'[OF contg']
             by (metis \<open>{u'..v'} \<subseteq> {a..b}\<close> eucl_ivals(5) set_integrable_def sets_lborel u'v'(1))
diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue May 24 16:21:49 2022 +0100
@@ -815,6 +815,14 @@
   "x \<in> cbox a b \<longleftrightarrow> Re x \<in> {Re a..Re b} \<and> Im x \<in> {Im a..Im b}"
   by (cases x; cases a; cases b) (auto simp: cbox_Complex_eq)
 
+lemma cbox_complex_of_real: "cbox (complex_of_real x) (complex_of_real y) = complex_of_real ` {x..y}"
+proof -
+  have "(x \<le> Re z \<and> Re z \<le> y \<and> Im z = 0) = (z \<in> complex_of_real ` {x..y})" for z
+    by (cases z) (simp add: complex_eq_cancel_iff2 image_iff)
+  then show ?thesis
+    by (auto simp: in_cbox_complex_iff)
+qed
+
 lemma box_Complex_eq:
   "box (Complex a c) (Complex b d) = (\<lambda>(x,y). Complex x y) ` (box a b \<times> box c d)"
   by (auto simp: box_def Basis_complex_def image_iff complex_eq_iff)
@@ -823,6 +831,9 @@
   "x \<in> box a b \<longleftrightarrow> Re x \<in> {Re a<..<Re b} \<and> Im x \<in> {Im a<..<Im b}"
   by (cases x; cases a; cases b) (auto simp: box_Complex_eq)
 
+lemma box_complex_of_real [simp]: "box (complex_of_real x) (complex_of_real y) = {}"
+  by (auto simp: in_box_complex_iff)
+
 lemma Int_interval:
   fixes a :: "'a::euclidean_space"
   shows "cbox a b \<inter> cbox c d =
diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Deriv.thy	Tue May 24 16:21:49 2022 +0100
@@ -841,14 +841,15 @@
 
 subsection \<open>Vector derivative\<close>
 
-lemma has_field_derivative_iff_has_vector_derivative:
-  "(f has_field_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F"
+text \<open>It's for real derivatives only, and not obviously generalisable to field derivatives\<close>
+lemma has_real_derivative_iff_has_vector_derivative:
+  "(f has_real_derivative y) F \<longleftrightarrow> (f has_vector_derivative y) F"
   unfolding has_vector_derivative_def has_field_derivative_def real_scaleR_def mult_commute_abs ..
 
 lemma has_field_derivative_subset:
   "(f has_field_derivative y) (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow>
     (f has_field_derivative y) (at x within t)"
-  unfolding has_field_derivative_def by (rule has_derivative_subset)
+  by (fact DERIV_subset)
 
 lemma has_vector_derivative_const[simp, derivative_intros]: "((\<lambda>x. c) has_vector_derivative 0) net"
   by (auto simp: has_vector_derivative_def)
@@ -903,7 +904,7 @@
 lemma has_vector_derivative_scaleR[derivative_intros]:
   "(f has_field_derivative f') (at x within s) \<Longrightarrow> (g has_vector_derivative g') (at x within s) \<Longrightarrow>
     ((\<lambda>x. f x *\<^sub>R g x) has_vector_derivative (f x *\<^sub>R g' + f' *\<^sub>R g x)) (at x within s)"
-  unfolding has_field_derivative_iff_has_vector_derivative
+  unfolding has_real_derivative_iff_has_vector_derivative
   by (rule bounded_bilinear.has_vector_derivative[OF bounded_bilinear_scaleR])
 
 lemma has_vector_derivative_mult[derivative_intros]:
@@ -915,7 +916,7 @@
 lemma has_vector_derivative_of_real[derivative_intros]:
   "(f has_field_derivative D) F \<Longrightarrow> ((\<lambda>x. of_real (f x)) has_vector_derivative (of_real D)) F"
   by (rule bounded_linear.has_vector_derivative[OF bounded_linear_of_real])
-    (simp add: has_field_derivative_iff_has_vector_derivative)
+    (simp add: has_real_derivative_iff_has_vector_derivative)
 
 lemma has_vector_derivative_real_field:
   "(f has_field_derivative f') (at (of_real a)) \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Library/Landau_Symbols.thy
--- a/src/HOL/Library/Landau_Symbols.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Library/Landau_Symbols.thy	Tue May 24 16:21:49 2022 +0100
@@ -508,6 +508,16 @@
 
 end
 
+lemma summable_comparison_test_bigo:
+  fixes f :: "nat \<Rightarrow> real"
+  assumes "summable (\<lambda>n. norm (g n))" "f \<in> O(g)"
+  shows   "summable f"
+proof -
+  from \<open>f \<in> O(g)\<close> obtain C where C: "eventually (\<lambda>x. norm (f x) \<le> C * norm (g x)) at_top"
+    by (auto elim: landau_o.bigE)
+  thus ?thesis
+    by (rule summable_comparison_test_ev) (insert assms, auto intro: summable_mult)
+qed
 
 lemma bigomega_iff_bigo: "g \<in> \<Omega>[F](f) \<longleftrightarrow> f \<in> O[F](g)"
 proof
diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Probability/Characteristic_Functions.thy
--- a/src/HOL/Probability/Characteristic_Functions.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Probability/Characteristic_Functions.thy	Tue May 24 16:21:49 2022 +0100
@@ -238,7 +238,7 @@
     have "LBINT s=0..x. (x - s)^n = ?F x - ?F 0"
       unfolding zero_ereal_def
       by (intro interval_integral_FTC_finite continuous_at_imp_continuous_on
-                has_field_derivative_iff_has_vector_derivative[THEN iffD1])
+                has_real_derivative_iff_has_vector_derivative[THEN iffD1])
          (auto simp del: power_Suc intro!: derivative_eq_intros simp add: add_nonneg_eq_0_iff)
     also have "\<dots> = x ^ (Suc n) / (Suc n)" by simp
     finally show ?thesis .
diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Probability/Sinc_Integral.thy
--- a/src/HOL/Probability/Sinc_Integral.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Probability/Sinc_Integral.thy	Tue May 24 16:21:49 2022 +0100
@@ -48,7 +48,7 @@
 proof (subst interval_integral_FTC_finite)
   show "(?F has_vector_derivative exp (- (u * x)) * sin x) (at x within {min 0 t..max 0 t})" for x
     by (auto intro!: derivative_eq_intros
-             simp: has_field_derivative_iff_has_vector_derivative[symmetric] power2_eq_square)
+             simp: has_real_derivative_iff_has_vector_derivative[symmetric] power2_eq_square)
        (simp_all add: field_simps add_nonneg_eq_0_iff)
 qed (auto intro: continuous_at_imp_continuous_on)
 
@@ -197,7 +197,7 @@
   ultimately show ?thesis
     using interval_integral_FTC2[of "min 0 (x - 1)" 0 "max 0 (x + 1)" sinc x]
     by (auto simp: continuous_at_imp_continuous_on isCont_sinc Si_alt_def[abs_def] zero_ereal_def
-                   has_field_derivative_iff_has_vector_derivative
+                   has_real_derivative_iff_has_vector_derivative
              split del: if_split)
 qed
 
diff -r 4c3bc0d2568f -r 7448423e5dba src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Mon May 23 17:21:57 2022 +0100
+++ b/src/HOL/Topological_Spaces.thy	Tue May 24 16:21:49 2022 +0100
@@ -3415,6 +3415,11 @@
   where complete_uniform: "complete S \<longleftrightarrow>
     (\<forall>F \<le> principal S. F \<noteq> bot \<longrightarrow> cauchy_filter F \<longrightarrow> (\<exists>x\<in>S. F \<le> nhds x))"
 
+lemma (in uniform_space) cauchy_filter_complete_converges:
+  assumes "cauchy_filter F" "complete A" "F \<le> principal A" "F \<noteq> bot"
+  shows   "\<exists>c. F \<le> nhds c"
+  using assms unfolding complete_uniform by blast
+
 end
 
 subsubsection \<open>Uniformly continuous functions\<close>