--- 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}"
--- 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'
--- 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)
--- 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)"
--- 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>
--- 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)