diff -r 5b7c85586eb1 -r 38457af660bc src/HOL/Analysis/Convex.thy
--- 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"