# 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 \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> Sup A \<in> C"
   by (metis closure_contains_Sup closure_minimal subset_eq)
 
-proposition  deriv_nonneg_imp_mono:
-  assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
-  assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
-  assumes ab: "a \<le> b"
-  shows "g a \<le> g b"
-proof (cases "a < b")
-  assume "a < b"
-  from deriv have "\<And>x. \<lbrakk>x \<ge> a; x \<le> b\<rbrakk> \<Longrightarrow> (g has_real_derivative g' x) (at x)" by simp
-  with MVT2[OF \<open>a < b\<close>] and deriv
-    obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
-  from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 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: "\<And>x y. a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> b \<Longrightarrow> g x \<le> g y"
   assumes "a \<le> b" "(c::real) \<le> d" "{c..d} \<subseteq> {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) \<longleftrightarrow>
+    (\<forall>i \<in> Basis. ((\<lambda>x. f x \<bullet> i) has_derivative (\<lambda>x. f' x \<bullet> 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) \<Longrightarrow> (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 @@
   "(\<And>N. N \<in> I \<Longrightarrow> AE x in M. P N x) \<Longrightarrow> countable I \<Longrightarrow> AE x in M. \<forall>N \<in> I. P N x"
   unfolding AE_ball_countable by simp
 
-lemma pairwise_alt: "pairwise R S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S-{x}. R x y)"
-  by (auto simp add: pairwise_def)
-
 lemma AE_pairwise: "countable F \<Longrightarrow> pairwise (\<lambda>A B. AE x in M. R x A B) F \<longleftrightarrow> (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) \<longleftrightarrow>
-    (\<forall>i \<in> Basis. ((\<lambda>x. f x \<bullet> i) has_derivative (\<lambda>x. f' x \<bullet> 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) \<longleftrightarrow>
     (\<forall>i \<in> Basis. (\<lambda>x. f x \<bullet> 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: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
+  assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
+  assumes ab: "a \<le> b"
+  shows "g a \<le> g b"
+proof (cases "a < b")
+  assume "a < b"
+  from deriv have "\<And>x. \<lbrakk>x \<ge> a; x \<le> b\<rbrakk> \<Longrightarrow> (g has_real_derivative g' x) (at x)" by simp
+  with MVT2[OF \<open>a < b\<close>] and deriv
+    obtain \<xi> where \<xi>_ab: "\<xi> > a" "\<xi> < b" and g_ab: "g b - g a = (b - a) * g' \<xi>" by blast
+  from \<xi>_ab ab nonneg have "(b - a) * g' \<xi> \<ge> 0" by simp
+  with g_ab show ?thesis by simp
+qed (insert ab, simp)
+
 
 subsubsection \<open>A function is constant if its derivative is 0 over an interval.\<close>
 
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 \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
   where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)"
 
+lemma pairwise_alt: "pairwise R S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S-{x}. R x y)"
+by (auto simp add: pairwise_def)
+
 lemma pairwise_trivial [simp]: "pairwise (\<lambda>i j. j \<noteq> i) I"
   by (auto simp: pairwise_def)