author nipkow Fri, 06 Dec 2019 17:03:58 +0100 changeset 71244 38457af660bc parent 71243 5b7c85586eb1 child 71254 a9ad4a954cb7 child 71255 4258ee13f5d4
cleaning
 src/HOL/Analysis/Convex.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Convex_Euclidean_Space.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Path_Connected.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Polytope.thy file | annotate | diff | comparison | revisions src/HOL/Analysis/Starlike.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Analysis/Convex.thy	Fri Dec 06 14:36:11 2019 +0100
+++ b/src/HOL/Analysis/Convex.thy	Fri Dec 06 17:03:58 2019 +0100
@@ -562,36 +562,6 @@
using convex_translation[OF convex_scaling[OF assms], of a c] by auto
qed

-lemma pos_is_convex: "convex {0 :: real <..}"
-  unfolding convex_alt
-proof safe
-  fix y x \<mu> :: real
-  assume *: "y > 0" "x > 0" "\<mu> \<ge> 0" "\<mu> \<le> 1"
-  {
-    assume "\<mu> = 0"
-    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y = y"
-      by simp
-    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0"
-      using * by simp
-  }
-  moreover
-  {
-    assume "\<mu> = 1"
-    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0"
-      using * by simp
-  }
-  moreover
-  {
-    assume "\<mu> \<noteq> 1" "\<mu> \<noteq> 0"
-    then have "\<mu> > 0" "(1 - \<mu>) > 0"
-      using * by auto
-    then have "\<mu> *\<^sub>R x + (1 - \<mu>) *\<^sub>R y > 0"
-      using * by (auto simp: add_pos_pos)
-  }
-  ultimately show "(1 - \<mu>) *\<^sub>R y + \<mu> *\<^sub>R x > 0"
-    by fastforce
-qed
-
lemma convex_on_sum:
fixes a :: "'a \<Rightarrow> real"
and y :: "'a \<Rightarrow> 'b::real_vector"
@@ -923,7 +893,7 @@
unfolding inverse_eq_divide by (auto simp: mult.assoc)
have f''_ge0: "\<And>z::real. z > 0 \<Longrightarrow> 1 / (ln b * z * z) \<ge> 0"
using \<open>b > 1\<close> by (auto intro!: less_imp_le)
-  from f''_ge0_imp_convex[OF pos_is_convex, unfolded greaterThan_iff, OF f' f''0 f''_ge0]
+  from f''_ge0_imp_convex[OF convex_real_interval(3), unfolded greaterThan_iff, OF f' f''0 f''_ge0]
show ?thesis
by auto
qed
@@ -1049,12 +1019,6 @@
shows "\<lbrakk>linear f; inj f\<rbrakk> \<Longrightarrow> convex (f ` s) \<longleftrightarrow> convex s"
by (metis (no_types) convex_linear_image convex_linear_vimage inj_vimage_image_eq)

-lemma fst_linear: "linear fst"
-  unfolding linear_iff by (simp add: algebra_simps)
-
-lemma snd_linear: "linear snd"
-  unfolding linear_iff by (simp add: algebra_simps)
-
lemma fst_snd_linear: "linear (\<lambda>(x,y). x + y)"
unfolding linear_iff by (simp add: algebra_simps)

@@ -1284,10 +1248,6 @@

subsection\<^marker>\<open>tag unimportant\<close> \<open>Connectedness of convex sets\<close>

-lemma connectedD:
-  "connected S \<Longrightarrow> open A \<Longrightarrow> open B \<Longrightarrow> S \<subseteq> A \<union> B \<Longrightarrow> A \<inter> B \<inter> S = {} \<Longrightarrow> A \<inter> S = {} \<or> B \<inter> S = {}"
-  by (rule Topological_Spaces.topological_space_class.connectedD)
-
lemma convex_connected:
fixes S :: "'a::real_normed_vector set"
assumes "convex S"```
```--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Dec 06 14:36:11 2019 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Fri Dec 06 17:03:58 2019 +0100
@@ -180,9 +180,6 @@
shows "rel_interior S = S"
by (metis assms interior_eq interior_subset_rel_interior rel_interior_subset set_eq_subset)

-lemma interior_ball [simp]: "interior (ball x e) = ball x e"
-
lemma interior_rel_interior_gen:
fixes S :: "'n::euclidean_space set"
shows "interior S = (if aff_dim S = int(DIM('n)) then rel_interior S else {})"
@@ -1200,16 +1197,13 @@
lemma closest_point_exists:
assumes "closed S"
and "S \<noteq> {}"
-  shows "closest_point S a \<in> S"
+  shows closest_point_in_set: "closest_point S a \<in> S"
and "\<forall>y\<in>S. dist a (closest_point S a) \<le> dist a y"
unfolding closest_point_def
apply(rule_tac[!] someI2_ex)
apply (auto intro: distance_attains_inf[OF assms(1,2), of a])
done

-lemma closest_point_in_set: "closed S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> closest_point S a \<in> S"
-  by (meson closest_point_exists)
-
lemma closest_point_le: "closed S \<Longrightarrow> x \<in> S \<Longrightarrow> dist a (closest_point S a) \<le> dist a x"
using closest_point_exists[of S] by auto
```
```--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Dec 06 14:36:11 2019 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Fri Dec 06 17:03:58 2019 +0100
@@ -1999,7 +1999,7 @@
using diff_f
apply (intro differentiable_chain_within linear_imp_differentiable [OF \<open>linear drop\<close>]
-             linear_imp_differentiable [OF fst_linear])
+             linear_imp_differentiable [OF linear_fst])
apply (force simp: image_comp o_def)
done
have "f = (f o fst o drop o (\<lambda>x. lift (x, 0)))"```
```--- a/src/HOL/Analysis/Path_Connected.thy	Fri Dec 06 14:36:11 2019 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy	Fri Dec 06 17:03:58 2019 +0100
@@ -2910,7 +2910,7 @@
have "T \<inter> \<Union>(B - {T}) = {}" using \<open>T \<in> B\<close> \<open>pairwise disjnt B\<close>
by (auto simp: pairwise_def disjnt_def)
then have 4: "T \<inter> \<Union>(B - {T}) \<inter> S = {}" by auto
-  from connectedD [OF \<open>connected S\<close> 1 2 3 4]
+  from connectedD [OF \<open>connected S\<close> 1 2 4 3]
have "S \<inter> \<Union>(B-{T}) = {}"
by (auto simp: Int_commute \<open>S \<inter> T \<noteq> {}\<close>)
with \<open>T \<in> B\<close> have "S \<subseteq> T"```
```--- a/src/HOL/Analysis/Polytope.thy	Fri Dec 06 14:36:11 2019 +0100
+++ b/src/HOL/Analysis/Polytope.thy	Fri Dec 06 17:03:58 2019 +0100
@@ -545,7 +545,7 @@
have "convex c"
using c by (metis face_of_imp_convex)
have conv: "convex (fst ` c)" "convex (snd ` c)"
-      by (simp_all add: \<open>convex c\<close> convex_linear_image fst_linear snd_linear)
+      by (simp_all add: \<open>convex c\<close> convex_linear_image linear_fst linear_snd)
have fstab: "a \<in> fst ` c \<and> b \<in> fst ` c"
if "a \<in> S" "b \<in> S" "x \<in> open_segment a b" "(x,x') \<in> c" for a b x x'
proof -
@@ -567,7 +567,7 @@
have snd: "snd ` c face_of S'"
by (force simp: face_of_def 1 conv sndab)
have cc: "rel_interior c \<subseteq> rel_interior (fst ` c) \<times> rel_interior (snd ` c)"
-      by (force simp: face_of_Times rel_interior_Times conv fst snd \<open>convex c\<close> fst_linear snd_linear rel_interior_convex_linear_image [symmetric])
+      by (force simp: face_of_Times rel_interior_Times conv fst snd \<open>convex c\<close> linear_fst linear_snd rel_interior_convex_linear_image [symmetric])
have "c = fst ` c \<times> snd ` c"
apply (rule face_of_eq [OF c])
apply (simp_all add: face_of_Times rel_interior_Times conv fst snd)```
```--- a/src/HOL/Analysis/Starlike.thy	Fri Dec 06 14:36:11 2019 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Fri Dec 06 17:03:58 2019 +0100
@@ -1830,13 +1830,13 @@
then have "fst -` rel_interior S \<noteq> {}"
using fst_vimage_eq_Times[of "rel_interior S"] by auto
then have "rel_interior ((fst :: 'n * 'm \<Rightarrow> 'n) -` S) = fst -` rel_interior S"
-      using fst_linear \<open>convex S\<close> rel_interior_convex_linear_preimage[of fst S] by auto
+      using linear_fst \<open>convex S\<close> rel_interior_convex_linear_preimage[of fst S] by auto
then have s: "rel_interior (S \<times> (UNIV :: 'm set)) = rel_interior S \<times> UNIV"
from ri have "snd -` rel_interior T \<noteq> {}"
using snd_vimage_eq_Times[of "rel_interior T"] by auto
then have "rel_interior ((snd :: 'n * 'm \<Rightarrow> 'm) -` T) = snd -` rel_interior T"
-      using snd_linear \<open>convex T\<close> rel_interior_convex_linear_preimage[of snd T] by auto
+      using linear_snd \<open>convex T\<close> rel_interior_convex_linear_preimage[of snd T] by auto
then have t: "rel_interior ((UNIV :: 'n set) \<times> T) = UNIV \<times> rel_interior T"
from s t have *: "rel_interior (S \<times> (UNIV :: 'm set)) \<inter> rel_interior ((UNIV :: 'n set) \<times> T) =
@@ -1951,7 +1951,7 @@
then have "fst ` S = {y. f y \<noteq> {}}"
unfolding fst_def using assms by auto
then have h1: "fst ` rel_interior S = rel_interior {y. f y \<noteq> {}}"
-    using rel_interior_convex_linear_image[of fst S] assms fst_linear by auto
+    using rel_interior_convex_linear_image[of fst S] assms linear_fst by auto
{
fix y
assume "y \<in> rel_interior {y. f y \<noteq> {}}"
@@ -1977,7 +1977,7 @@
then have "snd ` (S \<inter> fst -` {y}) = f y"
using assms by auto
then have ***: "rel_interior (f y) = snd ` rel_interior (S \<inter> fst -` {y})"
-      using rel_interior_convex_linear_image[of snd "S \<inter> fst -` {y}"] snd_linear conv
+      using rel_interior_convex_linear_image[of snd "S \<inter> fst -` {y}"] linear_snd conv
by auto
{
fix z```