# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1568733691 -3600
# Node ID ae2528273eeb8f2b5eedf24a19f917773d701d1d
# Parent  47258727fa42f4b562b7e7be68f067fe310f49dc
A couple of new theorems, stolen from AFP entries

diff -r 47258727fa42 -r ae2528273eeb src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Sep 17 12:36:04 2019 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Sep 17 16:21:31 2019 +0100
@@ -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>
 
diff -r 47258727fa42 -r ae2528273eeb src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Tue Sep 17 12:36:04 2019 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Tue Sep 17 16:21:31 2019 +0100
@@ -987,6 +987,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
diff -r 47258727fa42 -r ae2528273eeb src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Tue Sep 17 12:36:04 2019 +0100
+++ b/src/HOL/NthRoot.thy	Tue Sep 17 16:21:31 2019 +0100
@@ -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)
 
 
diff -r 47258727fa42 -r ae2528273eeb src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Sep 17 12:36:04 2019 +0100
+++ b/src/HOL/Transcendental.thy	Tue Sep 17 16:21:31 2019 +0100
@@ -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)