# HG changeset patch # User paulson # 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 \ 'a::euclidean_space" + assumes cont: "continuous_on {a + c..b + c} f" + shows "integral {a..b} (f \ (\x. x + c)) = integral {a + c..b + c} f" +proof (cases "a \ b") + case True + have "((\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 \Compute a double integral using iterated integrals and switching the order of integration\ 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 \ sets M" "B \ sets M" "A \ B \ null_sets M" + shows "emeasure M (A \ B) = emeasure M A + emeasure M B" +proof - + have "A \ B = A \ (B - A \ B)" by blast + also have "emeasure M \ = emeasure M A + emeasure M (B - A \ B)" + using assms by (subst plus_emeasure) auto + also have "emeasure M (B - A \ B) = emeasure M B" + using assms by (intro emeasure_Diff_null_set) auto + finally show ?thesis . +qed + subsection \The almost everywhere filter (i.e.\ quantifier)\ definition\<^marker>\tag important\ ae_filter :: "'a measure \ '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 \ n < N \ 1 \ x \ root N x \ root n x" +lemma real_root_decreasing: "0 < n \ n \ N \ 1 \ x \ root N x \ root n x" by (auto simp add: order_le_less real_root_strict_decreasing) -lemma real_root_increasing: "0 < n \ n < N \ 0 \ x \ x \ 1 \ root n x \ root N x" +lemma real_root_increasing: "0 < n \ n \ N \ 0 \ x \ x \ 1 \ root n x \ 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) \ x \ x \ pi/2 \ - (pi/2) \ y \ y \ pi/2 \ sin x = sin y \ x = y" by (metis arcsin_sin) +lemma arcsin_le_iff: + assumes "x \ -1" "x \ 1" "y \ -pi/2" "y \ pi/2" + shows "arcsin x \ y \ x \ sin y" +proof - + have "arcsin x \ y \ sin (arcsin x) \ 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 \ -1" "x \ 1" "y \ -pi/2" "y \ pi/2" + shows "arcsin x \ y \ x \ sin y" +proof - + have "arcsin x \ y \ sin (arcsin x) \ 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 \ x \ x \ pi \ 0 \ y \ y \ pi \ cos x < cos y \ y < x" by (meson cos_monotone_0_pi cos_monotone_0_pi_le leD le_less_linear)