# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1565881916 -3600
# Node ID fcf3b891ccb14f011eee31bdb34aff209c9dafc6
# Parent  2d2b5a8e8d59c920dbbc106e83946df17b34cf44
new material; rotated premises of Lim_transform_eventually

diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Abstract_Topology.thy
--- a/src/HOL/Analysis/Abstract_Topology.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Abstract_Topology.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -3985,7 +3985,7 @@
   ultimately
   have "\<forall>\<^sub>F x in at a within T. f x = g x"
     by eventually_elim (auto simp: \<open>S = _\<close> eq)
-  then show ?thesis using f
+  with f show ?thesis
     by (rule Lim_transform_eventually)
 qed
 
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Bochner_Integration.thy
--- a/src/HOL/Analysis/Bochner_Integration.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -1581,12 +1581,17 @@
 
 end
 
-lemma integrable_mult_left_iff:
+lemma integrable_mult_left_iff [simp]:
   fixes f :: "'a \<Rightarrow> real"
   shows "integrable M (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> integrable M f"
   using integrable_mult_left[of c M f] integrable_mult_left[of "1 / c" M "\<lambda>x. c * f x"]
   by (cases "c = 0") auto
 
+lemma integrable_mult_right_iff [simp]:
+  fixes f :: "'a \<Rightarrow> real"
+  shows "integrable M (\<lambda>x. f x * c) \<longleftrightarrow> c = 0 \<or> integrable M f"
+  using integrable_mult_left_iff [of M c f] by (simp add: mult.commute)
+
 lemma integrableI_nn_integral_finite:
   assumes [measurable]: "f \<in> borel_measurable M"
     and nonneg: "AE x in M. 0 \<le> f x"
@@ -2939,7 +2944,7 @@
           have "(\<integral>\<^sup>+ y. ennreal (norm (s i (x, y))) \<partial>M) \<le> (\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M)"
             using x s by (intro nn_integral_mono) auto
           also have "(\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M) < \<infinity>"
-            using int_2f by (simp add: integrable_iff_bounded)
+            using int_2f unfolding integrable_iff_bounded by simp
           finally show "(\<integral>\<^sup>+ xa. ennreal (norm (s i (x, xa))) \<partial>M) < \<infinity>" .
         qed
         then have "integral\<^sup>L M (\<lambda>y. s i (x, y)) = simple_bochner_integral M (\<lambda>y. s i (x, y))"
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -6481,7 +6481,7 @@
   have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
         sums contour_integral (circlepath z r) (\<lambda>u. f u/(u - w))"
     unfolding sums_def
-    apply (intro Lim_transform_eventually [OF eq] contour_integral_uniform_limit_circlepath [OF eventuallyI ul] cic)
+    apply (intro Lim_transform_eventually [OF _ eq] contour_integral_uniform_limit_circlepath [OF eventuallyI ul] cic)
     using \<open>0 < r\<close> apply auto
     done
   then have "(\<lambda>k. contour_integral (circlepath z r) (\<lambda>u. f u/(u - z)^(Suc k)) * (w - z)^k)
@@ -6715,7 +6715,7 @@
     then have tendsto_0: "((\<lambda>n. 1 / (2 * of_real pi * \<i>) * (?conint (\<lambda>x. f n x / (x - w)\<^sup>2) - ?conint (\<lambda>x. g x / (x - w)\<^sup>2))) \<longlongrightarrow> 0) F"
       using Lim_null by (force intro!: tendsto_mult_right_zero)
     have "((\<lambda>n. f' n w - g' w) \<longlongrightarrow> 0) F"
-      apply (rule Lim_transform_eventually [OF _ tendsto_0])
+      apply (rule Lim_transform_eventually [OF tendsto_0])
       apply (force simp: divide_simps intro: eq_f' eventually_mono [OF cont])
       done
     then show ?thesis using Lim_null by blast
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Change_Of_Vars.thy
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -2012,7 +2012,7 @@
         by auto
     qed
     then show ?thesis
-      unfolding borel_measurable_lebesgue_preimage_borel borel_measurable_UNIV [OF assms, symmetric]
+      unfolding borel_measurable_lebesgue_preimage_borel borel_measurable_if [OF assms, symmetric]
       by blast
 qed
 
@@ -2508,9 +2508,9 @@
           apply (intro borel_measurable_abs borel_measurable_det_Jacobian [OF h_lmeas, where f=g])
           by (meson der_g IntD2 has_derivative_within_subset inf_le2)
         then have "(\<lambda>x. if x \<in> {t. h n (g t) = y} \<inter> S then ?D x else 0) \<in> borel_measurable lebesgue"
-          by (rule borel_measurable_If_I [OF _ h_lmeas])
+          by (rule borel_measurable_if_I [OF _ h_lmeas])
         then show "(\<lambda>x. if x \<in> {t. h n (g t) = y} then ?D x else 0) \<in> borel_measurable (lebesgue_on S)"
-          by (simp add: if_if_eq_conj Int_commute borel_measurable_UNIV [OF S, symmetric])
+          by (simp add: if_if_eq_conj Int_commute borel_measurable_if [OF S, symmetric])
         show "(\<lambda>x. ?D x *\<^sub>R f (g x) /\<^sub>R y) integrable_on S"
           by (rule integrable_cmul) (use det_int_fg in auto)
         show "norm (if x \<in> {t. h n (g t) = y} then ?D x else 0) \<le> ?D x *\<^sub>R f (g x) /\<^sub>R y"
@@ -2671,7 +2671,7 @@
       also have "\<dots> \<in> borel_measurable lebesgue"
         by (rule Df_borel)
       finally have *: "(\<lambda>x. \<bar>?D x\<bar> * f (g x)) \<in> borel_measurable (lebesgue_on S')"
-        by (simp add: borel_measurable_If_D)
+        by (simp add: borel_measurable_if_D)
       have "?h \<in> borel_measurable (lebesgue_on S')"
         by (intro * S' der_gS' borel_measurable_det_Jacobian measurable) (blast intro: der_gS')
       moreover have "?h x = f(g x)" if "x \<in> S'" for x
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -4476,7 +4476,7 @@
   hence "(zor_poly f z0 \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
     unfolding isCont_def .
   ultimately have "((\<lambda>w. f w * (w - z0) powr - n) \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
-    by (rule Lim_transform_eventually)
+    by (blast intro: Lim_transform_eventually)
   hence "((\<lambda>x. f (g x) * (g x - z0) powr - n) \<longlongrightarrow> zor_poly f z0 z0) F"
     by (rule filterlim_compose[OF _ g])
   from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
@@ -4505,7 +4505,7 @@
   hence "(zor_poly f z0 \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
     unfolding isCont_def .
   ultimately have "((\<lambda>w. f w / (w - z0) ^ nat n) \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
-    by (rule Lim_transform_eventually)
+    by (blast intro: Lim_transform_eventually)
   hence "((\<lambda>x. f (g x) / (g x - z0) ^ nat n) \<longlongrightarrow> zor_poly f z0 z0) F"
     by (rule filterlim_compose[OF _ g])
   from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
@@ -4537,7 +4537,7 @@
   hence "(zor_poly f z0 \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
     unfolding isCont_def .
   ultimately have "((\<lambda>w. f w * (w - z0) ^ nat (-n)) \<longlongrightarrow> zor_poly f z0 z0) (at z0)"
-    by (rule Lim_transform_eventually)
+    by (blast intro: Lim_transform_eventually)
   hence "((\<lambda>x. f (g x) * (g x - z0) ^ nat (-n)) \<longlongrightarrow> zor_poly f z0 z0) F"
     by (rule filterlim_compose[OF _ g])
   from tendsto_unique[OF \<open>F \<noteq> bot\<close> this lim] show ?thesis .
@@ -4577,7 +4577,7 @@
   moreover have "((\<lambda>w. ((f w - f z) / (w - z)) / ((g w - g z) / (w - z))) \<longlongrightarrow> f' / g') (at z)"
     by (intro tendsto_divide has_field_derivativeD assms)
   ultimately have "((\<lambda>w. f w / g w) \<longlongrightarrow> f' / g') (at z)"
-    by (rule Lim_transform_eventually)
+    by (blast intro: Lim_transform_eventually)
   with assms show ?thesis by simp
 qed
 
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -2373,11 +2373,11 @@
   qed
 
   ultimately have "((\<lambda>y. (exp ((y - t) *\<^sub>R A) - 1 - (y - t) *\<^sub>R A) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0) (at t within T)"
-    by (rule Lim_transform_eventually[rotated])
+    by (rule Lim_transform_eventually)
   from tendsto_mult_right_zero[OF this, where c="exp (t *\<^sub>R A)"]
   show "((\<lambda>y. (exp (y *\<^sub>R A) - exp (t *\<^sub>R A) - (y - t) *\<^sub>R (exp (t *\<^sub>R A) * A)) /\<^sub>R norm (y - t)) \<longlongrightarrow> 0)
       (at t within T)"
-    by (rule Lim_transform_eventually[rotated])
+    by (rule Lim_transform_eventually)
       (auto simp: algebra_simps divide_simps exp_add_commuting[symmetric])
 qed (rule bounded_linear_scaleR_left)
 
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -495,9 +495,9 @@
   done
 
 lemma Lim_transform_within_set_eq:
-  fixes a l :: "'a::real_normed_vector"
-  shows "eventually (\<lambda>x. x \<in> s \<longleftrightarrow> x \<in> t) (at a)
-         \<Longrightarrow> ((f \<longlongrightarrow> l) (at a within s) \<longleftrightarrow> (f \<longlongrightarrow> l) (at a within t))"
+  fixes a :: "'a::metric_space" and l :: "'b::metric_space"
+  shows "eventually (\<lambda>x. x \<in> S \<longleftrightarrow> x \<in> T) (at a)
+         \<Longrightarrow> ((f \<longlongrightarrow> l) (at a within S) \<longleftrightarrow> (f \<longlongrightarrow> l) (at a within T))"
   by (force intro: Lim_transform_within_set elim: eventually_mono)
 
 lemma Lim_null:
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -557,8 +557,8 @@
   shows "integral\<^sup>N lborel f = I"
 proof -
   from f_borel have "(\<lambda>x. ennreal (f x)) \<in> borel_measurable lborel" by auto
-  from borel_measurable_implies_simple_function_sequence'[OF this] 
-  obtain F where F: "\<And>i. simple_function lborel (F i)" "incseq F" 
+  from borel_measurable_implies_simple_function_sequence'[OF this]
+  obtain F where F: "\<And>i. simple_function lborel (F i)" "incseq F"
                  "\<And>i x. F i x < top" "\<And>x. (SUP i. F i x) = ennreal (f x)"
     by blast
   then have [measurable]: "\<And>i. F i \<in> borel_measurable lborel"
@@ -876,7 +876,7 @@
 lemma borel_integrable_atLeastAtMost':
   fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
   assumes f: "continuous_on {a..b} f"
-  shows "set_integrable lborel {a..b} f" 
+  shows "set_integrable lborel {a..b} f"
   unfolding set_integrable_def
   by (intro borel_integrable_compact compact_Icc f)
 
@@ -909,7 +909,7 @@
 proof -
   let ?f = "\<lambda>x. indicator S x *\<^sub>R f x"
   have "(?f has_integral LINT x : S | lborel. f x) UNIV"
-    using assms has_integral_integral_lborel 
+    using assms has_integral_integral_lborel
     unfolding set_integrable_def set_lebesgue_integral_def by blast
   hence 1: "(f has_integral (set_lebesgue_integral lborel S f)) S"
     apply (subst has_integral_restrict_UNIV [symmetric])
@@ -927,7 +927,7 @@
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes f: "set_integrable lebesgue S f"
   shows "(f has_integral (LINT x:S|lebesgue. f x)) S"
-  using has_integral_integral_lebesgue f 
+  using has_integral_integral_lebesgue f
   by (fastforce simp add: set_integrable_def set_lebesgue_integral_def indicator_def if_distrib[of "\<lambda>x. x *\<^sub>R f _"] cong: if_cong)
 
 lemma set_lebesgue_integral_eq_integral:
@@ -1031,7 +1031,7 @@
     then have "f absolutely_integrable_on S"
       using absolutely_integrable_restrict_UNIV by blast
   }
-  then show ?thesis        
+  then show ?thesis
     unfolding absolutely_integrable_on_def by auto
 qed
 
@@ -1043,7 +1043,7 @@
 proof (cases "c=0")
   case False
   then show ?thesis
-  unfolding absolutely_integrable_on_def 
+  unfolding absolutely_integrable_on_def
   by (simp add: norm_mult)
 qed auto
 
@@ -1087,6 +1087,27 @@
   shows "f absolutely_integrable_on T"
   using absolutely_integrable_spike_set_eq f neg by blast
 
+lemma absolutely_integrable_reflect[simp]:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "(\<lambda>x. f(-x)) absolutely_integrable_on cbox (-b) (-a) \<longleftrightarrow> f absolutely_integrable_on cbox a b"
+  apply (auto simp: absolutely_integrable_on_def dest: integrable_reflect [THEN iffD1])
+  unfolding integrable_on_def by auto
+
+lemma absolutely_integrable_reflect_real[simp]:
+  fixes f :: "real \<Rightarrow> 'b::euclidean_space"
+  shows "(\<lambda>x. f(-x)) absolutely_integrable_on {-b .. -a} \<longleftrightarrow> f absolutely_integrable_on {a..b::real}"
+  unfolding box_real[symmetric] by (rule absolutely_integrable_reflect)
+
+lemma absolutely_integrable_on_subcbox:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "\<lbrakk>f absolutely_integrable_on S; cbox a b \<subseteq> S\<rbrakk> \<Longrightarrow> f absolutely_integrable_on cbox a b"
+  by (meson absolutely_integrable_on_def integrable_on_subcbox)
+
+lemma absolutely_integrable_on_subinterval:
+  fixes f :: "real \<Rightarrow> 'b::euclidean_space"
+  shows "\<lbrakk>f absolutely_integrable_on S; {a..b} \<subseteq> S\<rbrakk> \<Longrightarrow> f absolutely_integrable_on {a..b}"
+  using absolutely_integrable_on_subcbox by fastforce
+
 lemma lmeasurable_iff_integrable_on: "S \<in> lmeasurable \<longleftrightarrow> (\<lambda>x. 1::real) integrable_on S"
   by (subst absolutely_integrable_on_iff_nonneg[symmetric])
      (simp_all add: lmeasurable_iff_integrable set_integrable_def)
@@ -1598,7 +1619,7 @@
     by blast
   have e22: "0 < e/2 / (2 * B * real DIM('M)) ^ DIM('N)"
     using \<open>0 < e\<close> \<open>0 < B\<close> by (simp add: divide_simps)
-  obtain T where "open T" "S \<subseteq> T" "(T - S) \<in> lmeasurable" 
+  obtain T where "open T" "S \<subseteq> T" "(T - S) \<in> lmeasurable"
                  "measure lebesgue (T - S) < e/2 / (2 * B * DIM('M)) ^ DIM('N)"
     using sets_lebesgue_outer_open [OF \<open>S \<in> sets lebesgue\<close> e22]
     by (metis emeasure_eq_measure2 ennreal_leI linorder_not_le)
@@ -1752,7 +1773,7 @@
         finally show "\<Union>\<D>' \<subseteq> T" .
         show "T \<in> lmeasurable"
           using \<open>S \<in> lmeasurable\<close> \<open>S \<subseteq> T\<close> \<open>T - S \<in> lmeasurable\<close> fmeasurable_Diff_D by blast
-      qed 
+      qed
       have "sum (measure lebesgue) \<D>' = sum content \<D>'"
         using  \<open>\<D>' \<subseteq> \<D>\<close> cbox by (force intro: sum.cong)
       then have "(2 * B * DIM('M)) ^ DIM('N) * sum (measure lebesgue) \<D>' =
@@ -2140,7 +2161,7 @@
   fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
   assumes f: "set_integrable M k f" shows "set_integrable M k (\<lambda>x. norm (f x))"
   using integrable_norm f by (force simp add: set_integrable_def)
- 
+
 lemma absolutely_integrable_bounded_variation:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes f: "f absolutely_integrable_on UNIV"
@@ -2208,7 +2229,7 @@
           using d' by force
         show "x \<notin> \<Union>{i \<in> d. x \<notin> i}"
           by auto
-      qed 
+      qed
       then show ?thesis
         by force
     qed
@@ -2216,13 +2237,13 @@
       by metis
     have "e/2 > 0"
       using e by auto
-    with Henstock_lemma[OF f] 
+    with Henstock_lemma[OF f]
     obtain \<gamma> where g: "gauge \<gamma>"
-      "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; \<gamma> fine p\<rbrakk> 
+      "\<And>p. \<lbrakk>p tagged_partial_division_of cbox a b; \<gamma> fine p\<rbrakk>
                 \<Longrightarrow> (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2"
-      by (metis (no_types, lifting))      
+      by (metis (no_types, lifting))
     let ?g = "\<lambda>x. \<gamma> x \<inter> ball x (k x)"
-    show ?thesis 
+    show ?thesis
     proof (intro exI conjI allI impI)
       show "gauge ?g"
         using g(1) k(1) by (auto simp: gauge_def)
@@ -2275,9 +2296,9 @@
           unfolding p'_def using d' by blast
         have "y \<in> \<Union>{K. \<exists>x. (x, K) \<in> p'}" if y: "y \<in> cbox a b" for y
         proof -
-          obtain x l where xl: "(x, l) \<in> p" "y \<in> l" 
+          obtain x l where xl: "(x, l) \<in> p" "y \<in> l"
             using y unfolding p'(6)[symmetric] by auto
-          obtain i where i: "i \<in> d" "y \<in> i" 
+          obtain i where i: "i \<in> d" "y \<in> i"
             using y unfolding d'(6)[symmetric] by auto
           have "x \<in> i"
             using fineD[OF p(3) xl(1)] using k(2) i xl by auto
@@ -2290,12 +2311,12 @@
             using * by auto
         next
           show "cbox a b \<subseteq> \<Union>{k. \<exists>x. (x, k) \<in> p'}"
-          proof 
+          proof
             fix y
             assume y: "y \<in> cbox a b"
-            obtain x L where xl: "(x, L) \<in> p" "y \<in> L" 
+            obtain x L where xl: "(x, L) \<in> p" "y \<in> L"
               using y unfolding p'(6)[symmetric] by auto
-            obtain I where i: "I \<in> d" "y \<in> I" 
+            obtain I where i: "I \<in> d" "y \<in> I"
               using y unfolding d'(6)[symmetric] by auto
             have "x \<in> I"
               using fineD[OF p(3) xl(1)] using k(2) i xl by auto
@@ -2323,7 +2344,7 @@
       moreover have "\<exists>y i l. (x, K) = (y, i \<inter> l) \<and> (y, l) \<in> p \<and> i \<in> d \<and> i \<inter> l \<noteq> {}"
         if xK: "(x,K) \<in> p'" for x K
       proof -
-        obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l" 
+        obtain i l where il: "x \<in> i" "i \<in> d" "(x, l) \<in> p" "K = i \<inter> l"
           using xK unfolding p'_def by auto
         then show ?thesis
           using p'(2) by fastforce
@@ -2378,7 +2399,7 @@
               show ?thesis
                 apply (rule sum.mono_neutral_left)
                   apply (simp add: snd_p(1))
-                unfolding d'_def uv using * by auto 
+                unfolding d'_def uv using * by auto
             qed
             also have "\<dots> = (\<Sum>l\<in>snd ` p. norm (integral (K \<inter> l) f))"
             proof -
@@ -2388,8 +2409,8 @@
                 have "interior (K \<inter> l) \<subseteq> interior (l \<inter> y)"
                   by (metis Int_lower2 interior_mono le_inf_iff that(4))
                 then have "interior (K \<inter> l) = {}"
-                  by (simp add: snd_p(5) that) 
-                moreover from d'(4)[OF k] snd_p(4)[OF that(1)] 
+                  by (simp add: snd_p(5) that)
+                moreover from d'(4)[OF k] snd_p(4)[OF that(1)]
                 obtain u1 v1 u2 v2
                   where uv: "K = cbox u1 u2" "l = cbox v1 v2" by metis
                 ultimately show ?thesis
@@ -2449,7 +2470,7 @@
               then show ?thesis by auto
             qed
             have 1: "\<exists>i l. snd (a, b) = i \<inter> l \<and> i \<in> d \<and> l \<in> snd ` p" if "(a, b) \<in> p'" for a b
-              using that 
+              using that
               apply (clarsimp simp: p'_def image_iff)
               by (metis (no_types, hide_lams) snd_conv)
             show ?thesis
@@ -2494,7 +2515,7 @@
                 by auto
               then show "\<bar>content (l1 \<inter> k1)\<bar> * norm (f x1) = 0"
                 unfolding uv Int_interval content_eq_0_interior[symmetric] by auto
-            qed 
+            qed
             then show ?thesis
               unfolding *
               apply (subst sum.reindex_nontrivial [OF fin_pd])
@@ -2551,7 +2572,7 @@
           finally show ?thesis .
         qed
       qed (rule d)
-    qed 
+    qed
   qed
   then show ?thesis
     using absolutely_integrable_onI [OF f has_integral_integrable] has_integral[of _ ?S]
@@ -2598,7 +2619,7 @@
     then obtain d K where ddiv: "d division_of \<Union>d" and "K = (\<Sum>k\<in>d. norm (integral k f))"
       "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e < K"
       by (auto simp add: image_iff not_le)
-    then have d: "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e 
+    then have d: "Sup (sum (\<lambda>k. norm (integral k f)) ` {d. d division_of \<Union> d}) - e
                   < (\<Sum>k\<in>d. norm (integral k f))"
       by auto
     note d'=division_ofD[OF ddiv]
@@ -2644,7 +2665,7 @@
            and d1: "\<And>p. \<lbrakk>p tagged_division_of (cbox a b); d1 fine p\<rbrakk> \<Longrightarrow>
             norm ((\<Sum>(x,k) \<in> p. content k *\<^sub>R norm (f x)) - integral (cbox a b) (\<lambda>x. norm (f x))) < e/2"
           unfolding has_integral_integral has_integral by meson
-        obtain d2 where "gauge d2" 
+        obtain d2 where "gauge d2"
           and d2: "\<And>p. \<lbrakk>p tagged_partial_division_of (cbox a b); d2 fine p\<rbrakk> \<Longrightarrow>
             (\<Sum>(x,k) \<in> p. norm (content k *\<^sub>R f x - integral k f)) < e/2"
           by (blast intro: Henstock_lemma [OF f(1) \<open>e/2>0\<close>])
@@ -3171,6 +3192,11 @@
   using absolutely_integrable_integrable_bound
   by (simp add: absolutely_integrable_on_def continuous_on_norm integrable_continuous)
 
+lemma absolutely_integrable_continuous_real:
+  fixes f :: "real \<Rightarrow> 'b::euclidean_space"
+  shows "continuous_on {a..b} f \<Longrightarrow> f absolutely_integrable_on {a..b}"
+  by (metis absolutely_integrable_continuous box_real(2))
+
 lemma continuous_imp_integrable:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "continuous_on (cbox a b) f"
@@ -3261,13 +3287,13 @@
                (\<lambda>x. norm(\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f) x)"
     by (simp add: sum.delta)
   have *: "(\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0) \<circ>
-           (\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f 
-           absolutely_integrable_on S" 
+           (\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
+           absolutely_integrable_on S"
         if "i \<in> Basis" for i
   proof -
     have "bounded_linear (\<lambda>y. \<Sum>j\<in>Basis. if j = i then y *\<^sub>R j else 0)"
       by (simp add: linear_linear algebra_simps linearI)
-    moreover have "(\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f 
+    moreover have "(\<lambda>x. norm (\<Sum>j\<in>Basis. if j = i then (x \<bullet> i) *\<^sub>R j else 0)) \<circ> f
                    absolutely_integrable_on S"
       unfolding o_def
       apply (rule absolutely_integrable_norm [unfolded o_def])
@@ -3290,14 +3316,14 @@
   shows "f absolutely_integrable_on A"
   by (rule absolutely_integrable_integrable_bound [OF _ assms]) auto
 
-  
+
 lemma abs_absolutely_integrableI:
   assumes f: "f integrable_on S" and fcomp: "(\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) integrable_on S"
   shows "f absolutely_integrable_on S"
 proof -
   have "(\<lambda>x. (f x \<bullet> i) *\<^sub>R i) absolutely_integrable_on S" if "i \<in> Basis" for i
   proof -
-    have "(\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on S" 
+    have "(\<lambda>x. \<bar>f x \<bullet> i\<bar>) integrable_on S"
       using assms integrable_component [OF fcomp, where y=i] that by simp
     then have "(\<lambda>x. f x \<bullet> i) absolutely_integrable_on S"
       using abs_absolutely_integrableI_1 f integrable_component by blast
@@ -3310,7 +3336,7 @@
     by (simp add: euclidean_representation)
 qed
 
-    
+
 lemma absolutely_integrable_abs_iff:
    "f absolutely_integrable_on S \<longleftrightarrow>
     f integrable_on S \<and> (\<lambda>x. \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i) integrable_on S"
@@ -3319,7 +3345,7 @@
   assume ?lhs then show ?rhs
     using absolutely_integrable_abs absolutely_integrable_on_def by blast
 next
-  assume ?rhs 
+  assume ?rhs
   moreover
   have "(\<lambda>x. if x \<in> S then \<Sum>i\<in>Basis. \<bar>f x \<bullet> i\<bar> *\<^sub>R i else 0) = (\<lambda>x. \<Sum>i\<in>Basis. \<bar>(if x \<in> S then f x else 0) \<bullet> i\<bar> *\<^sub>R i)"
     by force
@@ -3333,7 +3359,7 @@
    shows "(\<lambda>x. \<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)
             absolutely_integrable_on S"
 proof -
-  have "(\<lambda>x. \<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) = 
+  have "(\<lambda>x. \<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
         (\<lambda>x. (1/2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))"
   proof (rule ext)
     fix x
@@ -3347,7 +3373,7 @@
     show "(\<Sum>i\<in>Basis. max (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
          (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))" .
   qed
-  moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))) 
+  moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x + (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
                  absolutely_integrable_on S"
     apply (intro absolutely_integrable_add absolutely_integrable_scaleR_left assms)
     using absolutely_integrable_abs [OF absolutely_integrable_diff [OF assms]]
@@ -3355,7 +3381,7 @@
     done
   ultimately show ?thesis by metis
 qed
-  
+
 corollary absolutely_integrable_max_1:
   fixes f :: "'n::euclidean_space \<Rightarrow> real"
   assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
@@ -3368,7 +3394,7 @@
    shows "(\<lambda>x. \<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i)
             absolutely_integrable_on S"
 proof -
-  have "(\<lambda>x. \<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) = 
+  have "(\<lambda>x. \<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
         (\<lambda>x. (1/2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))"
   proof (rule ext)
     fix x
@@ -3382,7 +3408,7 @@
     show "(\<Sum>i\<in>Basis. min (f x \<bullet> i) (g x \<bullet> i) *\<^sub>R i) =
          (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))" .
   qed
-  moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i))) 
+  moreover have "(\<lambda>x. (1 / 2) *\<^sub>R (f x + g x - (\<Sum>i\<in>Basis. \<bar>f x \<bullet> i - g x \<bullet> i\<bar> *\<^sub>R i)))
                  absolutely_integrable_on S"
     apply (intro absolutely_integrable_add absolutely_integrable_diff absolutely_integrable_scaleR_left assms)
     using absolutely_integrable_abs [OF absolutely_integrable_diff [OF assms]]
@@ -3390,7 +3416,7 @@
     done
   ultimately show ?thesis by metis
 qed
-  
+
 corollary absolutely_integrable_min_1:
   fixes f :: "'n::euclidean_space \<Rightarrow> real"
   assumes "f absolutely_integrable_on S" "g absolutely_integrable_on S"
@@ -3404,7 +3430,7 @@
 proof -
   have "(\<lambda>x. (f x \<bullet> i) *\<^sub>R i) absolutely_integrable_on A" if "i \<in> Basis" for i
   proof -
-    have "(\<lambda>x. f x \<bullet> i) integrable_on A" 
+    have "(\<lambda>x. f x \<bullet> i) integrable_on A"
       by (simp add: assms(1) integrable_component)
     then have "(\<lambda>x. f x \<bullet> i) absolutely_integrable_on A"
       by (metis that comp nonnegative_absolutely_integrable_1)
@@ -3416,7 +3442,7 @@
   then show ?thesis
     by (simp add: euclidean_representation)
 qed
-  
+
 lemma absolutely_integrable_component_ubound:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: euclidean_space"
   assumes f: "f integrable_on A" and g: "g absolutely_integrable_on A"
@@ -3511,7 +3537,7 @@
       using int [OF B'] by (auto simp: image_iff o_def cong: if_cong dest!: has_integral_vec1_I_cbox)
   qed
   show ?thesis
-    using assms 
+    using assms
     apply (subst has_integral_alt)
     apply (subst (asm) has_integral_alt)
     apply (simp add: has_integral_vec1_I_cbox split: if_split_asm)
@@ -3632,7 +3658,7 @@
     "AE x in lebesgue. norm (indicator S x *\<^sub>R f k x) \<le> indicator S x *\<^sub>R h x" for k
     using conv le by (auto intro!: always_eventually split: split_indicator)
   have g: "g absolutely_integrable_on S"
-    using 1 2 3 4 unfolding set_borel_measurable_def set_integrable_def    
+    using 1 2 3 4 unfolding set_borel_measurable_def set_integrable_def
     by (rule integrable_dominated_convergence)
   then show "g integrable_on S"
     by (auto simp: absolutely_integrable_on_def)
@@ -3712,7 +3738,7 @@
   assume fb [rule_format]: "\<And>k. \<forall>b\<in>Basis. (\<lambda>x. f k x \<bullet> b) absolutely_integrable_on S" and b: "b \<in> Basis"
   show "(\<lambda>x. g x \<bullet> b) integrable_on S"
   proof (rule dominated_convergence_integrable_1 [OF fb h])
-    fix x 
+    fix x
     assume "x \<in> S"
     show "norm (g x \<bullet> b) \<le> h x"
       using norm_nth_le \<open>x \<in> S\<close> b normg order.trans by blast
@@ -3773,7 +3799,7 @@
 
 \<close>
 
-lemma                                                                                          
+lemma
   fixes f :: "real \<Rightarrow> real"
   assumes [measurable]: "f \<in> borel_measurable borel"
   assumes f: "\<And>x. x \<in> {a..b} \<Longrightarrow> DERIV F x :> f x" "\<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x" and "a \<le> b"
@@ -4400,7 +4426,7 @@
   shows "{x. f x \<in> T} \<in> sets lebesgue"
   using assms borel_measurable_vimage_borel [of f UNIV] by auto
 
-lemma borel_measurable_If_I:
+lemma borel_measurable_if_I:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes f: "f \<in> borel_measurable (lebesgue_on S)" and S: "S \<in> sets lebesgue"
   shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
@@ -4416,7 +4442,7 @@
   done
 qed
 
-lemma borel_measurable_If_D:
+lemma borel_measurable_if_D:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
   shows "f \<in> borel_measurable (lebesgue_on S)"
@@ -4426,11 +4452,11 @@
   apply (force simp: space_restrict_space sets_restrict_space image_iff intro: rev_bexI)
   done
 
-lemma borel_measurable_UNIV:
+lemma borel_measurable_if:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "S \<in> sets lebesgue"
   shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S)"
-  using assms borel_measurable_If_D borel_measurable_If_I by blast
+  using assms borel_measurable_if_D borel_measurable_if_I by blast
 
 lemma borel_measurable_lebesgue_preimage_borel:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
@@ -4514,7 +4540,7 @@
   show "(\<lambda>x. if x \<in> S then f x else 0) integrable_on cbox a b" for a b
   proof (rule measurable_bounded_lemma)
     show "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
-      by (simp add: S borel_measurable_UNIV f)
+      by (simp add: S borel_measurable_if f)
     show "(\<lambda>x. if x \<in> S then g x else 0) integrable_on cbox a b"
       by (simp add: g integrable_altD(1))
     show "norm (if x \<in> S then f x else 0) \<le> (if x \<in> S then g x else 0)" for x
@@ -4556,7 +4582,7 @@
   have "(UNIV::'a set) \<in> sets lborel"
     by simp
   then show ?thesis
-    using assms borel_measurable_If_D borel_measurable_UNIV_eq integrable_imp_measurable_weak integrable_restrict_UNIV by blast
+    using assms borel_measurable_if_D borel_measurable_UNIV_eq integrable_imp_measurable_weak integrable_restrict_UNIV by blast
 qed
 
 lemma integrable_iff_integrable_on:
@@ -4599,6 +4625,12 @@
   apply (simp add: integrable_on_lebesgue_on measurable_bounded_by_integrable_imp_lebesgue_integrable)
   using abs_absolutely_integrableI_1 absolutely_integrable_measurable measurable_bounded_by_integrable_imp_integrable_real by blast
 
+lemma absolutely_integrable_imp_borel_measurable:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "f absolutely_integrable_on S" "S \<in> sets lebesgue"
+  shows "f \<in> borel_measurable (lebesgue_on S)"
+  using absolutely_integrable_measurable assms by blast
+
 lemma measurable_bounded_by_integrable_imp_absolutely_integrable:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   assumes "f \<in> borel_measurable (lebesgue_on S)" "S \<in> sets lebesgue"
@@ -4772,7 +4804,7 @@
     fix e :: real assume e: "e > 0"
     have sets [intro]: "A \<in> sets M" if "A \<in> sets borel" for A
       using that assms by blast
-  
+
     have "((\<lambda>b. LINT y:{a..b}|M. g y) \<longlongrightarrow> (LINT y:{a..}|M. g y)) at_top"
       by (intro tendsto_set_lebesgue_integral_at_top assms sets) auto
     with e obtain b0 :: real where b0: "\<forall>b\<ge>b0. \<bar>(LINT y:{a..}|M. g y) - (LINT y:{a..b}|M. g y)\<bar> < e"
@@ -4792,7 +4824,7 @@
 
     have "eventually (\<lambda>b. b \<ge> b0) at_top" by (rule eventually_ge_at_top)
     moreover have "eventually (\<lambda>b. b \<ge> a) at_top" by (rule eventually_ge_at_top)
-    ultimately show "eventually (\<lambda>b. \<forall>x\<in>A. 
+    ultimately show "eventually (\<lambda>b. \<forall>x\<in>A.
                        dist (LINT y:{a..b}|M. f x y) (LINT y:{a..}|M. f x y) < e) at_top"
     proof eventually_elim
       case (elim b)
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -727,7 +727,7 @@
     then have "ereal(1/v n) = 1/u n" using H(2) by simp
   }
   ultimately have "eventually (\<lambda>n. ereal(1/v n) = 1/u n) F" using ureal eventually_elim2 by force
-  with Lim_transform_eventually[OF this lim] show ?thesis by simp
+  with Lim_transform_eventually[OF lim this] show ?thesis by simp
 next
   case (PInf)
   then have "1/l = 0" by auto
@@ -744,7 +744,7 @@
   have "(v \<longlongrightarrow> \<infinity>) F" unfolding v_def using MInf assms(1) tendsto_uminus_ereal by fastforce
   then have "((\<lambda>n. 1/v n) \<longlongrightarrow> 0) F" using tendsto_inverse_ereal_PInf by auto
   then have "((\<lambda>n. -1/v n) \<longlongrightarrow> 0) F" using tendsto_uminus_ereal by fastforce
-  then show ?thesis unfolding v_def using Lim_transform_eventually[OF *] \<open> 1/l = 0 \<close> by auto
+  then show ?thesis unfolding v_def using Lim_transform_eventually[OF _ *] \<open> 1/l = 0 \<close> by auto
 qed
 
 lemma tendsto_divide_ereal [tendsto_intros]:
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Further_Topology.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -4020,7 +4020,7 @@
       apply (auto simp: exp_eq dist_norm norm_mult)
       done
     then have "((\<lambda>y. (g y - g z) / (y - z)) \<longlongrightarrow> f' / exp (g z)) (at z within S)"
-      by (auto intro!: Lim_transform_eventually [OF _ tendsto_divide [OF ee dd]])
+      by (auto intro!: Lim_transform_eventually [OF tendsto_divide [OF ee dd]])
     then show ?thesis
       by (auto simp: field_differentiable_def has_field_derivative_iff)
   qed
@@ -4068,7 +4068,7 @@
       apply (auto simp: exp_eq dist_norm norm_mult)
       done
     then have "((\<lambda>y. (g y - g z) / (y - z)) \<longlongrightarrow> f' / exp (g z)) (at z within S)"
-      by (auto intro!: Lim_transform_eventually [OF _ tendsto_divide [OF ee dd]])
+      by (auto intro!: Lim_transform_eventually [OF tendsto_divide [OF ee dd]])
     then show ?thesis
       by (auto simp: field_differentiable_def has_field_derivative_iff)
   qed
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -715,7 +715,7 @@
     by (intro tendsto_intros LIMSEQ_n_over_Suc_n) simp_all
   hence "(\<lambda>n. of_real (ln (real n / (real n + 1)))) \<longlonglongrightarrow> (0 :: 'a)" by (simp add: add_ac)
   hence lim: "(\<lambda>n. of_real (ln (real n)) - of_real (ln (real n + 1))) \<longlonglongrightarrow> (0::'a)"
-  proof (rule Lim_transform_eventually [rotated])
+  proof (rule Lim_transform_eventually)
     show "eventually (\<lambda>n. of_real (ln (real n / (real n + 1))) =
             of_real (ln (real n)) - (of_real (ln (real n + 1)) :: 'a)) at_top"
       using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp add: ln_div)
@@ -1118,7 +1118,7 @@
     by (intro tendsto_intros lim_inverse_n)
   hence "(\<lambda>n. ?f n * rGamma_series z n) \<longlonglongrightarrow> rGamma z" by simp
   ultimately have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> rGamma z"
-    by (rule Lim_transform_eventually)
+    by (blast intro: Lim_transform_eventually)
   moreover have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> z * rGamma (z + 1)"
     by (intro tendsto_intros)
   ultimately show "z * rGamma (z + 1) = rGamma z" using LIMSEQ_unique by blast
@@ -1324,7 +1324,7 @@
        (simp_all add: convergent_LIMSEQ_iff rGamma_complex_def)
   hence "(\<lambda>n. ?f n * rGamma_series z n) \<longlonglongrightarrow> rGamma z" by simp
   ultimately have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> rGamma z"
-    by (rule Lim_transform_eventually)
+    by (blast intro: Lim_transform_eventually)
   moreover have "(\<lambda>n. z * rGamma_series (z + 1) n) \<longlonglongrightarrow> z * rGamma (z + 1)"
     using rGamma_series_complex_converges
     by (auto intro!: tendsto_mult simp: rGamma_complex_def convergent_LIMSEQ_iff)
@@ -2054,7 +2054,7 @@
       by (intro tendsto_intros Gamma_series'_LIMSEQ)
          (simp_all add: o_def strict_mono_def Gamma_eq_zero_iff)
     ultimately have "?h \<longlonglongrightarrow> ?powr 2 (2*z) * Gamma z * Gamma (z+1/2) / Gamma (2*z)"
-      by (rule Lim_transform_eventually)
+      by (blast intro: Lim_transform_eventually)
   } note lim = this
 
   from assms double_in_nonpos_Ints_imp[of z] have z': "2 * z \<notin> \<int>\<^sub>\<le>\<^sub>0" by auto
@@ -2504,7 +2504,7 @@
                      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)
+  ultimately show "?r \<longlonglongrightarrow> 1" by (force intro: Lim_transform_eventually)
 
   from eventually_gt_at_top[of "0::nat"]
     show "eventually (\<lambda>n. ?r n = Gamma_series_euler' z n / Gamma_series z n) sequentially"
@@ -2901,8 +2901,7 @@
     by eventually_elim (simp add: powr_def algebra_simps Ln_of_nat Gamma_series_def)
   from this and Gamma_series_LIMSEQ[of z]
     have C: "(\<lambda>k. of_nat k powr z * fact k / pochhammer z (k+1)) \<longlonglongrightarrow> Gamma z"
-    by (rule Lim_transform_eventually)
-
+    by (blast intro: Lim_transform_eventually)
   {
     fix x :: real assume x: "x \<ge> 0"
     have lim_exp: "(\<lambda>k. (1 - x / real k) ^ k) \<longlonglongrightarrow> exp (-x)"
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Harmonic_Numbers.thy
--- a/src/HOL/Analysis/Harmonic_Numbers.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -218,7 +218,7 @@
               filterlim_subseq) (auto simp: strict_mono_def)
   hence "(\<lambda>n. ?em (2*n) - ?em n + ln (2::real)) \<longlonglongrightarrow> ln 2" by simp
   ultimately have "(\<lambda>n. (\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k))) \<longlonglongrightarrow> ln 2"
-    by (rule Lim_transform_eventually)
+    by (blast intro: Lim_transform_eventually)
 
   moreover have "summable (\<lambda>k. (-1)^k * inverse (real_of_nat (Suc k)))"
     using LIMSEQ_inverse_real_of_nat
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -3522,12 +3522,17 @@
     and "\<forall>k\<in>Basis. m k \<noteq> 0"
   shows "((\<lambda>x. f (\<Sum>k\<in>Basis. (m k * (x\<bullet>k))*\<^sub>R k)) has_integral
          ((1/ \<bar>prod m Basis\<bar>) *\<^sub>R i)) ((\<lambda>x. (\<Sum>k\<in>Basis. (1 / m k * (x\<bullet>k))*\<^sub>R k)) ` cbox a b)"
-apply (rule has_integral_twiddle[where f=f])
-unfolding zero_less_abs_iff content_image_stretch_interval
-unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
-using assms
-by auto
-
+  apply (rule has_integral_twiddle[where f=f])
+  unfolding zero_less_abs_iff content_image_stretch_interval
+  unfolding image_stretch_interval empty_as_interval euclidean_eq_iff[where 'a='a]
+  using assms
+  by auto
+
+lemma has_integral_stretch_real:
+  fixes f :: "real \<Rightarrow> 'b::real_normed_vector"
+  assumes "(f has_integral i) {a..b}" and "m \<noteq> 0"
+  shows "((\<lambda>x. f (m * x)) has_integral (1 / \<bar>m\<bar>) *\<^sub>R i) ((\<lambda>x. x / m) ` {a..b})"
+  using has_integral_stretch [of f i a b "\<lambda>b. m"] assms by simp
 
 lemma integrable_stretch:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
@@ -3605,6 +3610,11 @@
   "((\<lambda>x. f (-x)) has_integral i) (cbox (-b) (-a)) \<longleftrightarrow> (f has_integral i) (cbox a b)"
   by (auto dest: has_integral_reflect_lemma)
 
+lemma has_integral_reflect_real[simp]:
+  fixes a b::real
+  shows "((\<lambda>x. f (-x)) has_integral i) {-b..-a} \<longleftrightarrow> (f has_integral i) {a..b}"
+  by (metis has_integral_reflect interval_cbox)
+
 lemma integrable_reflect[simp]: "(\<lambda>x. f(-x)) integrable_on cbox (-b) (-a) \<longleftrightarrow> f integrable_on cbox a b"
   unfolding integrable_on_def by auto
 
@@ -3619,7 +3629,6 @@
   unfolding box_real[symmetric]
   by (rule integral_reflect)
 
-
 subsection \<open>Stronger form of FCT; quite a tedious proof\<close>
 
 lemma split_minus[simp]: "(\<lambda>(x, k). f x k) x - (\<lambda>(x, k). g x k) x = (\<lambda>(x, k). f x k - g x k) x"
@@ -7286,19 +7295,19 @@
     thus "bounded (range(\<lambda>k. integral {c..} (f k)))"
       by (intro boundedI[of _ "exp (-a*c)/a"]) auto
   qed (auto simp: f_def)
-
+  have "(\<lambda>k. exp (-a*c)/a - exp (-a * of_nat k)/a) \<longlonglongrightarrow> exp (-a*c)/a - 0/a"
+    by (intro tendsto_intros filterlim_compose[OF exp_at_bot]
+        filterlim_tendsto_neg_mult_at_bot[OF tendsto_const] filterlim_real_sequentially)+
+      (insert a, simp_all)
+  moreover
   from eventually_gt_at_top[of "nat \<lceil>c\<rceil>"] have "eventually (\<lambda>k. of_nat k > c) sequentially"
     by eventually_elim linarith
   hence "eventually (\<lambda>k. exp (-a*c)/a - exp (-a * of_nat k)/a = integral {c..} (f k)) sequentially"
-    by eventually_elim (simp add: integral_f)
-  moreover have "(\<lambda>k. exp (-a*c)/a - exp (-a * of_nat k)/a) \<longlonglongrightarrow> exp (-a*c)/a - 0/a"
-    by (intro tendsto_intros filterlim_compose[OF exp_at_bot]
-          filterlim_tendsto_neg_mult_at_bot[OF tendsto_const] filterlim_real_sequentially)+
-       (insert a, simp_all)
+    by eventually_elim (simp add: integral_f) 
   ultimately have "(\<lambda>k. integral {c..} (f k)) \<longlonglongrightarrow> exp (-a*c)/a - 0/a"
     by (rule Lim_transform_eventually)
   from LIMSEQ_unique[OF conjunct2[OF A] this]
-    have "integral {c..} (\<lambda>x. exp (-a*x)) = exp (-a*c)/a" by simp
+  have "integral {c..} (\<lambda>x. exp (-a*x)) = exp (-a*c)/a" by simp
   with conjunct1[OF A] show ?thesis
     by (simp add: has_integral_integral)
 qed
@@ -7363,7 +7372,7 @@
         have "eventually (\<lambda>k. x powr a = f k x) sequentially"
         by eventually_elim (insert x, simp add: f_def)
       moreover have "(\<lambda>_. x powr a) \<longlonglongrightarrow> x powr a" by simp
-      ultimately show ?thesis by (rule Lim_transform_eventually)
+      ultimately show ?thesis by (blast intro: Lim_transform_eventually)
     qed (simp_all add: f_def)
   next
     {
@@ -7390,7 +7399,7 @@
   hence "(\<lambda>k. c powr (a + 1) / (a + 1) - inverse (real (Suc k)) powr (a + 1) / (a + 1))
           \<longlonglongrightarrow> c powr (a + 1) / (a + 1)" by simp
   ultimately have "(\<lambda>k. integral {0..c} (f k)) \<longlonglongrightarrow> c powr (a+1) / (a+1)"
-    by (rule Lim_transform_eventually)
+    by (blast intro: Lim_transform_eventually)
   with A have "integral {0..c} (\<lambda>x. x powr a) = c powr (a+1) / (a+1)"
     by (blast intro: LIMSEQ_unique)
   with A show ?thesis by (simp add: has_integral_integral)
@@ -7474,7 +7483,7 @@
     by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr]
           filterlim_ident filterlim_real_sequentially | simp)+)
   hence "(\<lambda>n. F n - F a) \<longlonglongrightarrow> -F a" by simp
-  ultimately have "(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> -F a" by (rule Lim_transform_eventually)
+  ultimately have "(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> -F a" by (blast intro: Lim_transform_eventually)
   from conjunct2[OF *] and this
     have "integral {a..} (\<lambda>x. x powr e) = -F a" by (rule LIMSEQ_unique)
   with conjunct1[OF *] show ?thesis
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -417,10 +417,43 @@
   shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M"
   by (metis (mono_tags, lifting) IntD1 assms measurable_cong_simp space_restrict_space)
 
+lemma lebesgue_on_UNIV_eq: "lebesgue_on UNIV = lebesgue"
+proof -
+  have "measure_of UNIV (sets lebesgue) (emeasure lebesgue) = lebesgue"
+    by (metis measure_of_of_measure space_borel space_completion space_lborel)
+  then show ?thesis
+    by (auto simp: restrict_space_def)
+qed
+
 lemma integrable_lebesgue_on_UNIV_eq:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}"
   shows "integrable (lebesgue_on UNIV) f = integrable lebesgue f"
   by (auto simp: integrable_restrict_space)
+lemma integral_restrict_Int:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "S \<in> sets lebesgue" "T \<in> sets lebesgue"
+  shows "integral\<^sup>L (lebesgue_on T) (\<lambda>x. if x \<in> S then f x else 0) = integral\<^sup>L (lebesgue_on (S \<inter> T)) f"
+proof -
+  have "(\<lambda>x. indicat_real T x *\<^sub>R (if x \<in> S then f x else 0)) = (\<lambda>x. indicat_real (S \<inter> T) x *\<^sub>R f x)"
+    by (force simp: indicator_def)
+  then show ?thesis
+    by (simp add: assms sets.Int Bochner_Integration.integral_restrict_space)
+qed
+
+lemma integral_restrict:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "S \<subseteq> T" "S \<in> sets lebesgue" "T \<in> sets lebesgue"
+  shows "integral\<^sup>L (lebesgue_on T) (\<lambda>x. if x \<in> S then f x else 0) = integral\<^sup>L (lebesgue_on S) f"
+  using integral_restrict_Int [of S T f] assms
+  by (simp add: Int_absorb2)
+
+lemma integral_restrict_UNIV:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "S \<in> sets lebesgue"
+  shows "integral\<^sup>L lebesgue (\<lambda>x. if x \<in> S then f x else 0) = integral\<^sup>L (lebesgue_on S) f"
+  using integral_restrict_Int [of S UNIV f] assms
+  by (simp add: lebesgue_on_UNIV_eq)
+
 
 text\<^marker>\<open>tag unimportant\<close> \<open>Measurability of continuous functions\<close>
 
@@ -1027,6 +1060,12 @@
   and lmeasurable_box [iff]: "box a b \<in> lmeasurable"
   by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq)
 
+lemma
+  fixes a::real
+  shows lmeasurable_interval [iff]: "{a..b} \<in> lmeasurable" "{a<..<b} \<in> lmeasurable"
+  apply (metis box_real(2) lmeasurable_cbox)
+  by (metis box_real(1) lmeasurable_box)
+
 lemma fmeasurable_compact: "compact S \<Longrightarrow> S \<in> fmeasurable lborel"
   using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact)
 
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -2335,7 +2335,7 @@
       then have eq: "(\<Union>i. F i) = F i"
         by auto
       with i show ?thesis
-        by (auto intro!: Lim_transform_eventually[OF _ tendsto_const] eventually_sequentiallyI[where c=i])
+        by (auto intro!: Lim_transform_eventually[OF tendsto_const] eventually_sequentiallyI[where c=i])
     next
       assume "\<not> (\<exists>i. \<forall>j\<ge>i. F i = F j)"
       then obtain f where f: "\<And>i. i \<le> f i" "\<And>i. F i \<noteq> F (f i)" by metis
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -3993,7 +3993,7 @@
     by (auto intro!: tendsto_inverse)
   from real \<open>0 < x\<close> show ?thesis
     by (auto simp: at_ereal tendsto_compose_filtermap[symmetric] eventually_at_filter
-             intro!: Lim_transform_eventually[OF _ **] t1_space_nhds)
+             intro!: Lim_transform_eventually[OF **] t1_space_nhds)
 qed (insert \<open>0 < x\<close>, auto intro!: inverse_infty_ereal_tendsto_0)
 
 lemma inverse_ereal_tendsto_at_right_0: "(inverse \<longlongrightarrow> \<infinity>) (at_right (0::ereal))"
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Library/Landau_Symbols.thy
--- a/src/HOL/Library/Landau_Symbols.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -1676,7 +1676,7 @@
     by (intro always_eventually) simp
   moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp
   ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"
-    by (rule Lim_transform_eventually)
+    by (simp add: Landau_Symbols.tendsto_eventually)
 qed
 
 lemma asymp_equiv_symI: 
@@ -1702,7 +1702,7 @@
   qed
   hence "eventually (\<lambda>x. f x / g x = (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) F"
     by eventually_elim simp
-  from this and assms show "f \<sim>[F] g" unfolding asymp_equiv_def 
+  with assms show "f \<sim>[F] g" unfolding asymp_equiv_def 
     by (rule Lim_transform_eventually)
 qed (simp_all add: asymp_equiv_def)
 
@@ -1748,10 +1748,10 @@
   shows   "f \<sim>[F] h"
 proof -
   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
-  from assms[THEN asymp_equiv_eventually_zeros]
-    have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp
-  moreover from tendsto_mult[OF assms[THEN asymp_equivD]] 
-    have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp
+  from tendsto_mult[OF assms[THEN asymp_equivD]] 
+  have "((\<lambda>x. ?T f g x * ?T g h x) \<longlongrightarrow> 1) F" by simp
+  moreover from assms[THEN asymp_equiv_eventually_zeros]
+  have "eventually (\<lambda>x. ?T f g x * ?T g h x = ?T f h x) F" by eventually_elim simp
   ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
 qed
 
@@ -1845,13 +1845,15 @@
   shows   "(g \<longlongrightarrow> c) F"
 proof -
   let ?h = "\<lambda>x. (if g x = 0 \<and> f x = 0 then 1 else g x / f x) * f x"
-  have "eventually (\<lambda>x. ?h x = g x) F"
-    using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp
-  moreover from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)
+  from assms(1) have "g \<sim>[F] f" by (rule asymp_equiv_symI)
   hence "filterlim (\<lambda>x. if g x = 0 \<and> f x = 0 then 1 else g x / f x) (nhds 1) F"
     by (rule asymp_equivD)
   from tendsto_mult[OF this assms(2)] have "(?h \<longlongrightarrow> c) F" by simp
-  ultimately show ?thesis by (rule Lim_transform_eventually)
+  moreover 
+  have "eventually (\<lambda>x. ?h x = g x) F"
+    using asymp_equiv_eventually_zeros[OF assms(1)] by eventually_elim simp
+  ultimately show ?thesis
+    by (rule Lim_transform_eventually)
 qed
 
 lemma tendsto_asymp_equiv_cong:
@@ -1861,10 +1863,11 @@
   {
     fix f g :: "'a \<Rightarrow> 'b"
     assume *: "f \<sim>[F] g" "(g \<longlongrightarrow> c) F"
+    have "((\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> c * 1) F"
+      by (intro tendsto_intros asymp_equivD *)
+    moreover 
     have "eventually (\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x) = f x) F"
       using asymp_equiv_eventually_zeros[OF *(1)] by eventually_elim simp
-    moreover have "((\<lambda>x. g x * (if f x = 0 \<and> g x = 0 then 1 else f x / g x)) \<longlongrightarrow> c * 1) F"
-      by (intro tendsto_intros asymp_equivD *)
     ultimately have "(f \<longlongrightarrow> c * 1) F"
       by (rule Lim_transform_eventually)
   }
@@ -1968,11 +1971,11 @@
   from assms have "((\<lambda>x. ?T f1 g1 x * ?T f2 g2 x) \<longlongrightarrow> 1 * 1) F"
     by (intro tendsto_mult asymp_equivD)
   moreover {
-    have "eventually (\<lambda>x. ?S x = ?S' x) F"
-      using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto
-    moreover have "(?S \<longlongrightarrow> 0) F"
+    have "(?S \<longlongrightarrow> 0) F"
       by (intro filterlim_If assms[THEN A, THEN tendsto_mono[rotated]])
          (auto intro: le_infI1 le_infI2)
+    moreover have "eventually (\<lambda>x. ?S x = ?S' x) F"
+      using assms[THEN asymp_equiv_eventually_zeros] by eventually_elim auto
     ultimately have "(?S' \<longlongrightarrow> 0) F" by (rule Lim_transform_eventually)
   }
   ultimately have "(?T (\<lambda>x. f1 x * f2 x) (\<lambda>x. g1 x * g2 x) \<longlongrightarrow> 1 * 1) F"
@@ -2037,12 +2040,12 @@
   shows   "(\<lambda>x. f x powr y) \<sim>[F] (\<lambda>x. g x powr y)"
 proof -
   let ?T = "\<lambda>f g x. if f x = 0 \<and> g x = 0 then 1 else f x / g x"
-  have "eventually (\<lambda>x. ?T f g x powr y = ?T (\<lambda>x. f x powr y) (\<lambda>x. g x powr y) x) F"
+  have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"
+    by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all
+  hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp
+  moreover have "eventually (\<lambda>x. ?T f g x powr y = ?T (\<lambda>x. f x powr y) (\<lambda>x. g x powr y) x) F"
     using asymp_equiv_eventually_zeros[OF assms(1)] assms(2,3)
     by eventually_elim (auto simp: powr_divide)
-  moreover have "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1 powr y) F"
-    by (intro tendsto_intros asymp_equivD[OF assms(1)]) simp_all
-  hence "((\<lambda>x. ?T f g x powr y) \<longlongrightarrow> 1) F" by simp
   ultimately show ?thesis unfolding asymp_equiv_def by (rule Lim_transform_eventually)
 qed
 
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Limits.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -1981,7 +1981,7 @@
   using Lim_transform Lim_transform2 by blast
 
 lemma Lim_transform_eventually:
-  "eventually (\<lambda>x. f x = g x) net \<Longrightarrow> (f \<longlongrightarrow> l) net \<Longrightarrow> (g \<longlongrightarrow> l) net"
+  "\<lbrakk>(f \<longlongrightarrow> l) F; eventually (\<lambda>x. f x = g x) F\<rbrakk> \<Longrightarrow> (g \<longlongrightarrow> l) F"
   using eventually_elim2 by (fastforce simp add: tendsto_def)
 
 lemma Lim_transform_within:
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -856,7 +856,7 @@
         have "integrable (map_pmf (to_nat_on M) M) (\<lambda>n. B)"
           by auto
         then show "summable (\<lambda>n. pmf (map_pmf (to_nat_on (set_pmf M)) M) n * B)"
-          by (simp add: measure_pmf_eq_density integrable_density integrable_count_space_nat_iff summable_rabs_cancel)
+          by (fastforce simp add: measure_pmf_eq_density integrable_density integrable_count_space_nat_iff summable_mult2)
       qed
     qed simp
   qed simp
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Probability/Sinc_Integral.thy
--- a/src/HOL/Probability/Sinc_Integral.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Probability/Sinc_Integral.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -271,7 +271,7 @@
 
 lemma Si_at_top: "(Si \<longlongrightarrow> pi / 2) at_top"
 proof -
-  have "\<forall>\<^sub>F t in at_top. pi / 2 - (LBINT u=0..\<infinity>. exp (-(u * t)) * (u * sin t + cos t) / (1 + u^2)) = Si t"
+  have \<dagger>: "\<forall>\<^sub>F t in at_top. pi / 2 - (LBINT u=0..\<infinity>. exp (-(u * t)) * (u * sin t + cos t) / (1 + u^2)) = Si t"
     using eventually_ge_at_top[of 0]
   proof eventually_elim
     fix t :: real assume "t \<ge> 0"
@@ -326,8 +326,8 @@
       using Si_at_top_integrable[OF \<open>0\<le>t\<close>] by (simp add: integrable_I0i_1_div_plus_square LBINT_I0i_1_div_plus_square)
     finally show "pi / 2 - (LBINT u=0..\<infinity>. exp (-(u * t)) * (u * sin t + cos t) / (1 + u^2)) = Si t" ..
   qed
-  then show ?thesis
-    by (rule Lim_transform_eventually)
+  show ?thesis
+    by (rule Lim_transform_eventually [OF _ \<dagger>])
        (auto intro!: tendsto_eq_intros Si_at_top_LBINT)
 qed
 
diff -r 2d2b5a8e8d59 -r fcf3b891ccb1 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Aug 14 19:50:23 2019 +0200
+++ b/src/HOL/Transcendental.thy	Thu Aug 15 16:11:56 2019 +0100
@@ -4135,6 +4135,15 @@
     using that by (auto elim: evenE)
 qed
 
+lemma sin_zero_pi_iff:
+  fixes x::real
+  assumes "\<bar>x\<bar> < pi"
+  shows "sin x = 0 \<longleftrightarrow> x = 0"
+proof
+  show "x = 0" if "sin x = 0"
+    using that assms by (auto simp: sin_zero_iff)
+qed auto
+
 lemma cos_zero_iff_int: "cos x = 0 \<longleftrightarrow> (\<exists>n. odd n \<and> x = of_int n * (pi/2))"
 proof -
   have 1: "\<And>n. odd n \<Longrightarrow> \<exists>i. odd i \<and> real n = real_of_int i"