# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1440008299 -3600
# Node ID 6a6f15d8fbc49acc612c9c2f1da77fbc5dd8bc61
# Parent  d94f3afd69b6dcead0fd6bf11f99f79234ac8a97
New material and fixes related to the forthcoming Stone-Weierstrass development

diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Filter.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -670,7 +670,7 @@
   "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
   by (simp add: at_top_def le_INF_iff le_principal)
 
-lemma eventually_sequentiallyI:
+lemma eventually_sequentiallyI [intro?]:
   assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
   shows "eventually P sequentially"
 using assms by (auto simp: eventually_sequentially)
diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Groups_Big.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -807,20 +807,10 @@
   case False thus ?thesis by simp
 qed
 
-lemma setsum_abs_ge_zero[iff]: 
+lemma setsum_abs_ge_zero[iff]:
   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
   shows "0 \<le> setsum (%i. abs(f i)) A"
-proof (cases "finite A")
-  case True
-  thus ?thesis
-  proof induct
-    case empty thus ?case by simp
-  next
-    case (insert x A) thus ?case by auto
-  qed
-next
-  case False thus ?thesis by simp
-qed
+  by (simp add: setsum_nonneg)
 
 lemma abs_setsum_abs[simp]: 
   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
@@ -931,6 +921,19 @@
   "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
   by (induct A rule: infinite_finite_induct) simp_all
 
+lemma setsum_pos2:
+    assumes "finite I" "i \<in> I" "0 < f i" "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i)"
+      shows "(0::'a::{ordered_ab_group_add,comm_monoid_add}) < setsum f I"
+proof -
+  have "0 \<le> setsum f (I-{i})"
+    using assms by (simp add: setsum_nonneg)
+  also have "... < setsum f (I-{i}) + f i"
+    using assms by auto
+  also have "... = setsum f I"
+    using assms by (simp add: setsum.remove)
+  finally show ?thesis .
+qed
+
 
 subsubsection \<open>Cardinality as special case of @{const setsum}\<close>
 
@@ -957,7 +960,7 @@
   using setsum.distrib[of f "\<lambda>_. 1" A] 
   by simp
 
-lemma setsum_bounded:
+lemma setsum_bounded_above:
   assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
   shows "setsum f A \<le> of_nat (card A) * K"
 proof (cases "finite A")
@@ -967,6 +970,23 @@
   case False thus ?thesis by simp
 qed
 
+lemma setsum_bounded_above_strict:
+  assumes "\<And>i. i\<in>A \<Longrightarrow> f i < (K::'a::{ordered_cancel_ab_semigroup_add,semiring_1})"
+          "card A > 0"
+  shows "setsum f A < of_nat (card A) * K"
+using assms setsum_strict_mono[where A=A and g = "%x. K"]
+by (simp add: card_gt_0_iff)
+
+lemma setsum_bounded_below:
+  assumes le: "\<And>i. i\<in>A \<Longrightarrow> (K::'a::{semiring_1, ordered_ab_semigroup_add}) \<le> f i"
+  shows "of_nat (card A) * K \<le> setsum f A"
+proof (cases "finite A")
+  case True
+  thus ?thesis using le setsum_mono[where K=A and f = "%x. K"] by simp
+next
+  case False thus ?thesis by simp
+qed
+
 lemma card_UN_disjoint:
   assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
     and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
@@ -1210,6 +1230,15 @@
   using assms by (induct A rule: infinite_finite_induct)
     (auto intro!: setprod_nonneg mult_mono)
 
+lemma (in linordered_semidom) setprod_mono_strict:
+    assumes"finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
+    shows "setprod f A < setprod g A"
+using assms 
+apply (induct A rule: finite_induct)
+apply (simp add: )
+apply (force intro: mult_strict_mono' setprod_nonneg)
+done
+
 lemma (in linordered_field) abs_setprod:
   "\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
   by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
@@ -1218,12 +1247,15 @@
   "finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = (1::nat))"
   by (induct A rule: finite_induct) simp_all
 
-lemma setprod_pos_nat:
-  "finite A \<Longrightarrow> (\<forall>a\<in>A. f a > (0::nat)) \<Longrightarrow> setprod f A > 0"
-  using setprod_zero_iff by (simp del: neq0_conv add: neq0_conv [symmetric])
-
 lemma setprod_pos_nat_iff [simp]:
   "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
   using setprod_zero_iff by (simp del:neq0_conv add:neq0_conv [symmetric])
 
+lemma setsum_nonneg_eq_0_iff:
+  fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
+  shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
+  apply (induct set: finite, simp)
+  apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
+  done
+
 end
diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/Hilbert_Choice.thy
--- a/src/HOL/Hilbert_Choice.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Hilbert_Choice.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -49,12 +49,16 @@
 text\<open>Easier to apply than @{text someI} because the conclusion has only one
 occurrence of @{term P}.\<close>
 lemma someI2: "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
-by (blast intro: someI)
+  by (blast intro: someI)
 
 text\<open>Easier to apply than @{text someI2} if the witness comes from an
 existential formula\<close>
+
 lemma someI2_ex: "[| \<exists>a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
-by (blast intro: someI2)
+  by (blast intro: someI2)
+
+lemma someI2_bex: "[| \<exists>a\<in>A. P a; !!x. x \<in> A \<and> P x ==> Q x |] ==> Q (SOME x. x \<in> A \<and> P x)"
+  by (blast intro: someI2)
 
 lemma some_equality [intro]:
      "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a"
@@ -102,7 +106,7 @@
 by (fast elim: someI)
 
 lemma dependent_nat_choice:
-  assumes  1: "\<exists>x. P 0 x" and 
+  assumes  1: "\<exists>x. P 0 x" and
            2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y"
   shows "\<exists>f. \<forall>n. P n (f n) \<and> Q n (f n) (f (Suc n))"
 proof (intro exI allI conjI)
@@ -263,7 +267,7 @@
 apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
 done
 
-lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A" 
+lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A"
 apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
 apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
 done
@@ -312,7 +316,7 @@
     unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
   ultimately have "range pick \<subseteq> S" by auto
   moreover
-  { fix n m                 
+  { fix n m
     have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
     with * have "pick n \<noteq> pick (n + Suc m)" by auto
   }
diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -317,7 +317,7 @@
 "m_s S X = (\<Sum> x \<in> X. m(S x))"
 
 lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X"
-by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded[OF h])
+by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded_above[OF h])
 
 fun m_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>o") where
 "m_o (Some S) X = m_s S X" |
diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -109,7 +109,7 @@
 "m_s S X = (\<Sum> x \<in> X. m(fun S x))"
 
 lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X"
-by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded[OF h])
+by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded_above[OF h])
 
 definition m_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>o") where
 "m_o opt X = (case opt of None \<Rightarrow> h * card X + 1 | Some S \<Rightarrow> m_s S X)"
diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Limits.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -1945,6 +1945,20 @@
     by auto
 qed
 
+lemma open_Collect_positive:
+ fixes f :: "'a::t2_space \<Rightarrow> real"
+ assumes f: "continuous_on s f"
+ shows "\<exists>A. open A \<and> A \<inter> s = {x\<in>s. 0 < f x}"
+ using continuous_on_open_invariant[THEN iffD1, OF f, rule_format, of "{0 <..}"]
+ by (auto simp: Int_def field_simps)
+
+lemma open_Collect_less_Int:
+ fixes f g :: "'a::t2_space \<Rightarrow> real"
+ assumes f: "continuous_on s f" and g: "continuous_on s g"
+ shows "\<exists>A. open A \<and> A \<inter> s = {x\<in>s. f x < g x}"
+ using open_Collect_positive[OF continuous_on_diff[OF g f]] by (simp add: field_simps)
+
+
 subsection \<open>Boundedness of continuous functions\<close>
 
 text\<open>By bisection, function continuous on closed interval is bounded above\<close>
diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -1226,7 +1226,7 @@
   then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` closure S = closure S)"
     using closure_subset by (auto simp add: closure_scaleR)
   then show ?thesis
-    using cone_iff[of "closure S"] by auto
+    using False cone_iff[of "closure S"] by auto
 qed
 
 
@@ -9545,4 +9545,216 @@
 apply simp
 done
 
+subsection\<open>The infimum of the distance between two sets\<close>
+
+definition setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
+  "setdist s t \<equiv>
+       (if s = {} \<or> t = {} then 0
+        else Inf {dist x y| x y. x \<in> s \<and> y \<in> t})"
+
+lemma setdist_empty1 [simp]: "setdist {} t = 0"
+  by (simp add: setdist_def)
+
+lemma setdist_empty2 [simp]: "setdist t {} = 0"
+  by (simp add: setdist_def)
+
+lemma setdist_pos_le: "0 \<le> setdist s t"
+  by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest)
+
+lemma le_setdistI:
+  assumes "s \<noteq> {}" "t \<noteq> {}" "\<And>x y. \<lbrakk>x \<in> s; y \<in> t\<rbrakk> \<Longrightarrow> d \<le> dist x y"
+    shows "d \<le> setdist s t"
+  using assms
+  by (auto simp: setdist_def Set.ex_in_conv [symmetric] intro: cInf_greatest)
+
+lemma setdist_le_dist: "\<lbrakk>x \<in> s; y \<in> t\<rbrakk> \<Longrightarrow> setdist s t \<le> dist x y"
+  unfolding setdist_def
+  by (auto intro!: bdd_belowI [where m=0] cInf_lower)
+
+lemma le_setdist_iff: 
+        "d \<le> setdist s t \<longleftrightarrow>
+        (\<forall>x \<in> s. \<forall>y \<in> t. d \<le> dist x y) \<and> (s = {} \<or> t = {} \<longrightarrow> d \<le> 0)"
+  apply (cases "s = {} \<or> t = {}")
+  apply (force simp add: setdist_def)
+  apply (intro iffI conjI)
+  using setdist_le_dist apply fastforce
+  apply (auto simp: intro: le_setdistI)
+  done
+
+lemma setdist_ltE: 
+  assumes "setdist s t < b" "s \<noteq> {}" "t \<noteq> {}"
+    obtains x y where "x \<in> s" "y \<in> t" "dist x y < b"
+using assms
+by (auto simp: not_le [symmetric] le_setdist_iff)
+
+lemma setdist_refl: "setdist s s = 0"
+  apply (cases "s = {}")
+  apply (force simp add: setdist_def)
+  apply (rule antisym [OF _ setdist_pos_le])
+  apply (metis all_not_in_conv dist_self setdist_le_dist)
+  done
+
+lemma setdist_sym: "setdist s t = setdist t s"
+  by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf])
+
+lemma setdist_triangle: "setdist s t \<le> setdist s {a} + setdist {a} t"
+proof (cases "s = {} \<or> t = {}")
+  case True then show ?thesis
+    using setdist_pos_le by fastforce
+next
+  case False
+  have "\<And>x. x \<in> s \<Longrightarrow> setdist s t - dist x a \<le> setdist {a} t" 
+    apply (rule le_setdistI, blast)
+    using False apply (fastforce intro: le_setdistI)
+    apply (simp add: algebra_simps)
+    apply (metis dist_commute dist_triangle_alt order_trans [OF setdist_le_dist])
+    done
+  then have "setdist s t - setdist {a} t \<le> setdist s {a}"
+    using False by (fastforce intro: le_setdistI)
+  then show ?thesis
+    by (simp add: algebra_simps)
+qed
+
+lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y"
+  by (simp add: setdist_def)
+
+lemma setdist_Lipschitz: "abs(setdist {x} s - setdist {y} s) \<le> dist x y"
+  apply (subst setdist_singletons [symmetric])
+  by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)
+
+lemma continuous_at_setdist: "continuous (at x) (\<lambda>y. (setdist {y} s))"
+  by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
+
+lemma continuous_on_setdist: "continuous_on t (\<lambda>y. (setdist {y} s))"
+  by (metis continuous_at_setdist continuous_at_imp_continuous_on)
+
+lemma uniformly_continuous_on_setdist: "uniformly_continuous_on t (\<lambda>y. (setdist {y} s))"
+  by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
+
+lemma setdist_subset_right: "\<lbrakk>t \<noteq> {}; t \<subseteq> u\<rbrakk> \<Longrightarrow> setdist s u \<le> setdist s t"
+  apply (cases "s = {} \<or> u = {}", force)
+  apply (auto simp: setdist_def intro!: bdd_belowI [where m=0] cInf_superset_mono)
+  done
+
+lemma setdist_subset_left: "\<lbrakk>s \<noteq> {}; s \<subseteq> t\<rbrakk> \<Longrightarrow> setdist t u \<le> setdist s u"
+  by (metis setdist_subset_right setdist_sym)
+
+lemma setdist_closure_1 [simp]: "setdist (closure s) t = setdist s t"
+proof (cases "s = {} \<or> t = {}")
+  case True then show ?thesis by force
+next
+  case False
+  { fix y
+    assume "y \<in> t"
+    have "continuous_on (closure s) (\<lambda>a. dist a y)"
+      by (auto simp: continuous_intros dist_norm)
+    then have *: "\<And>x. x \<in> closure s \<Longrightarrow> setdist s t \<le> dist x y"
+      apply (rule continuous_ge_on_closure)
+      apply assumption
+      apply (blast intro: setdist_le_dist `y \<in> t` )
+      done
+  } note * = this
+  show ?thesis
+    apply (rule antisym)
+     using False closure_subset apply (blast intro: setdist_subset_left)
+    using False *
+    apply (force simp add: closure_eq_empty intro!: le_setdistI)
+    done
+qed
+
+lemma setdist_closure_2 [simp]: "setdist t (closure s) = setdist t s"
+by (metis setdist_closure_1 setdist_sym)
+
+lemma setdist_compact_closed:
+  fixes s :: "'a::euclidean_space set"
+  assumes s: "compact s" and t: "closed t"
+      and "s \<noteq> {}" "t \<noteq> {}"
+    shows "\<exists>x \<in> s. \<exists>y \<in> t. dist x y = setdist s t"
+proof -
+  have "{x - y |x y. x \<in> s \<and> y \<in> t} \<noteq> {}"
+    using assms by blast
+  then
+  have "\<exists>x \<in> s. \<exists>y \<in> t. dist x y \<le> setdist s t"
+    using  distance_attains_inf [where a=0, OF compact_closed_differences [OF s t]] assms
+    apply (clarsimp simp: dist_norm le_setdist_iff, blast)
+    done
+  then show ?thesis
+    by (blast intro!: antisym [OF _ setdist_le_dist] )
+qed
+
+lemma setdist_closed_compact:
+  fixes s :: "'a::euclidean_space set"
+  assumes s: "closed s" and t: "compact t"
+      and "s \<noteq> {}" "t \<noteq> {}"
+    shows "\<exists>x \<in> s. \<exists>y \<in> t. dist x y = setdist s t"
+  using setdist_compact_closed [OF t s `t \<noteq> {}` `s \<noteq> {}`]
+  by (metis dist_commute setdist_sym)
+
+lemma setdist_eq_0I: "\<lbrakk>x \<in> s; x \<in> t\<rbrakk> \<Longrightarrow> setdist s t = 0"
+  by (metis antisym dist_self setdist_le_dist setdist_pos_le)
+
+lemma setdist_eq_0_compact_closed:
+  fixes s :: "'a::euclidean_space set"
+  assumes s: "compact s" and t: "closed t"
+    shows "setdist s t = 0 \<longleftrightarrow> s = {} \<or> t = {} \<or> s \<inter> t \<noteq> {}"
+  apply (cases "s = {} \<or> t = {}", force)
+  using setdist_compact_closed [OF s t]  
+  apply (force intro: setdist_eq_0I )
+  done
+
+corollary setdist_gt_0_compact_closed:
+  fixes s :: "'a::euclidean_space set"
+  assumes s: "compact s" and t: "closed t"
+    shows "setdist s t > 0 \<longleftrightarrow> (s \<noteq> {} \<and> t \<noteq> {} \<and> s \<inter> t = {})"
+  using setdist_pos_le [of s t] setdist_eq_0_compact_closed [OF assms]
+  by linarith
+
+lemma setdist_eq_0_closed_compact:
+  fixes s :: "'a::euclidean_space set"
+  assumes s: "closed s" and t: "compact t"
+    shows "setdist s t = 0 \<longleftrightarrow> s = {} \<or> t = {} \<or> s \<inter> t \<noteq> {}"
+  using setdist_eq_0_compact_closed [OF t s]
+  by (metis Int_commute setdist_sym)
+
+lemma setdist_eq_0_bounded:
+  fixes s :: "'a::euclidean_space set"
+  assumes "bounded s \<or> bounded t"
+    shows "setdist s t = 0 \<longleftrightarrow> s = {} \<or> t = {} \<or> closure s \<inter> closure t \<noteq> {}"
+  apply (cases "s = {} \<or> t = {}", force)
+  using setdist_eq_0_compact_closed [of "closure s" "closure t"] 
+        setdist_eq_0_closed_compact [of "closure s" "closure t"] assms 
+  apply (force simp add:  bounded_closure compact_eq_bounded_closed)
+  done
+
+lemma setdist_unique: 
+  "\<lbrakk>a \<in> s; b \<in> t; \<And>x y. x \<in> s \<and> y \<in> t ==> dist a b \<le> dist x y\<rbrakk>
+   \<Longrightarrow> setdist s t = dist a b"
+  by (force simp add: setdist_le_dist le_setdist_iff intro: antisym)
+
+lemma setdist_closest_point: 
+    "\<lbrakk>closed s; s \<noteq> {}\<rbrakk> \<Longrightarrow> setdist {a} s = dist a (closest_point s a)"
+  apply (rule setdist_unique)
+  using closest_point_le
+  apply (auto simp: closest_point_in_set)
+  done
+
+lemma setdist_eq_0_sing_1 [simp]: 
+  fixes s :: "'a::euclidean_space set"
+  shows "setdist {x} s = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
+by (auto simp: setdist_eq_0_bounded)
+
+lemma setdist_eq_0_sing_2 [simp]: 
+  fixes s :: "'a::euclidean_space set"
+  shows "setdist s {x} = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
+by (auto simp: setdist_eq_0_bounded)
+
+lemma setdist_sing_in_set:
+  fixes s :: "'a::euclidean_space set"
+  shows "x \<in> s \<Longrightarrow> setdist {x} s = 0"
+using closure_subset by force
+
+lemma setdist_le_sing: "x \<in> s ==> setdist s t \<le> setdist {x} t"
+  using setdist_subset_left by auto
+
+
 end
diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -92,6 +92,18 @@
     by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"])
 qed auto
 
+lemma (in euclidean_space) euclidean_representation_setsum_fun: 
+    "(\<lambda>x. \<Sum>b\<in>Basis. inner (f x) b *\<^sub>R b) = f"
+  by (rule ext) (simp add: euclidean_representation_setsum)
+
+lemma euclidean_isCont:
+  assumes "\<And>b. b \<in> Basis \<Longrightarrow> isCont (\<lambda>x. (inner (f x) b) *\<^sub>R b) x"
+    shows "isCont f x"
+  apply (subst euclidean_representation_setsum_fun [symmetric])
+  apply (rule isCont_setsum)
+  apply (blast intro: assms)
+  done
+
 lemma DIM_positive: "0 < DIM('a::euclidean_space)"
   by (simp add: card_gt_0_iff)
 
diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/Multivariate_Analysis/L2_Norm.thy
--- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -70,13 +70,6 @@
   apply (simp add: real_sqrt_mult setsum_nonneg)
   done
 
-lemma setsum_nonneg_eq_0_iff:
-  fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
-  shows "\<lbrakk>finite A; \<forall>x\<in>A. 0 \<le> f x\<rbrakk> \<Longrightarrow> setsum f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
-  apply (induct set: finite, simp)
-  apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
-  done
-
 lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
   unfolding setL2_def
   by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)
diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -562,25 +562,45 @@
   using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
   by (auto simp add: field_simps cong: conj_cong)
 
-lemma real_pow_lbound: "0 \<le> x \<Longrightarrow> 1 + real n * x \<le> (1 + x) ^ n"
+text{*Bernoulli's inequality*}
+lemma Bernoulli_inequality:
+  fixes x :: real
+  assumes "-1 \<le> x"
+    shows "1 + n * x \<le> (1 + x) ^ n"
 proof (induct n)
   case 0
   then show ?case by simp
 next
   case (Suc n)
-  then have h: "1 + real n * x \<le> (1 + x) ^ n"
-    by simp
-  from h have p: "1 \<le> (1 + x) ^ n"
-    using Suc.prems by simp
-  from h have "1 + real n * x + x \<le> (1 + x) ^ n + x"
+  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
+    by (simp add: algebra_simps)
+  also have "... = (1 + x) * (1 + n*x)"
+    by (auto simp: power2_eq_square algebra_simps  real_of_nat_Suc)
+  also have "... \<le> (1 + x) ^ Suc n"
+    using Suc.hyps assms mult_left_mono by fastforce
+  finally show ?case .
+qed
+
+lemma Bernoulli_inequality_even:
+  fixes x :: real
+  assumes "even n"
+    shows "1 + n * x \<le> (1 + x) ^ n"
+proof (cases "-1 \<le> x \<or> n=0")
+  case True
+  then show ?thesis
+    by (auto simp: Bernoulli_inequality)
+next
+  case False
+  then have "real n \<ge> 1"
     by simp
-  also have "\<dots> \<le> (1 + x) ^ Suc n"
-    apply (subst diff_le_0_iff_le[symmetric])
-    using mult_left_mono[OF p Suc.prems]
-    apply (simp add: field_simps)
-    done
-  finally show ?case
-    by (simp add: real_of_nat_Suc field_simps)
+  with False have "n * x \<le> -1"
+    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
+  then have "1 + n * x \<le> 0"
+    by auto
+  also have "... \<le> (1 + x) ^ n"
+    using assms
+    using zero_le_even_power by blast
+  finally show ?thesis .
 qed
 
 lemma real_arch_pow:
@@ -592,8 +612,8 @@
     by arith
   from reals_Archimedean3[OF x0, rule_format, of y]
   obtain n :: nat where n: "y < real n * (x - 1)" by metis
-  from x0 have x00: "x- 1 \<ge> 0" by arith
-  from real_pow_lbound[OF x00, of n] n
+  from x0 have x00: "x- 1 \<ge> -1" by arith
+  from Bernoulli_inequality[OF x00, of n] n
   have "y < x^n" by auto
   then show ?thesis by metis
 qed
@@ -1417,7 +1437,7 @@
   also have "(\<Sum>x\<in>P. \<Sum>b\<in>Basis. \<bar>f x \<bullet> b\<bar>) = (\<Sum>b\<in>Basis. \<Sum>x\<in>P. \<bar>f x \<bullet> b\<bar>)"
     by (rule setsum.commute)
   also have "\<dots> \<le> of_nat (card (Basis :: 'n set)) * (2 * e)"
-  proof (rule setsum_bounded)
+  proof (rule setsum_bounded_above)
     fix i :: 'n
     assume i: "i \<in> Basis"
     have "norm (\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le>
@@ -2828,7 +2848,7 @@
     unfolding real_of_nat_def
     apply (subst euclidean_inner)
     apply (subst power2_abs[symmetric])
-    apply (rule order_trans[OF setsum_bounded[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
+    apply (rule order_trans[OF setsum_bounded_above[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
     apply (auto simp add: power2_eq_square[symmetric])
     apply (subst power2_abs[symmetric])
     apply (rule power_mono)
diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -175,7 +175,7 @@
 lemma simple_path_eq_arc: "pathfinish g \<noteq> pathstart g \<Longrightarrow> (simple_path g = arc g)"
   by (simp add: arc_simple_path)
 
-lemma path_image_nonempty: "path_image g \<noteq> {}"
+lemma path_image_nonempty [simp]: "path_image g \<noteq> {}"
   unfolding path_image_def image_is_empty box_eq_empty
   by auto
 
diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -1602,7 +1602,7 @@
 lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
   unfolding closure_interior by simp
 
-lemma closure_eq_empty: "closure S = {} \<longleftrightarrow> S = {}"
+lemma closure_eq_empty [iff]: "closure S = {} \<longleftrightarrow> S = {}"
   using closure_empty closure_subset[of S]
   by blast
 
@@ -1826,7 +1826,7 @@
 
 text\<open>Interrelations between restricted and unrestricted limits.\<close>
 
-lemma Lim_at_imp_Lim_at_within: 
+lemma Lim_at_imp_Lim_at_within:
   "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
   by (metis order_refl filterlim_mono subset_UNIV at_le)
 
@@ -2831,12 +2831,12 @@
      (metis abs_le_D1 add.commute diff_le_eq)
 
 lemma bounded_inner_imp_bdd_above:
-  assumes "bounded s" 
+  assumes "bounded s"
     shows "bdd_above ((\<lambda>x. x \<bullet> a) ` s)"
 by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)
 
 lemma bounded_inner_imp_bdd_below:
-  assumes "bounded s" 
+  assumes "bounded s"
     shows "bdd_below ((\<lambda>x. x \<bullet> a) ` s)"
 by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)
 
@@ -4635,6 +4635,12 @@
 
 text\<open>Some simple consequential lemmas.\<close>
 
+lemma uniformly_continuous_onE:
+  assumes "uniformly_continuous_on s f" "0 < e"
+  obtains d where "d>0" "\<And>x x'. \<lbrakk>x\<in>s; x'\<in>s; dist x' x < d\<rbrakk> \<Longrightarrow> dist (f x') (f x) < e"
+using assms
+by (auto simp: uniformly_continuous_on_def)
+
 lemma uniformly_continuous_imp_continuous:
   "uniformly_continuous_on s f \<Longrightarrow> continuous_on s f"
   unfolding uniformly_continuous_on_def continuous_on_iff by blast
@@ -6166,6 +6172,19 @@
   finally show ?thesis .
 qed
 
+lemma continuous_on_closed_Collect_le:
+  fixes f g :: "'a::t2_space \<Rightarrow> real"
+  assumes f: "continuous_on s f" and g: "continuous_on s g" and s: "closed s"
+  shows "closed {x \<in> s. f x \<le> g x}"
+proof -
+  have "closed ((\<lambda>x. g x - f x) -` {0..} \<inter> s)"
+    using closed_real_atLeast continuous_on_diff [OF g f]
+    by (simp add: continuous_on_closed_vimage [OF s])
+  also have "((\<lambda>x. g x - f x) -` {0..} \<inter> s) = {x\<in>s. f x \<le> g x}"
+    by auto
+  finally show ?thesis .
+qed
+
 lemma continuous_at_inner: "continuous (at x) (inner a)"
   unfolding continuous_at by (intro tendsto_intros)
 
@@ -6194,6 +6213,25 @@
   shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
   by (simp add: Collect_ball_eq closed_INT closed_Collect_le)
 
+lemma continuous_le_on_closure:
+  fixes a::real
+  assumes f: "continuous_on (closure s) f"
+      and x: "x \<in> closure(s)"
+      and xlo: "\<And>x. x \<in> s ==> f(x) \<le> a"
+    shows "f(x) \<le> a"
+    using image_closure_subset [OF f] 
+  using image_closure_subset [OF f] closed_halfspace_le [of "1::real" a] assms
+  by force
+
+lemma continuous_ge_on_closure:
+  fixes a::real
+  assumes f: "continuous_on (closure s) f"
+      and x: "x \<in> closure(s)"
+      and xlo: "\<And>x. x \<in> s ==> f(x) \<ge> a"
+    shows "f(x) \<ge> a"
+  using image_closure_subset [OF f] closed_halfspace_ge [of a "1::real"] assms
+  by force
+
 text \<open>Openness of halfspaces.\<close>
 
 lemma open_halfspace_lt: "open {x. inner a x < b}"
@@ -7320,7 +7358,7 @@
 
 subsection \<open>Banach fixed point theorem (not really topological...)\<close>
 
-lemma banach_fix:
+theorem banach_fix:
   assumes s: "complete s" "s \<noteq> {}"
     and c: "0 \<le> c" "c < 1"
     and f: "(f ` s) \<subseteq> s"
@@ -7501,7 +7539,7 @@
 
 subsection \<open>Edelstein fixed point theorem\<close>
 
-lemma edelstein_fix:
+theorem edelstein_fix:
   fixes s :: "'a::metric_space set"
   assumes s: "compact s" "s \<noteq> {}"
     and gs: "(g ` s) \<subseteq> s"
diff -r d94f3afd69b6 -r 6a6f15d8fbc4 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Aug 19 15:40:59 2015 +0200
+++ b/src/HOL/Power.thy	Wed Aug 19 19:18:19 2015 +0100
@@ -762,6 +762,10 @@
   "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
   by (simp add: algebra_simps power2_eq_square mult_2_right)
 
+lemma (in comm_ring_1) power2_commute:
+  "(x - y)\<^sup>2 = (y - x)\<^sup>2"
+  by (simp add: algebra_simps power2_eq_square)
+
 
 text \<open>Simprules for comparisons where common factors can be cancelled.\<close>