# HG changeset patch # User nipkow # Date 1566918531 -7200 # Node ID 6a2c982363e9819bb08fc60e9cfe2ef4eda7a14f # Parent 5549e686d6acb1475d9e8f52186a3f348dcb35ce moved lemmas diff -r 5549e686d6ac -r 6a2c982363e9 src/HOL/Analysis/Borel_Space.thy --- a/src/HOL/Analysis/Borel_Space.thy Sun Aug 25 22:17:24 2019 +0200 +++ b/src/HOL/Analysis/Borel_Space.thy Tue Aug 27 17:08:51 2019 +0200 @@ -244,20 +244,6 @@ shows "closed C \ A \ C \ A \ {} \ bdd_above A \ Sup A \ C" by (metis closure_contains_Sup closure_minimal subset_eq) -proposition deriv_nonneg_imp_mono: - assumes deriv: "\x. x \ {a..b} \ (g has_real_derivative g' x) (at x)" - assumes nonneg: "\x. x \ {a..b} \ g' x \ 0" - assumes ab: "a \ b" - shows "g a \ g b" -proof (cases "a < b") - assume "a < b" - from deriv have "\x. \x \ a; x \ b\ \ (g has_real_derivative g' x) (at x)" by simp - with MVT2[OF \a < b\] and deriv - obtain \ where \_ab: "\ > a" "\ < b" and g_ab: "g b - g a = (b - a) * g' \" by blast - from \_ab ab nonneg have "(b - a) * g' \ \ 0" by simp - with g_ab show ?thesis by simp -qed (insert ab, simp) - lemma continuous_interval_vimage_Int: assumes "continuous_on {a::real..b} g" and mono: "\x y. a \ x \ x \ y \ y \ b \ g x \ g y" assumes "a \ b" "(c::real) \ d" "{c..d} \ {g a..g b}" diff -r 5549e686d6ac -r 6a2c982363e9 src/HOL/Analysis/Derivative.thy --- a/src/HOL/Analysis/Derivative.thy Sun Aug 25 22:17:24 2019 +0200 +++ b/src/HOL/Analysis/Derivative.thy Tue Aug 27 17:08:51 2019 +0200 @@ -39,6 +39,15 @@ norm (f x' - f x - f'(x' - x)) / norm (x' - x) < e)" using has_derivative_within' [of f f' x UNIV] by simp +lemma has_derivative_componentwise_within: + "(f has_derivative f') (at a within S) \ + (\i \ Basis. ((\x. f x \ i) has_derivative (\x. f' x \ i)) (at a within S))" + apply (simp add: has_derivative_within) + apply (subst tendsto_componentwise_iff) + apply (simp add: bounded_linear_componentwise_iff [symmetric] ball_conj_distrib) + apply (simp add: algebra_simps) + done + lemma has_derivative_at_withinI: "(f has_derivative f') (at x) \ (f has_derivative f') (at x within s)" unfolding has_derivative_within' has_derivative_at' diff -r 5549e686d6ac -r 6a2c982363e9 src/HOL/Analysis/Measure_Space.thy --- a/src/HOL/Analysis/Measure_Space.thy Sun Aug 25 22:17:24 2019 +0200 +++ b/src/HOL/Analysis/Measure_Space.thy Tue Aug 27 17:08:51 2019 +0200 @@ -1184,9 +1184,6 @@ "(\N. N \ I \ AE x in M. P N x) \ countable I \ AE x in M. \N \ I. P N x" unfolding AE_ball_countable by simp -lemma pairwise_alt: "pairwise R S \ (\x\S. \y\S-{x}. R x y)" - by (auto simp add: pairwise_def) - lemma AE_pairwise: "countable F \ pairwise (\A B. AE x in M. R x A B) F \ (AE x in M. pairwise (R x) F)" unfolding pairwise_alt by (simp add: AE_ball_countable) diff -r 5549e686d6ac -r 6a2c982363e9 src/HOL/Analysis/Weierstrass_Theorems.thy --- a/src/HOL/Analysis/Weierstrass_Theorems.thy Sun Aug 25 22:17:24 2019 +0200 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Tue Aug 27 17:08:51 2019 +0200 @@ -1247,15 +1247,6 @@ done qed -lemma has_derivative_componentwise_within: - "(f has_derivative f') (at a within S) \ - (\i \ Basis. ((\x. f x \ i) has_derivative (\x. f' x \ i)) (at a within S))" - apply (simp add: has_derivative_within) - apply (subst tendsto_componentwise_iff) - apply (simp add: bounded_linear_componentwise_iff [symmetric] ball_conj_distrib) - apply (simp add: algebra_simps) - done - lemma differentiable_componentwise_within: "f differentiable (at a within S) \ (\i \ Basis. (\x. f x \ i) differentiable at a within S)" diff -r 5549e686d6ac -r 6a2c982363e9 src/HOL/Deriv.thy --- a/src/HOL/Deriv.thy Sun Aug 25 22:17:24 2019 +0200 +++ b/src/HOL/Deriv.thy Tue Aug 27 17:08:51 2019 +0200 @@ -1451,6 +1451,20 @@ finally show "f x < f y" by simp qed +proposition deriv_nonneg_imp_mono: + assumes deriv: "\x. x \ {a..b} \ (g has_real_derivative g' x) (at x)" + assumes nonneg: "\x. x \ {a..b} \ g' x \ 0" + assumes ab: "a \ b" + shows "g a \ g b" +proof (cases "a < b") + assume "a < b" + from deriv have "\x. \x \ a; x \ b\ \ (g has_real_derivative g' x) (at x)" by simp + with MVT2[OF \a < b\] and deriv + obtain \ where \_ab: "\ > a" "\ < b" and g_ab: "g b - g a = (b - a) * g' \" by blast + from \_ab ab nonneg have "(b - a) * g' \ \ 0" by simp + with g_ab show ?thesis by simp +qed (insert ab, simp) + subsubsection \A function is constant if its derivative is 0 over an interval.\ diff -r 5549e686d6ac -r 6a2c982363e9 src/HOL/Set.thy --- a/src/HOL/Set.thy Sun Aug 25 22:17:24 2019 +0200 +++ b/src/HOL/Set.thy Tue Aug 27 17:08:51 2019 +0200 @@ -1863,6 +1863,9 @@ definition pairwise :: "('a \ 'a \ bool) \ 'a set \ bool" where "pairwise R S \ (\x \ S. \y \ S. x \ y \ R x y)" +lemma pairwise_alt: "pairwise R S \ (\x\S. \y\S-{x}. R x y)" +by (auto simp add: pairwise_def) + lemma pairwise_trivial [simp]: "pairwise (\i j. j \ i) I" by (auto simp: pairwise_def)