--- 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>
--- 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
--- 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)
--- 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)