merged
authorwenzelm
Thu, 19 Sep 2019 16:38:32 +0200
changeset 70736 dea35c31a0b8
parent 70726 91587befabfd (diff)
parent 70735 561b11865cb5 (current diff)
child 70738 da7c0df11a04
child 70739 29243d779b61
merged
--- a/src/HOL/Analysis/Change_Of_Vars.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -9,41 +9,6 @@
 
 begin
 
-subsection \<open>Orthogonal Transformation of Balls\<close>
-
-lemma image_orthogonal_transformation_ball:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
-  assumes "orthogonal_transformation f"
-  shows "f ` ball x r = ball (f x) r"
-proof (intro equalityI subsetI)
-  fix y assume "y \<in> f ` ball x r"
-  with assms show "y \<in> ball (f x) r"
-    by (auto simp: orthogonal_transformation_isometry)
-next
-  fix y assume y: "y \<in> ball (f x) r"
-  then obtain z where z: "y = f z"
-    using assms orthogonal_transformation_surj by blast
-  with y assms show "y \<in> f ` ball x r"
-    by (auto simp: orthogonal_transformation_isometry)
-qed
-
-lemma  image_orthogonal_transformation_cball:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
-  assumes "orthogonal_transformation f"
-  shows "f ` cball x r = cball (f x) r"
-proof (intro equalityI subsetI)
-  fix y assume "y \<in> f ` cball x r"
-  with assms show "y \<in> cball (f x) r"
-    by (auto simp: orthogonal_transformation_isometry)
-next
-  fix y assume y: "y \<in> cball (f x) r"
-  then obtain z where z: "y = f z"
-    using assms orthogonal_transformation_surj by blast
-  with y assms show "y \<in> f ` cball x r"
-    by (auto simp: orthogonal_transformation_isometry)
-qed
-
-
 subsection \<open>Measurable Shear and Stretch\<close>
 
 proposition
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -2568,12 +2568,23 @@
   apply (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide)
   done
 
-lemma lim_ln_over_n: "((\<lambda>n. ln(real_of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
+lemma lim_ln_over_n [tendsto_intros]: "((\<lambda>n. ln(real_of_nat n) / of_nat n) \<longlongrightarrow> 0) sequentially"
   using lim_ln_over_power [of 1, THEN filterlim_sequentially_Suc [THEN iffD2]]
   apply (subst filterlim_sequentially_Suc [symmetric])
   apply (simp add: lim_sequentially dist_norm)
   done
 
+lemma lim_log_over_n [tendsto_intros]:
+  "(\<lambda>n. log k n/n) \<longlonglongrightarrow> 0"
+proof -
+  have *: "log k n/n = (1/ln k) * (ln n / n)" for n
+    unfolding log_def by auto
+  have "(\<lambda>n. (1/ln k) * (ln n / n)) \<longlonglongrightarrow> (1/ln k) * 0"
+    by (intro tendsto_intros)
+  then show ?thesis
+    unfolding * by auto
+qed
+
 lemma lim_1_over_complex_power:
   assumes "0 < Re s"
   shows "(\<lambda>n. 1 / of_nat n powr s) \<longlonglongrightarrow> 0"
--- a/src/HOL/Analysis/Derivative.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -233,6 +233,12 @@
   unfolding frechet_derivative_works has_derivative_def
   by (auto intro: bounded_linear.linear)
 
+lemma frechet_derivative_const [simp]: "frechet_derivative (\<lambda>x. c) (at a) = (\<lambda>x. 0)"
+  using differentiable_const frechet_derivative_works has_derivative_const has_derivative_unique by blast
+
+lemma frechet_derivative_id [simp]: "frechet_derivative id (at a) = id"
+  using differentiable_def frechet_derivative_works has_derivative_id has_derivative_unique by blast
+
 
 subsection \<open>Differentiability implies continuity\<close>
 
@@ -485,6 +491,11 @@
   "(f has_derivative f') (at x) \<Longrightarrow> f' = frechet_derivative f (at x)"
   using differentiable_def frechet_derivative_works has_derivative_unique by blast
 
+lemma frechet_derivative_compose:
+  "frechet_derivative (f o g) (at x) = frechet_derivative (f) (at (g x)) o frechet_derivative g (at x)"
+  if "g differentiable at x" "f differentiable at (g x)"
+  by (metis diff_chain_at frechet_derivative_at frechet_derivative_works that)
+
 lemma frechet_derivative_within_cbox:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "\<And>i. i\<in>Basis \<Longrightarrow> a\<bullet>i < b\<bullet>i"
@@ -494,6 +505,11 @@
   using assms
   by (metis Derivative.differentiableI frechet_derivative_unique_within_closed_interval frechet_derivative_works)
 
+lemma frechet_derivative_transform_within_open:
+  "frechet_derivative f (at x) = frechet_derivative g (at x)"
+  if "f differentiable at x" "open X" "x \<in> X" "\<And>x. x \<in> X \<Longrightarrow> f x = g x"
+  by (meson frechet_derivative_at frechet_derivative_works has_derivative_transform_within_open that)
+
 
 subsection \<open>Derivatives of local minima and maxima are zero\<close>
 
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -2000,6 +2000,11 @@
 lemma infdist_zero[simp]: "a \<in> A \<Longrightarrow> infdist a A = 0"
   by (auto intro!: antisym infdist_nonneg infdist_le2)
 
+lemma infdist_Un_min:
+  assumes "A \<noteq> {}" "B \<noteq> {}"
+  shows "infdist x (A \<union> B) = min (infdist x A) (infdist x B)"
+using assms by (simp add: infdist_def cINF_union inf_real_def)
+
 lemma infdist_triangle: "infdist x A \<le> infdist y A + dist x y"
 proof (cases "A = {}")
   case True
@@ -2041,6 +2046,9 @@
   finally show ?thesis by simp
 qed
 
+lemma infdist_triangle_abs: "\<bar>infdist x A - infdist y A\<bar> \<le> dist x y"
+  by (metis (full_types) abs_diff_le_iff diff_le_eq dist_commute infdist_triangle)
+
 lemma in_closure_iff_infdist_zero:
   assumes "A \<noteq> {}"
   shows "x \<in> closure A \<longleftrightarrow> infdist x A = 0"
@@ -2179,6 +2187,11 @@
   shows "continuous F (\<lambda>x. infdist (f x) A)"
   using assms unfolding continuous_def by (rule tendsto_infdist)
 
+lemma continuous_on_infdist [continuous_intros]:
+  assumes "continuous_on S f"
+  shows "continuous_on S (\<lambda>x. infdist (f x) A)"
+using assms unfolding continuous_on by (auto intro: tendsto_infdist)
+
 lemma compact_infdist_le:
   fixes A::"'a::heine_borel set"
   assumes "A \<noteq> {}"
@@ -3231,8 +3244,14 @@
     by (auto simp: setdist_def infdist_def)
 qed
 
-lemma continuous_on_infdist [continuous_intros]: "continuous_on B (\<lambda>y. infdist y A)"
-  by (simp add: continuous_on_setdist infdist_eq_setdist)
+lemma infdist_mono:
+  assumes "A \<subseteq> B" "A \<noteq> {}"
+  shows "infdist x B \<le> infdist x A"
+  by (simp add: assms infdist_eq_setdist setdist_subset_right)
+
+lemma infdist_singleton [simp]:
+  "infdist x {y} = dist x y"
+  by (simp add: infdist_eq_setdist)
 
 proposition setdist_attains_inf:
   assumes "compact B" "B \<noteq> {}"
@@ -3244,7 +3263,7 @@
 next
   case False
   obtain y where "y \<in> B" and min: "\<And>y'. y' \<in> B \<Longrightarrow> infdist y A \<le> infdist y' A"
-    using continuous_attains_inf [OF assms continuous_on_infdist] by blast
+    by (metis continuous_attains_inf [OF assms continuous_on_infdist] continuous_on_id)
   show thesis
   proof
     have "setdist A B = (INF y\<in>B. infdist y A)"
@@ -3266,4 +3285,4 @@
   qed (fact \<open>y \<in> B\<close>)
 qed
 
-end
\ No newline at end of file
+end
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -9,17 +9,13 @@
 theory Elementary_Normed_Spaces
   imports
   "HOL-Library.FuncSet"
-  Elementary_Metric_Spaces Linear_Algebra
+  Elementary_Metric_Spaces Cartesian_Space
   Connected
 begin
+subsection \<open>Orthogonal Transformation of Balls\<close>
 
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Various Lemmas Combining Imports\<close>
 
-lemma countable_PiE:
-  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)"
-  by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq)
-
-
 lemma open_sums:
   fixes T :: "('b::real_normed_vector) set"
   assumes "open S \<or> open T"
@@ -53,6 +49,38 @@
   qed
 qed
 
+lemma image_orthogonal_transformation_ball:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+  assumes "orthogonal_transformation f"
+  shows "f ` ball x r = ball (f x) r"
+proof (intro equalityI subsetI)
+  fix y assume "y \<in> f ` ball x r"
+  with assms show "y \<in> ball (f x) r"
+    by (auto simp: orthogonal_transformation_isometry)
+next
+  fix y assume y: "y \<in> ball (f x) r"
+  then obtain z where z: "y = f z"
+    using assms orthogonal_transformation_surj by blast
+  with y assms show "y \<in> f ` ball x r"
+    by (auto simp: orthogonal_transformation_isometry)
+qed
+
+lemma image_orthogonal_transformation_cball:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+  assumes "orthogonal_transformation f"
+  shows "f ` cball x r = cball (f x) r"
+proof (intro equalityI subsetI)
+  fix y assume "y \<in> f ` cball x r"
+  with assms show "y \<in> cball (f x) r"
+    by (auto simp: orthogonal_transformation_isometry)
+next
+  fix y assume y: "y \<in> cball (f x) r"
+  then obtain z where z: "y = f z"
+    using assms orthogonal_transformation_surj by blast
+  with y assms show "y \<in> f ` cball x r"
+    by (auto simp: orthogonal_transformation_isometry)
+qed
+
 
 subsection \<open>Support\<close>
 
--- a/src/HOL/Analysis/Elementary_Topology.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Topology.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -2479,6 +2479,14 @@
   unfolding homeomorphism_def
   by (intro conjI ballI continuous_on_compose) (auto simp: image_iff)
 
+lemma homeomorphism_cong:
+  "homeomorphism X' Y' f' g'"
+    if "homeomorphism X Y f g" "X' = X" "Y' = Y" "\<And>x. x \<in> X \<Longrightarrow> f' x = f x" "\<And>y. y \<in> Y \<Longrightarrow> g' y = g y"
+  using that by (auto simp add: homeomorphism_def)
+
+lemma homeomorphism_empty [simp]:
+  "homeomorphism {} {} f g"
+  unfolding homeomorphism_def by auto
 
 lemma homeomorphism_symD: "homeomorphism S t f g \<Longrightarrow> homeomorphism t S g f"
   by (simp add: homeomorphism_def)
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -1108,6 +1108,48 @@
   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 integrable_subinterval:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "integrable (lebesgue_on {a..b}) f"
+    and "{c..d} \<subseteq> {a..b}"
+  shows "integrable (lebesgue_on {c..d}) f"
+proof (rule absolutely_integrable_imp_integrable)
+  show "f absolutely_integrable_on {c..d}"
+  proof -
+    have "f integrable_on {c..d}"
+      using assms integrable_on_lebesgue_on integrable_on_subinterval by fastforce
+    moreover have "(\<lambda>x. norm (f x)) integrable_on {c..d}"
+    proof (rule integrable_on_subinterval)
+      show "(\<lambda>x. norm (f x)) integrable_on {a..b}"
+        by (simp add: assms integrable_on_lebesgue_on)
+    qed (use assms in auto)
+    ultimately show ?thesis
+      by (auto simp: absolutely_integrable_on_def)
+  qed
+qed auto
+
+lemma indefinite_integral_continuous_real:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "integrable (lebesgue_on {a..b}) f"
+  shows "continuous_on {a..b} (\<lambda>x. integral\<^sup>L (lebesgue_on {a..x}) f)"
+proof -
+  have "f integrable_on {a..b}"
+    by (simp add: assms integrable_on_lebesgue_on)
+  then have "continuous_on {a..b} (\<lambda>x. integral {a..x} f)"
+    using indefinite_integral_continuous_1 by blast
+  moreover have "integral\<^sup>L (lebesgue_on {a..x}) f = integral {a..x} f" if "a \<le> x" "x \<le> b" for x
+  proof -
+    have "{a..x} \<subseteq> {a..b}"
+      using that by auto
+    then have "integrable (lebesgue_on {a..x}) f"
+      using integrable_subinterval assms by blast
+    then show "integral\<^sup>L (lebesgue_on {a..x}) f = integral {a..x} f"
+      by (simp add: lebesgue_integral_eq_integral)
+  qed
+  ultimately show ?thesis
+    by (metis (no_types, lifting) atLeastAtMost_iff continuous_on_cong)
+qed
+
 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)
@@ -3132,21 +3174,8 @@
   qed
 qed
 
-
 subsection\<open>Lemmas about absolute integrability\<close>
 
-text\<open>FIXME Redundant!\<close>
-lemma absolutely_integrable_add[intro]:
-  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x + g x) absolutely_integrable_on s"
-  by (rule set_integral_add)
-
-text\<open>FIXME Redundant!\<close>
-lemma absolutely_integrable_diff[intro]:
-  fixes f g :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
-  shows "f absolutely_integrable_on s \<Longrightarrow> g absolutely_integrable_on s \<Longrightarrow> (\<lambda>x. f x - g x) absolutely_integrable_on s"
-  by (rule set_integral_diff)
-
 lemma absolutely_integrable_linear:
   fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
     and h :: "'n::euclidean_space \<Rightarrow> 'p::euclidean_space"
@@ -3375,8 +3404,8 @@
   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)))
                  absolutely_integrable_on S"
-    apply (intro absolutely_integrable_add absolutely_integrable_scaleR_left assms)
-    using absolutely_integrable_abs [OF absolutely_integrable_diff [OF assms]]
+    apply (intro set_integral_add absolutely_integrable_scaleR_left assms)
+    using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
     apply (simp add: algebra_simps)
     done
   ultimately show ?thesis by metis
@@ -3410,8 +3439,8 @@
   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)))
                  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]]
+    apply (intro set_integral_add set_integral_diff absolutely_integrable_scaleR_left assms)
+    using absolutely_integrable_abs [OF set_integral_diff(1) [OF assms]]
     apply (simp add: algebra_simps)
     done
   ultimately show ?thesis by metis
@@ -3450,7 +3479,7 @@
   shows "f absolutely_integrable_on A"
 proof -
   have "(\<lambda>x. g x - (g x - f x)) absolutely_integrable_on A"
-    apply (rule absolutely_integrable_diff [OF g nonnegative_absolutely_integrable])
+    apply (rule set_integral_diff [OF g nonnegative_absolutely_integrable])
     using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast
     by (simp add: comp inner_diff_left)
   then show ?thesis
@@ -3464,7 +3493,7 @@
   shows "g absolutely_integrable_on A"
 proof -
   have "(\<lambda>x. f x + (g x - f x)) absolutely_integrable_on A"
-    apply (rule absolutely_integrable_add [OF f nonnegative_absolutely_integrable])
+    apply (rule set_integral_add [OF f nonnegative_absolutely_integrable])
     using Henstock_Kurzweil_Integration.integrable_diff absolutely_integrable_on_def f g apply blast
     by (simp add: comp inner_diff_left)
   then show ?thesis
@@ -4495,6 +4524,22 @@
     by (auto simp: has_bochner_integral_restrict_space)
 qed
 
+lemma has_bochner_integral_reflect_real[simp]:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  shows "has_bochner_integral (lebesgue_on {-b..-a}) (\<lambda>x. f(-x)) i \<longleftrightarrow> has_bochner_integral (lebesgue_on {a..b}) f i"
+  by (auto simp: dest: has_bochner_integral_reflect_real_lemma)
+
+lemma integrable_reflect_real[simp]:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  shows "integrable (lebesgue_on {-b..-a}) (\<lambda>x. f(-x)) \<longleftrightarrow> integrable (lebesgue_on {a..b}) f"
+  by (metis has_bochner_integral_iff has_bochner_integral_reflect_real)
+
+lemma integral_reflect_real[simp]:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  shows "integral\<^sup>L (lebesgue_on {-b .. -a}) (\<lambda>x. f(-x)) = integral\<^sup>L (lebesgue_on {a..b::real}) f"
+  using has_bochner_integral_reflect_real [of b a f]
+  by (metis has_bochner_integral_iff not_integrable_integral_eq)
+
 subsection\<open>More results on integrability\<close>
 
 lemma integrable_on_all_intervals_UNIV:
@@ -4790,15 +4835,24 @@
        "(\<lambda>x. if x \<in> T then f x else 0) absolutely_integrable_on UNIV"
     using S T absolutely_integrable_restrict_UNIV by blast+
   then have "(\<lambda>x. (if x \<in> S then f x else 0) + (if x \<in> T then f x else 0)) absolutely_integrable_on UNIV"
-    by (rule absolutely_integrable_add)
+    by (rule set_integral_add)
   then have "(\<lambda>x. ((if x \<in> S then f x else 0) + (if x \<in> T then f x else 0)) - (if x \<in> ?ST then f x else 0)) absolutely_integrable_on UNIV"
-    using Int by (rule absolutely_integrable_diff)
+    using Int by (rule set_integral_diff)
   then have "(\<lambda>x. if x \<in> S \<union> T then f x else 0) absolutely_integrable_on UNIV"
     by (rule absolutely_integrable_spike) (auto intro: empty_imp_negligible)
   then show ?thesis
     unfolding absolutely_integrable_restrict_UNIV .
 qed
 
+lemma absolutely_integrable_on_combine:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "f absolutely_integrable_on {a..c}"
+    and "f absolutely_integrable_on {c..b}"
+    and "a \<le> c"
+    and "c \<le> b"
+  shows "f absolutely_integrable_on {a..b}"
+  by (metis absolutely_integrable_Un assms ivl_disj_un_two_touch(4))
+
 lemma uniform_limit_set_lebesgue_integral_at_top:
   fixes f :: "'a \<Rightarrow> real \<Rightarrow> 'b::{banach, second_countable_topology}"
     and g :: "real \<Rightarrow> real"
--- a/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -860,32 +860,6 @@
   qed (auto simp: conF)
 qed
 
-
-lemma measurable_on_preimage_lemma0:
-  fixes f :: "'a::euclidean_space \<Rightarrow> real"
-  assumes "m \<in> \<int>" and f: "m / 2^n \<le> (f x)" "(f x) < (m+1) / 2^n" and m: "\<bar>m\<bar> \<le> 2^(2 * n)"
-  shows "(\<Sum>k\<in>{k \<in> \<int>. \<bar>k\<bar> \<le> 2^(2 * n)}.
-             (k / 2^n) * indicator {y. k / 2^n \<le> f y \<and> f y < (k+1) / 2^n} x)
-       = (m / 2^n)"  (is "?lhs = ?rhs")
-proof -
-  have "?lhs = (\<Sum>k\<in>{m}. (k / 2^n) * indicator {y. k / 2^n \<le> f y \<and> f y < (k+1) / 2^n} x)"
-  proof (intro sum.mono_neutral_right ballI)
-    show "finite {k::real. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2^(2 * n)}"
-      using finite_abs_int_segment by blast
-    show "(i / 2^n) * indicat_real {y. i / 2^n \<le> f y \<and> f y < (i+1) / 2^n} x = 0"
-      if "i \<in> {N \<in> \<int>. \<bar>N\<bar> \<le> 2^(2 * n)} - {m}" for i
-      using f m \<open>m \<in> \<int>\<close> that Ints_eq_abs_less1 [of i m]
-      by (auto simp: indicator_def divide_simps)
-  qed (auto simp: assms)
-  also have "\<dots> = ?rhs"
-    using assms by (auto simp: indicator_def)
-  finally show ?thesis .
-qed
-
-(*see HOL Light's lebesgue_measurable BUT OUR lmeasurable IS NOT THE SAME. It's more like "sets lebesgue"
- `lebesgue_measurable s <=> (indicator s) measurable_on (:real^N)`;;
-*)
-
 proposition indicator_measurable_on:
   assumes "S \<in> sets lebesgue"
   shows "indicat_real S measurable_on UNIV"
@@ -1615,6 +1589,7 @@
 qed
 
 subsection \<open>Measurability on generalisations of the binary product\<close>
+
 lemma measurable_on_bilinear:
   fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::euclidean_space"
   assumes h: "bilinear h" and f: "f measurable_on S" and g: "g measurable_on S"
@@ -1663,4 +1638,72 @@
   shows "(\<lambda>x. f x * g x) absolutely_integrable_on S"
   using absolutely_integrable_bounded_measurable_product bilinear_times assms by blast
 
+
+lemma borel_measurable_AE:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "f \<in> borel_measurable lebesgue" and ae: "AE x in lebesgue. f x = g x"
+  shows "g \<in> borel_measurable lebesgue"
+proof -
+  obtain N where N: "N \<in> null_sets lebesgue" "\<And>x. x \<notin> N \<Longrightarrow> f x = g x"
+    using ae unfolding completion.AE_iff_null_sets by auto
+  have "f measurable_on UNIV"
+    by (simp add: assms lebesgue_measurable_imp_measurable_on)
+  then have "g measurable_on UNIV"
+    by (metis Diff_iff N measurable_on_spike negligible_iff_null_sets)
+  then show ?thesis
+    using measurable_on_imp_borel_measurable_lebesgue_UNIV by blast
+qed
+
+lemma has_bochner_integral_combine:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "a \<le> c" "c \<le> b"
+    and ac: "has_bochner_integral (lebesgue_on {a..c}) f i"
+    and cb: "has_bochner_integral (lebesgue_on {c..b}) f j"
+  shows "has_bochner_integral (lebesgue_on {a..b}) f(i + j)"
+proof -
+  have i: "has_bochner_integral lebesgue (\<lambda>x. indicator {a..c} x *\<^sub>R f x) i"
+   and j: "has_bochner_integral lebesgue (\<lambda>x. indicator {c..b} x *\<^sub>R f x) j"
+    using assms  by (auto simp: has_bochner_integral_restrict_space)
+  have AE: "AE x in lebesgue. indicat_real {a..c} x *\<^sub>R f x + indicat_real {c..b} x *\<^sub>R f x = indicat_real {a..b} x *\<^sub>R f x"
+  proof (rule AE_I')
+    have eq: "indicat_real {a..c} x *\<^sub>R f x + indicat_real {c..b} x *\<^sub>R f x = indicat_real {a..b} x *\<^sub>R f x" if "x \<noteq> c" for x
+      using assms that by (auto simp: indicator_def)
+    then show "{x \<in> space lebesgue. indicat_real {a..c} x *\<^sub>R f x + indicat_real {c..b} x *\<^sub>R f x \<noteq> indicat_real {a..b} x *\<^sub>R f x} \<subseteq> {c}"
+      by auto
+  qed auto
+  have "has_bochner_integral lebesgue (\<lambda>x. indicator {a..b} x *\<^sub>R f x) (i + j)"
+  proof (rule has_bochner_integralI_AE [OF has_bochner_integral_add [OF i j] _ AE])
+    have eq: "indicat_real {a..c} x *\<^sub>R f x + indicat_real {c..b} x *\<^sub>R f x = indicat_real {a..b} x *\<^sub>R f x" if "x \<noteq> c" for x
+      using assms that by (auto simp: indicator_def)
+    show "(\<lambda>x. indicat_real {a..b} x *\<^sub>R f x) \<in> borel_measurable lebesgue"
+    proof (rule borel_measurable_AE [OF borel_measurable_add AE])
+      show "(\<lambda>x. indicator {a..c} x *\<^sub>R f x) \<in> borel_measurable lebesgue"
+           "(\<lambda>x. indicator {c..b} x *\<^sub>R f x) \<in> borel_measurable lebesgue"
+        using i j by auto
+    qed
+  qed
+  then show ?thesis
+    by (simp add: has_bochner_integral_restrict_space)
+qed
+
+lemma integrable_combine:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes "integrable (lebesgue_on {a..c}) f" "integrable (lebesgue_on {c..b}) f"
+    and "a \<le> c" "c \<le> b"
+  shows "integrable (lebesgue_on {a..b}) f"
+  using assms has_bochner_integral_combine has_bochner_integral_iff by blast
+
+lemma integral_combine:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes f: "integrable (lebesgue_on {a..b}) f" and "a \<le> c" "c \<le> b"
+  shows "integral\<^sup>L (lebesgue_on {a..b}) f = integral\<^sup>L (lebesgue_on {a..c}) f + integral\<^sup>L (lebesgue_on {c..b}) f"
+proof -
+  have i: "has_bochner_integral (lebesgue_on {a..c}) f(integral\<^sup>L (lebesgue_on {a..c}) f)"
+    using integrable_subinterval \<open>c \<le> b\<close> f has_bochner_integral_iff by fastforce
+  have j: "has_bochner_integral (lebesgue_on {c..b}) f(integral\<^sup>L (lebesgue_on {c..b}) f)"
+    using integrable_subinterval \<open>a \<le> c\<close> f has_bochner_integral_iff by fastforce
+  show ?thesis
+    by (meson \<open>a \<le> c\<close> \<open>c \<le> b\<close> has_bochner_integral_combine has_bochner_integral_iff i j)
+qed
+
 end
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -6935,6 +6935,19 @@
   by (intro has_integral_substitution_strong[of "{}" a b g c d] assms)
      (auto intro: DERIV_continuous_on assms)
 
+lemma integral_shift:
+  fixes f :: "real \<Rightarrow> 'a::euclidean_space"
+  assumes cont: "continuous_on {a + c..b + c} f"
+  shows "integral {a..b} (f \<circ> (\<lambda>x. x + c)) = integral {a + c..b + c} f"
+proof (cases "a \<le> b")
+  case True
+  have "((\<lambda>x. 1 *\<^sub>R f (x + c)) has_integral integral {a+c..b+c} f) {a..b}"
+    using True cont
+    by (intro has_integral_substitution[where c = "a + c" and d = "b + c"])
+       (auto intro!: derivative_eq_intros)
+  thus ?thesis by (simp add: has_integral_iff o_def)
+qed auto
+
 
 subsection \<open>Compute a double integral using iterated integrals and switching the order of integration\<close>
 
--- a/src/HOL/Analysis/Improper_Integral.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Improper_Integral.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -1757,13 +1757,11 @@
             have I_int [simp]: "?I \<inter> box a b = ?I"
               using 1 by (simp add: Int_absorb2)
             have int_fI: "f integrable_on ?I"
-              apply (rule integrable_subinterval [OF int_f order_refl])
-              using "*" box_subset_cbox by blast
+              by (metis I_int inf_le2 int_f)
             then have "(\<lambda>x. f x \<bullet> j) integrable_on ?I"
               by (simp add: integrable_component)
             moreover have "g integrable_on ?I"
-              apply (rule integrable_subinterval [OF int_gab])
-              using "*" box_subset_cbox by blast
+              by (metis I_int inf.orderI int_gab integrable_on_open_interval integrable_on_subcbox)
             moreover
             have "\<bar>integral ?I (\<lambda>x. f x \<bullet> j)\<bar> \<le> norm (integral ?I f)"
               by (simp add: Basis_le_norm int_fI \<open>j \<in> Basis\<close>)
@@ -1837,13 +1835,11 @@
             have I_int [simp]: "?I \<inter> box a b = ?I"
               using 1 by (simp add: Int_absorb2)
             have int_fI: "f integrable_on ?I"
-              apply (rule integrable_subinterval [OF int_f order_refl])
-              using "*" box_subset_cbox by blast
+              by (simp add: inf.orderI int_f)
             then have "(\<lambda>x. f x \<bullet> j) integrable_on ?I"
               by (simp add: integrable_component)
             moreover have "g integrable_on ?I"
-              apply (rule integrable_subinterval [OF int_gab])
-              using "*" box_subset_cbox by blast
+              by (metis I_int inf.orderI int_gab integrable_on_open_interval integrable_on_subcbox)
             moreover
             have "\<bar>integral ?I (\<lambda>x. f x \<bullet> j)\<bar> \<le> norm (integral ?I f)"
               by (simp add: Basis_le_norm int_fI \<open>j \<in> Basis\<close>)
@@ -2268,6 +2264,5 @@
     using second_mean_value_theorem_full [where g=g, OF assms]
     by (metis (full_types) integral_unique)
 
-
 end
 
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -1219,8 +1219,10 @@
   finally show ?thesis .
 qed
 
-lemma lborel_distr_plus: "distr lborel borel ((+) c) = (lborel :: real measure)"
-  by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ennreal_def[symmetric])
+lemma lborel_distr_plus:
+  fixes c :: "'a::euclidean_space"
+  shows "distr lborel borel ((+) c) = lborel"
+by (subst lborel_affine[of 1 c], auto simp: density_1)
 
 interpretation lborel: sigma_finite_measure lborel
   by (rule sigma_finite_lborel)
--- a/src/HOL/Analysis/Measure_Space.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -472,10 +472,23 @@
   "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> emeasure M a + emeasure M b = emeasure M (a \<union> b)"
   using additiveD[OF emeasure_additive] ..
 
-lemma emeasure_Union:
+lemma emeasure_Un:
   "A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> emeasure M (A \<union> B) = emeasure M A + emeasure M (B - A)"
   using plus_emeasure[of A M "B - A"] by auto
 
+lemma emeasure_Un_Int:
+  assumes "A \<in> sets M" "B \<in> sets M"
+  shows "emeasure M A + emeasure M B = emeasure M (A \<union> B) + emeasure M (A \<inter> B)"
+proof -
+  have "A = (A-B) \<union> (A \<inter> B)" by auto
+  then have "emeasure M A = emeasure M (A-B) + emeasure M (A \<inter> B)"
+    by (metis Diff_Diff_Int Diff_disjoint assms plus_emeasure sets.Diff)
+  moreover have "A \<union> B = (A-B) \<union> B" by auto
+  then have "emeasure M (A \<union> B) = emeasure M (A-B) + emeasure M B"
+    by (metis Diff_disjoint Int_commute assms plus_emeasure sets.Diff)
+  ultimately show ?thesis by (metis add.assoc add.commute)
+qed
+
 lemma sum_emeasure:
   "F`I \<subseteq> sets M \<Longrightarrow> disjoint_family_on F I \<Longrightarrow> finite I \<Longrightarrow>
     (\<Sum>i\<in>I. emeasure M (F i)) = emeasure M (\<Union>i\<in>I. F i)"
@@ -987,6 +1000,18 @@
     by (subst plus_emeasure[symmetric]) auto
 qed
 
+lemma emeasure_Un':
+  assumes "A \<in> sets M" "B \<in> sets M" "A \<inter> B \<in> null_sets M"
+  shows   "emeasure M (A \<union> B) = emeasure M A + emeasure M B"
+proof -
+  have "A \<union> B = A \<union> (B - A \<inter> B)" by blast
+  also have "emeasure M \<dots> = emeasure M A + emeasure M (B - A \<inter> B)"
+    using assms by (subst plus_emeasure) auto
+  also have "emeasure M (B - A \<inter> B) = emeasure M B"
+    using assms by (intro emeasure_Diff_null_set) auto
+  finally show ?thesis .
+qed
+
 subsection \<open>The almost everywhere filter (i.e.\ quantifier)\<close>
 
 definition\<^marker>\<open>tag important\<close> ae_filter :: "'a measure \<Rightarrow> 'a filter" where
--- a/src/HOL/Analysis/Set_Integral.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -173,12 +173,30 @@
   unfolding set_integrable_def
   using integrable_mult_right[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
 
+lemma set_integrable_mult_right_iff [simp]:
+  fixes a :: "'a::{real_normed_field, second_countable_topology}"
+  assumes "a \<noteq> 0"
+  shows "set_integrable M A (\<lambda>t. a * f t) \<longleftrightarrow> set_integrable M A f"
+proof
+  assume "set_integrable M A (\<lambda>t. a * f t)"
+  then have "set_integrable M A (\<lambda>t. 1/a * (a * f t))"
+    using set_integrable_mult_right by blast
+  then show "set_integrable M A f"
+    using assms by auto
+qed auto
+
 lemma set_integrable_mult_left [simp, intro]:
   fixes a :: "'a::{real_normed_field, second_countable_topology}"
   shows "(a \<noteq> 0 \<Longrightarrow> set_integrable M A f) \<Longrightarrow> set_integrable M A (\<lambda>t. f t * a)"
   unfolding set_integrable_def
   using integrable_mult_left[of a M "\<lambda>x. indicator A x *\<^sub>R f x"] by simp
 
+lemma set_integrable_mult_left_iff [simp]:
+  fixes a :: "'a::{real_normed_field, second_countable_topology}"
+  assumes "a \<noteq> 0"
+  shows "set_integrable M A (\<lambda>t. f t * a) \<longleftrightarrow> set_integrable M A f"
+  using assms by (subst set_integrable_mult_right_iff [symmetric]) (auto simp: mult.commute)
+
 lemma set_integrable_divide [simp, intro]:
   fixes a :: "'a::{real_normed_field, field, second_countable_topology}"
   assumes "a \<noteq> 0 \<Longrightarrow> set_integrable M A f"
@@ -192,6 +210,12 @@
     unfolding set_integrable_def .
 qed
 
+lemma set_integrable_mult_divide_iff [simp]:
+  fixes a :: "'a::{real_normed_field, second_countable_topology}"
+  assumes "a \<noteq> 0"
+  shows "set_integrable M A (\<lambda>t. f t / a) \<longleftrightarrow> set_integrable M A f"
+  by (simp add: divide_inverse assms)
+
 lemma set_integral_add [simp, intro]:
   fixes f g :: "_ \<Rightarrow> _ :: {banach, second_countable_topology}"
   assumes "set_integrable M A f" "set_integrable M A g"
@@ -205,8 +229,6 @@
     (LINT x:A|M. f x) - (LINT x:A|M. g x)"
   using assms unfolding set_integrable_def set_lebesgue_integral_def by (simp_all add: scaleR_diff_right)
 
-(* question: why do we have this for negation, but multiplication by a constant
-   requires an integrability assumption? *)
 lemma set_integral_uminus: "set_integrable M A f \<Longrightarrow> LINT x:A|M. - f x = - (LINT x:A|M. f x)"
   unfolding set_integrable_def set_lebesgue_integral_def
   by (subst integral_minus[symmetric]) simp_all
--- a/src/HOL/Finite_Set.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Finite_Set.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -1493,12 +1493,11 @@
   using card_Un_Int [of A B] by simp
 
 lemma card_Un_le: "card (A \<union> B) \<le> card A + card B"
-  apply (cases "finite A")
-   apply (cases "finite B")
-    apply (use le_iff_add card_Un_Int in blast)
-   apply simp
-  apply simp
-  done
+proof (cases "finite A \<and> finite B")
+  case True
+  then show ?thesis
+    using le_iff_add card_Un_Int [of A B] by auto
+qed auto
 
 lemma card_Diff_subset:
   assumes "finite B"
--- a/src/HOL/Groups_Big.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Groups_Big.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -1187,6 +1187,16 @@
     using assms card_eq_0_iff finite_UnionD by fastforce
 qed
 
+lemma card_UN_le:
+  assumes "finite I"
+  shows "card(\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. card(A i))"
+  using assms
+proof induction
+  case (insert i I)
+  then show ?case
+    using card_Un_le nat_add_left_cancel_le by (force intro: order_trans) 
+qed auto
+
 lemma sum_multicount_gen:
   assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
   shows "sum (\<lambda>i. (card {j\<in>t. R i j})) s = sum k t"
--- a/src/HOL/Library/Extended_Real.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -1725,13 +1725,44 @@
   by (cases a b c rule: ereal3_cases)
      (auto simp: field_simps zero_less_mult_iff)
 
-lemma ereal_inverse_real: "\<bar>z\<bar> \<noteq> \<infinity> \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> ereal (inverse (real_of_ereal z)) = inverse z"
-  by (cases z) simp_all
+lemma ereal_inverse_real [simp]: "\<bar>z\<bar> \<noteq> \<infinity> \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> ereal (inverse (real_of_ereal z)) = inverse z"
+  by auto
 
 lemma ereal_inverse_mult:
   "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> inverse (a * (b::ereal)) = inverse a * inverse b"
   by (cases a; cases b) auto
 
+lemma inverse_eq_infinity_iff_eq_zero [simp]:
+  "1/(x::ereal) = \<infinity> \<longleftrightarrow> x = 0"
+by (simp add: divide_ereal_def)
+
+lemma ereal_distrib_left:
+  fixes a b c :: ereal
+  assumes "a \<noteq> \<infinity> \<or> b \<noteq> -\<infinity>"
+    and "a \<noteq> -\<infinity> \<or> b \<noteq> \<infinity>"
+    and "\<bar>c\<bar> \<noteq> \<infinity>"
+  shows "c * (a + b) = c * a + c * b"
+using assms
+by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
+
+lemma ereal_distrib_minus_left:
+  fixes a b c :: ereal
+  assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>"
+    and "a \<noteq> -\<infinity> \<or> b \<noteq> -\<infinity>"
+    and "\<bar>c\<bar> \<noteq> \<infinity>"
+  shows "c * (a - b) = c * a - c * b"
+using assms
+by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
+
+lemma ereal_distrib_minus_right:
+  fixes a b c :: ereal
+  assumes "a \<noteq> \<infinity> \<or> b \<noteq> \<infinity>"
+    and "a \<noteq> -\<infinity> \<or> b \<noteq> -\<infinity>"
+    and "\<bar>c\<bar> \<noteq> \<infinity>"
+  shows "(a - b) * c = a * c - b * c"
+using assms
+by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
+
 
 subsection "Complete lattice"
 
@@ -4116,6 +4147,11 @@
     by (force simp: continuous_on_def mult_ac)
 qed (insert assms, auto simp: mono_def ereal_mult_right_mono)
 
+lemma Liminf_ereal_mult_left:
+  assumes "F \<noteq> bot" "(c::real) \<ge> 0"
+    shows "Liminf F (\<lambda>n. ereal c * f n) = ereal c * Liminf F f"
+using Liminf_ereal_mult_right[OF assms] by (subst (1 2) mult.commute)
+
 lemma Limsup_ereal_mult_left:
   assumes "F \<noteq> bot" "(c::real) \<ge> 0"
   shows   "Limsup F (\<lambda>n. ereal c * f n) = ereal c * Limsup F f"
--- a/src/HOL/Limits.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Limits.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -2392,7 +2392,7 @@
     by (rule LIMSEQ_imp_Suc) (simp add: True)
 qed
 
-lemma LIMSEQ_power_zero: "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
+lemma LIMSEQ_power_zero [tendsto_intros]: "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
   for x :: "'a::real_normed_algebra_1"
   apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
   by (simp add: Zfun_le norm_power_ineq tendsto_Zfun_iff)
--- a/src/HOL/Nonstandard_Analysis/CLim.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/CLim.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -11,7 +11,7 @@
 begin
 
 (*not in simpset?*)
-declare hypreal_epsilon_not_zero [simp]
+declare epsilon_not_zero [simp]
 
 (*??generalize*)
 lemma lemma_complex_mult_inverse_squared [simp]: "x \<noteq> 0 \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"
--- a/src/HOL/Nonstandard_Analysis/HDeriv.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -46,7 +46,7 @@
   shows "NSDERIV f x :> D \<Longrightarrow> NSDERIV f x :> E \<Longrightarrow> D = E"
 proof -
   have "\<exists>s. (s::'a star) \<in> Infinitesimal - {0}"
-    by (metis Diff_iff HDeriv.of_hypreal_eq_0_iff Infinitesimal_epsilon Infinitesimal_of_hypreal hypreal_epsilon_not_zero singletonD)
+    by (metis Diff_iff HDeriv.of_hypreal_eq_0_iff Infinitesimal_epsilon Infinitesimal_of_hypreal epsilon_not_zero singletonD)
   with assms show ?thesis
     by (meson approx_trans3 nsderiv_def star_of_approx_iff)
 qed
--- a/src/HOL/Nonstandard_Analysis/HLim.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/HLim.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -93,7 +93,7 @@
     have "star_of a + of_hypreal \<epsilon> \<approx> star_of a"
       by (simp add: approx_def)
     then show ?thesis
-      using hypreal_epsilon_not_zero that by (force simp add: NSLIM_def)
+      using epsilon_not_zero that by (force simp add: NSLIM_def)
   qed
   with assms show ?thesis by metis
 qed
@@ -151,7 +151,7 @@
     hnorm (starfun f x - star_of L) < star_of r"
   proof (rule exI, safe)
     show "0 < \<epsilon>"
-      by (rule hypreal_epsilon_gt_zero)
+      by (rule epsilon_gt_zero)
   next
     fix x
     assume neq: "x \<noteq> star_of a"
@@ -291,7 +291,7 @@
   have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
   proof (rule exI, safe)
     show "0 < \<epsilon>"
-      by (rule hypreal_epsilon_gt_zero)
+      by (rule epsilon_gt_zero)
   next
     fix x y :: "'a star"
     assume "hnorm (x - y) < \<epsilon>"
--- a/src/HOL/Nonstandard_Analysis/HLog.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/HLog.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -9,15 +9,6 @@
   imports HTranscendental
 begin
 
-
-(* should be in NSA.ML *)
-lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>"
-  by (simp add: epsilon_def star_n_zero_num star_n_le)
-
-lemma hpfinite_witness: "\<epsilon> \<in> {x. 0 \<le> x \<and> x \<in> HFinite}"
-  by auto
-
-
 definition powhr :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"  (infixr "powhr" 80)
   where [transfer_unfold]: "x powhr a = starfun2 (powr) x a"
 
@@ -39,7 +30,7 @@
 lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
   by transfer simp
 
-lemma powhr_divide: "\<And>a x y. 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powhr a = (x powhr a) / (y powhr a)"
+lemma powhr_divide: "\<And>a x y. 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> (x / y) powhr a = (x powhr a) / (y powhr a)"
   by transfer (rule powr_divide)
 
 lemma powhr_add: "\<And>a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
--- a/src/HOL/Nonstandard_Analysis/HyperDef.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -229,14 +229,17 @@
     by (auto simp: epsilon_def star_of_def star_n_eq_iff)
 qed
 
-lemma hypreal_epsilon_not_zero: "\<epsilon> \<noteq> 0"
+lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>"
+  by (simp add: epsilon_def star_n_zero_num star_n_le)
+
+lemma epsilon_not_zero: "\<epsilon> \<noteq> 0"
   using hypreal_of_real_not_eq_epsilon by force
 
-lemma hypreal_epsilon_inverse_omega: "\<epsilon> = inverse \<omega>"
+lemma epsilon_inverse_omega: "\<epsilon> = inverse \<omega>"
   by (simp add: epsilon_def omega_def star_n_inverse)
 
-lemma hypreal_epsilon_gt_zero: "0 < \<epsilon>"
-  by (simp add: hypreal_epsilon_inverse_omega)
+lemma epsilon_gt_zero: "0 < \<epsilon>"
+  by (simp add: epsilon_inverse_omega)
 
 
 subsection \<open>Embedding the Naturals into the Hyperreals\<close>
--- a/src/HOL/Nonstandard_Analysis/NSA.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -1592,7 +1592,7 @@
 
 lemma Infinitesimal_epsilon [simp]: "\<epsilon> \<in> Infinitesimal"
   by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega
-      simp add: hypreal_epsilon_inverse_omega)
+      simp add: epsilon_inverse_omega)
 
 lemma HFinite_epsilon [simp]: "\<epsilon> \<in> HFinite"
   by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
--- a/src/HOL/Nonstandard_Analysis/NSComplex.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSComplex.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -197,8 +197,8 @@
 lemma hIm_hcomplex_of_hypreal [simp]: "\<And>z. hIm (hcomplex_of_hypreal z) = 0"
   by transfer (rule Im_complex_of_real)
 
-lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: "hcomplex_of_hypreal \<epsilon> \<noteq> 0"
-  by (simp add: hypreal_epsilon_not_zero)
+lemma hcomplex_of_epsilon_not_zero [simp]: "hcomplex_of_hypreal \<epsilon> \<noteq> 0"
+  by (simp add: epsilon_not_zero)
 
 
 subsection \<open>\<open>HComplex\<close> theorems\<close>
--- a/src/HOL/NthRoot.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/NthRoot.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -268,10 +268,10 @@
   with assms show ?thesis by simp
 qed
 
-lemma real_root_decreasing: "0 < n \<Longrightarrow> n < N \<Longrightarrow> 1 \<le> x \<Longrightarrow> root N x \<le> root n x"
+lemma real_root_decreasing: "0 < n \<Longrightarrow> n \<le> N \<Longrightarrow> 1 \<le> x \<Longrightarrow> root N x \<le> root n x"
   by (auto simp add: order_le_less real_root_strict_decreasing)
 
-lemma real_root_increasing: "0 < n \<Longrightarrow> n < N \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> root n x \<le> root N x"
+lemma real_root_increasing: "0 < n \<Longrightarrow> n \<le> N \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> root n x \<le> root N x"
   by (auto simp add: order_le_less real_root_strict_increasing)
 
 
--- a/src/HOL/Power.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Power.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -54,12 +54,6 @@
 lemma power_mult: "a ^ (m * n) = (a ^ m) ^ n"
   by (induct n) (simp_all add: power_add)
 
-lemma power2_eq_square: "a\<^sup>2 = a * a"
-  by (simp add: numeral_2_eq_2)
-
-lemma power3_eq_cube: "a ^ 3 = a * a * a"
-  by (simp add: numeral_3_eq_3 mult.assoc)
-
 lemma power_even_eq: "a ^ (2 * n) = (a ^ n)\<^sup>2"
   by (subst mult.commute) (simp add: power_mult)
 
@@ -73,6 +67,15 @@
   by (simp only: numeral_Bit1 One_nat_def add_Suc_right add_0_right
       power_Suc power_add Let_def mult.assoc)
 
+lemma power2_eq_square: "a\<^sup>2 = a * a"
+  by (simp add: numeral_2_eq_2)
+
+lemma power3_eq_cube: "a ^ 3 = a * a * a"
+  by (simp add: numeral_3_eq_3 mult.assoc)
+
+lemma power4_eq_xxxx: "x^4 = x * x * x * x"
+  by (simp add: mult.assoc power_numeral_even)
+
 lemma funpow_times_power: "(times x ^^ f x) = times (x ^ f x)"
 proof (induct "f x" arbitrary: f)
   case 0
--- a/src/HOL/Real_Vector_Spaces.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -1981,14 +1981,12 @@
 lemma Cauchy_iff2: "Cauchy X \<longleftrightarrow> (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse (real (Suc j))))"
   by (simp only: metric_Cauchy_iff2 dist_real_def)
 
-lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
+lemma lim_1_over_n [tendsto_intros]: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
 proof (subst lim_sequentially, intro allI impI exI)
-  fix e :: real
-  assume e: "e > 0"
-  fix n :: nat
-  assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
+  fix e::real and n
+  assume e: "e > 0" 
   have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
-  also note n
+  also assume "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
   finally show "dist (1 / of_nat n :: 'a) 0 < e"
     using e by (simp add: divide_simps mult.commute norm_divide)
 qed
--- a/src/HOL/Series.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Series.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -585,19 +585,17 @@
 text \<open>Sum of a geometric progression.\<close>
 
 lemma geometric_sums:
-  assumes less_1: "norm c < 1"
+  assumes "norm c < 1"
   shows "(\<lambda>n. c^n) sums (1 / (1 - c))"
 proof -
-  from less_1 have neq_1: "c \<noteq> 1" by auto
-  then have neq_0: "c - 1 \<noteq> 0" by simp
-  from less_1 have lim_0: "(\<lambda>n. c^n) \<longlonglongrightarrow> 0"
-    by (rule LIMSEQ_power_zero)
+  have neq_0: "c - 1 \<noteq> 0"
+    using assms by auto
   then have "(\<lambda>n. c ^ n / (c - 1) - 1 / (c - 1)) \<longlonglongrightarrow> 0 / (c - 1) - 1 / (c - 1)"
-    using neq_0 by (intro tendsto_intros)
+    by (intro tendsto_intros assms)
   then have "(\<lambda>n. (c ^ n - 1) / (c - 1)) \<longlonglongrightarrow> 1 / (1 - c)"
     by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib)
-  then show "(\<lambda>n. c ^ n) sums (1 / (1 - c))"
-    by (simp add: sums_def geometric_sum neq_1)
+  with neq_0 show "(\<lambda>n. c ^ n) sums (1 / (1 - c))"
+    by (simp add: sums_def geometric_sum)
 qed
 
 lemma summable_geometric: "norm c < 1 \<Longrightarrow> summable (\<lambda>n. c^n)"
--- a/src/HOL/Set_Interval.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Set_Interval.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -1268,6 +1268,18 @@
   qed
 qed
 
+lemma UN_le_add_shift_strict:
+  "(\<Union>i<n::nat. M(i+k)) = (\<Union>i\<in>{k..<n+k}. M i)" (is "?A = ?B")
+proof
+  show "?B \<subseteq> ?A"
+  proof
+    fix x assume "x \<in> ?B"
+    then obtain i where i: "i \<in> {k..<n+k}" "x \<in> M(i)" by auto
+    then have "i - k < n \<and> x \<in> M((i-k) + k)" by auto
+    then show "x \<in> ?A" using UN_le_add_shift by blast
+  qed
+qed (fastforce)
+
 lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
   by (auto simp add: atLeast0LessThan)
 
--- a/src/HOL/Topological_Spaces.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Topological_Spaces.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -1633,6 +1633,39 @@
   "eventually P (nhds a) \<longleftrightarrow> (\<forall>f. f \<longlonglongrightarrow> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
   using eventually_nhds_within_iff_sequentially[of P a UNIV] by simp
 
+(*Thanks to Sébastien Gouëzel*)
+lemma Inf_as_limit:
+  fixes A::"'a::{linorder_topology, first_countable_topology, complete_linorder} set"
+  assumes "A \<noteq> {}"
+  shows "\<exists>u. (\<forall>n. u n \<in> A) \<and> u \<longlonglongrightarrow> Inf A"
+proof (cases "Inf A \<in> A")
+  case True
+  show ?thesis
+    by (rule exI[of _ "\<lambda>n. Inf A"], auto simp add: True)
+next
+  case False
+  obtain y where "y \<in> A" using assms by auto
+  then have "Inf A < y" using False Inf_lower less_le by auto
+  obtain F :: "nat \<Rightarrow> 'a set" where F: "\<And>i. open (F i)" "\<And>i. Inf A \<in> F i"
+                                       "\<And>u. (\<forall>n. u n \<in> F n) \<Longrightarrow> u \<longlonglongrightarrow> Inf A"
+    by (metis first_countable_topology_class.countable_basis)
+  define u where "u = (\<lambda>n. SOME z. z \<in> F n \<and> z \<in> A)"
+  have "\<exists>z. z \<in> U \<and> z \<in> A" if "Inf A \<in> U" "open U" for U
+  proof -
+    obtain b where "b > Inf A" "{Inf A ..<b} \<subseteq> U"
+      using open_right[OF \<open>open U\<close> \<open>Inf A \<in> U\<close> \<open>Inf A < y\<close>] by auto
+    obtain z where "z < b" "z \<in> A"
+      using \<open>Inf A < b\<close> Inf_less_iff by auto
+    then have "z \<in> {Inf A ..<b}"
+      by (simp add: Inf_lower)
+    then show ?thesis using \<open>z \<in> A\<close> \<open>{Inf A ..<b} \<subseteq> U\<close> by auto
+  qed
+  then have *: "u n \<in> F n \<and> u n \<in> A" for n
+    using \<open>Inf A \<in> F n\<close> \<open>open (F n)\<close> unfolding u_def by (metis (no_types, lifting) someI_ex)
+  then have "u \<longlonglongrightarrow> Inf A" using F(3) by simp
+  then show ?thesis using * by auto
+qed
+
 lemma tendsto_at_iff_sequentially:
   "(f \<longlongrightarrow> a) (at x within s) \<longleftrightarrow> (\<forall>X. (\<forall>i. X i \<in> s - {x}) \<longrightarrow> X \<longlonglongrightarrow> x \<longrightarrow> ((f \<circ> X) \<longlonglongrightarrow> a))"
   for f :: "'a::first_countable_topology \<Rightarrow> _"
--- a/src/HOL/Transcendental.thy	Thu Sep 19 16:38:05 2019 +0200
+++ b/src/HOL/Transcendental.thy	Thu Sep 19 16:38:32 2019 +0200
@@ -2461,7 +2461,7 @@
 lemma powr_non_neg[simp]: "\<not>a powr x < 0" for a x::real
   using powr_ge_pzero[of a x] by arith
 
-lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
+lemma powr_divide: "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
   for a b x :: real
   apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
   apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
@@ -2471,7 +2471,7 @@
   for a b x :: "'a::{ln,real_normed_field}"
   by (simp add: powr_def exp_add [symmetric] distrib_right)
 
-lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
+lemma powr_mult_base: "0 \<le> x \<Longrightarrow>x * x powr y = x powr (1 + y)"
   for x :: real
   by (auto simp: powr_add)
 
@@ -5314,6 +5314,26 @@
   "- (pi/2) \<le> x \<Longrightarrow> x \<le> pi/2 \<Longrightarrow> - (pi/2) \<le> y \<Longrightarrow> y \<le> pi/2 \<Longrightarrow> sin x = sin y \<Longrightarrow> x = y"
   by (metis arcsin_sin)
 
+lemma arcsin_le_iff:
+  assumes "x \<ge> -1" "x \<le> 1" "y \<ge> -pi/2" "y \<le> pi/2"
+  shows   "arcsin x \<le> y \<longleftrightarrow> x \<le> sin y"
+proof -
+  have "arcsin x \<le> y \<longleftrightarrow> sin (arcsin x) \<le> sin y"
+    using arcsin_bounded[of x] assms by (subst sin_mono_le_eq) auto
+  also from assms have "sin (arcsin x) = x" by simp
+  finally show ?thesis .
+qed
+
+lemma le_arcsin_iff:
+  assumes "x \<ge> -1" "x \<le> 1" "y \<ge> -pi/2" "y \<le> pi/2"
+  shows   "arcsin x \<ge> y \<longleftrightarrow> x \<ge> sin y"
+proof -
+  have "arcsin x \<ge> y \<longleftrightarrow> sin (arcsin x) \<ge> sin y"
+    using arcsin_bounded[of x] assms by (subst sin_mono_le_eq) auto
+  also from assms have "sin (arcsin x) = x" by simp
+  finally show ?thesis .
+qed
+
 lemma cos_mono_less_eq: "0 \<le> x \<Longrightarrow> x \<le> pi \<Longrightarrow> 0 \<le> y \<Longrightarrow> y \<le> pi \<Longrightarrow> cos x < cos y \<longleftrightarrow> y < x"
   by (meson cos_monotone_0_pi cos_monotone_0_pi_le leD le_less_linear)