New material and fixes related to the forthcoming Stone-Weierstrass development
authorpaulson <lp15@cam.ac.uk>
Wed Aug 19 19:18:19 2015 +0100 (2015-08-19)
changeset 609746a6f15d8fbc4
parent 60973 d94f3afd69b6
child 60980 213bae1c0757
New material and fixes related to the forthcoming Stone-Weierstrass development
src/HOL/Filter.thy
src/HOL/Groups_Big.thy
src/HOL/Hilbert_Choice.thy
src/HOL/IMP/Abs_Int0.thy
src/HOL/IMP/Abs_Int1.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/L2_Norm.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Path_Connected.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Filter.thy	Wed Aug 19 15:40:59 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Wed Aug 19 19:18:19 2015 +0100
     1.3 @@ -670,7 +670,7 @@
     1.4    "F \<le> sequentially \<longleftrightarrow> (\<forall>N. eventually (\<lambda>n. N \<le> n) F)"
     1.5    by (simp add: at_top_def le_INF_iff le_principal)
     1.6  
     1.7 -lemma eventually_sequentiallyI:
     1.8 +lemma eventually_sequentiallyI [intro?]:
     1.9    assumes "\<And>x. c \<le> x \<Longrightarrow> P x"
    1.10    shows "eventually P sequentially"
    1.11  using assms by (auto simp: eventually_sequentially)
     2.1 --- a/src/HOL/Groups_Big.thy	Wed Aug 19 15:40:59 2015 +0200
     2.2 +++ b/src/HOL/Groups_Big.thy	Wed Aug 19 19:18:19 2015 +0100
     2.3 @@ -807,20 +807,10 @@
     2.4    case False thus ?thesis by simp
     2.5  qed
     2.6  
     2.7 -lemma setsum_abs_ge_zero[iff]: 
     2.8 +lemma setsum_abs_ge_zero[iff]:
     2.9    fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
    2.10    shows "0 \<le> setsum (%i. abs(f i)) A"
    2.11 -proof (cases "finite A")
    2.12 -  case True
    2.13 -  thus ?thesis
    2.14 -  proof induct
    2.15 -    case empty thus ?case by simp
    2.16 -  next
    2.17 -    case (insert x A) thus ?case by auto
    2.18 -  qed
    2.19 -next
    2.20 -  case False thus ?thesis by simp
    2.21 -qed
    2.22 +  by (simp add: setsum_nonneg)
    2.23  
    2.24  lemma abs_setsum_abs[simp]: 
    2.25    fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
    2.26 @@ -931,6 +921,19 @@
    2.27    "(\<And>a. a \<in> A \<Longrightarrow> d dvd f a) \<Longrightarrow> d dvd setsum f A"
    2.28    by (induct A rule: infinite_finite_induct) simp_all
    2.29  
    2.30 +lemma setsum_pos2:
    2.31 +    assumes "finite I" "i \<in> I" "0 < f i" "(\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i)"
    2.32 +      shows "(0::'a::{ordered_ab_group_add,comm_monoid_add}) < setsum f I"
    2.33 +proof -
    2.34 +  have "0 \<le> setsum f (I-{i})"
    2.35 +    using assms by (simp add: setsum_nonneg)
    2.36 +  also have "... < setsum f (I-{i}) + f i"
    2.37 +    using assms by auto
    2.38 +  also have "... = setsum f I"
    2.39 +    using assms by (simp add: setsum.remove)
    2.40 +  finally show ?thesis .
    2.41 +qed
    2.42 +
    2.43  
    2.44  subsubsection \<open>Cardinality as special case of @{const setsum}\<close>
    2.45  
    2.46 @@ -957,7 +960,7 @@
    2.47    using setsum.distrib[of f "\<lambda>_. 1" A] 
    2.48    by simp
    2.49  
    2.50 -lemma setsum_bounded:
    2.51 +lemma setsum_bounded_above:
    2.52    assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{semiring_1, ordered_ab_semigroup_add})"
    2.53    shows "setsum f A \<le> of_nat (card A) * K"
    2.54  proof (cases "finite A")
    2.55 @@ -967,6 +970,23 @@
    2.56    case False thus ?thesis by simp
    2.57  qed
    2.58  
    2.59 +lemma setsum_bounded_above_strict:
    2.60 +  assumes "\<And>i. i\<in>A \<Longrightarrow> f i < (K::'a::{ordered_cancel_ab_semigroup_add,semiring_1})"
    2.61 +          "card A > 0"
    2.62 +  shows "setsum f A < of_nat (card A) * K"
    2.63 +using assms setsum_strict_mono[where A=A and g = "%x. K"]
    2.64 +by (simp add: card_gt_0_iff)
    2.65 +
    2.66 +lemma setsum_bounded_below:
    2.67 +  assumes le: "\<And>i. i\<in>A \<Longrightarrow> (K::'a::{semiring_1, ordered_ab_semigroup_add}) \<le> f i"
    2.68 +  shows "of_nat (card A) * K \<le> setsum f A"
    2.69 +proof (cases "finite A")
    2.70 +  case True
    2.71 +  thus ?thesis using le setsum_mono[where K=A and f = "%x. K"] by simp
    2.72 +next
    2.73 +  case False thus ?thesis by simp
    2.74 +qed
    2.75 +
    2.76  lemma card_UN_disjoint:
    2.77    assumes "finite I" and "\<forall>i\<in>I. finite (A i)"
    2.78      and "\<forall>i\<in>I. \<forall>j\<in>I. i \<noteq> j \<longrightarrow> A i \<inter> A j = {}"
    2.79 @@ -1210,6 +1230,15 @@
    2.80    using assms by (induct A rule: infinite_finite_induct)
    2.81      (auto intro!: setprod_nonneg mult_mono)
    2.82  
    2.83 +lemma (in linordered_semidom) setprod_mono_strict:
    2.84 +    assumes"finite A" "\<forall>i\<in>A. 0 \<le> f i \<and> f i < g i" "A \<noteq> {}"
    2.85 +    shows "setprod f A < setprod g A"
    2.86 +using assms 
    2.87 +apply (induct A rule: finite_induct)
    2.88 +apply (simp add: )
    2.89 +apply (force intro: mult_strict_mono' setprod_nonneg)
    2.90 +done
    2.91 +
    2.92  lemma (in linordered_field) abs_setprod:
    2.93    "\<bar>setprod f A\<bar> = (\<Prod>x\<in>A. \<bar>f x\<bar>)"
    2.94    by (induct A rule: infinite_finite_induct) (simp_all add: abs_mult)
    2.95 @@ -1218,12 +1247,15 @@
    2.96    "finite A \<Longrightarrow> setprod f A = 1 \<longleftrightarrow> (\<forall>a\<in>A. f a = (1::nat))"
    2.97    by (induct A rule: finite_induct) simp_all
    2.98  
    2.99 -lemma setprod_pos_nat:
   2.100 -  "finite A \<Longrightarrow> (\<forall>a\<in>A. f a > (0::nat)) \<Longrightarrow> setprod f A > 0"
   2.101 -  using setprod_zero_iff by (simp del: neq0_conv add: neq0_conv [symmetric])
   2.102 -
   2.103  lemma setprod_pos_nat_iff [simp]:
   2.104    "finite A \<Longrightarrow> setprod f A > 0 \<longleftrightarrow> (\<forall>a\<in>A. f a > (0::nat))"
   2.105    using setprod_zero_iff by (simp del:neq0_conv add:neq0_conv [symmetric])
   2.106  
   2.107 +lemma setsum_nonneg_eq_0_iff:
   2.108 +  fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
   2.109 +  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)"
   2.110 +  apply (induct set: finite, simp)
   2.111 +  apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
   2.112 +  done
   2.113 +
   2.114  end
     3.1 --- a/src/HOL/Hilbert_Choice.thy	Wed Aug 19 15:40:59 2015 +0200
     3.2 +++ b/src/HOL/Hilbert_Choice.thy	Wed Aug 19 19:18:19 2015 +0100
     3.3 @@ -49,12 +49,16 @@
     3.4  text\<open>Easier to apply than @{text someI} because the conclusion has only one
     3.5  occurrence of @{term P}.\<close>
     3.6  lemma someI2: "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
     3.7 -by (blast intro: someI)
     3.8 +  by (blast intro: someI)
     3.9  
    3.10  text\<open>Easier to apply than @{text someI2} if the witness comes from an
    3.11  existential formula\<close>
    3.12 +
    3.13  lemma someI2_ex: "[| \<exists>a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
    3.14 -by (blast intro: someI2)
    3.15 +  by (blast intro: someI2)
    3.16 +
    3.17 +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)"
    3.18 +  by (blast intro: someI2)
    3.19  
    3.20  lemma some_equality [intro]:
    3.21       "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a"
    3.22 @@ -102,7 +106,7 @@
    3.23  by (fast elim: someI)
    3.24  
    3.25  lemma dependent_nat_choice:
    3.26 -  assumes  1: "\<exists>x. P 0 x" and 
    3.27 +  assumes  1: "\<exists>x. P 0 x" and
    3.28             2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y"
    3.29    shows "\<exists>f. \<forall>n. P n (f n) \<and> Q n (f n) (f (Suc n))"
    3.30  proof (intro exI allI conjI)
    3.31 @@ -263,7 +267,7 @@
    3.32  apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
    3.33  done
    3.34  
    3.35 -lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A" 
    3.36 +lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A"
    3.37  apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
    3.38  apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
    3.39  done
    3.40 @@ -312,7 +316,7 @@
    3.41      unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
    3.42    ultimately have "range pick \<subseteq> S" by auto
    3.43    moreover
    3.44 -  { fix n m                 
    3.45 +  { fix n m
    3.46      have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
    3.47      with * have "pick n \<noteq> pick (n + Suc m)" by auto
    3.48    }
     4.1 --- a/src/HOL/IMP/Abs_Int0.thy	Wed Aug 19 15:40:59 2015 +0200
     4.2 +++ b/src/HOL/IMP/Abs_Int0.thy	Wed Aug 19 19:18:19 2015 +0100
     4.3 @@ -317,7 +317,7 @@
     4.4  "m_s S X = (\<Sum> x \<in> X. m(S x))"
     4.5  
     4.6  lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X"
     4.7 -by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded[OF h])
     4.8 +by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded_above[OF h])
     4.9  
    4.10  fun m_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>o") where
    4.11  "m_o (Some S) X = m_s S X" |
     5.1 --- a/src/HOL/IMP/Abs_Int1.thy	Wed Aug 19 15:40:59 2015 +0200
     5.2 +++ b/src/HOL/IMP/Abs_Int1.thy	Wed Aug 19 19:18:19 2015 +0100
     5.3 @@ -109,7 +109,7 @@
     5.4  "m_s S X = (\<Sum> x \<in> X. m(fun S x))"
     5.5  
     5.6  lemma m_s_h: "finite X \<Longrightarrow> m_s S X \<le> h * card X"
     5.7 -by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded[OF h])
     5.8 +by(simp add: m_s_def) (metis mult.commute of_nat_id setsum_bounded_above[OF h])
     5.9  
    5.10  definition m_o :: "'av st option \<Rightarrow> vname set \<Rightarrow> nat" ("m\<^sub>o") where
    5.11  "m_o opt X = (case opt of None \<Rightarrow> h * card X + 1 | Some S \<Rightarrow> m_s S X)"
     6.1 --- a/src/HOL/Limits.thy	Wed Aug 19 15:40:59 2015 +0200
     6.2 +++ b/src/HOL/Limits.thy	Wed Aug 19 19:18:19 2015 +0100
     6.3 @@ -1945,6 +1945,20 @@
     6.4      by auto
     6.5  qed
     6.6  
     6.7 +lemma open_Collect_positive:
     6.8 + fixes f :: "'a::t2_space \<Rightarrow> real"
     6.9 + assumes f: "continuous_on s f"
    6.10 + shows "\<exists>A. open A \<and> A \<inter> s = {x\<in>s. 0 < f x}"
    6.11 + using continuous_on_open_invariant[THEN iffD1, OF f, rule_format, of "{0 <..}"]
    6.12 + by (auto simp: Int_def field_simps)
    6.13 +
    6.14 +lemma open_Collect_less_Int:
    6.15 + fixes f g :: "'a::t2_space \<Rightarrow> real"
    6.16 + assumes f: "continuous_on s f" and g: "continuous_on s g"
    6.17 + shows "\<exists>A. open A \<and> A \<inter> s = {x\<in>s. f x < g x}"
    6.18 + using open_Collect_positive[OF continuous_on_diff[OF g f]] by (simp add: field_simps)
    6.19 +
    6.20 +
    6.21  subsection \<open>Boundedness of continuous functions\<close>
    6.22  
    6.23  text\<open>By bisection, function continuous on closed interval is bounded above\<close>
     7.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 19 15:40:59 2015 +0200
     7.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 19 19:18:19 2015 +0100
     7.3 @@ -1226,7 +1226,7 @@
     7.4    then have "0 \<in> closure S \<and> (\<forall>c. c > 0 \<longrightarrow> op *\<^sub>R c ` closure S = closure S)"
     7.5      using closure_subset by (auto simp add: closure_scaleR)
     7.6    then show ?thesis
     7.7 -    using cone_iff[of "closure S"] by auto
     7.8 +    using False cone_iff[of "closure S"] by auto
     7.9  qed
    7.10  
    7.11  
    7.12 @@ -9545,4 +9545,216 @@
    7.13  apply simp
    7.14  done
    7.15  
    7.16 +subsection\<open>The infimum of the distance between two sets\<close>
    7.17 +
    7.18 +definition setdist :: "'a::metric_space set \<Rightarrow> 'a set \<Rightarrow> real" where
    7.19 +  "setdist s t \<equiv>
    7.20 +       (if s = {} \<or> t = {} then 0
    7.21 +        else Inf {dist x y| x y. x \<in> s \<and> y \<in> t})"
    7.22 +
    7.23 +lemma setdist_empty1 [simp]: "setdist {} t = 0"
    7.24 +  by (simp add: setdist_def)
    7.25 +
    7.26 +lemma setdist_empty2 [simp]: "setdist t {} = 0"
    7.27 +  by (simp add: setdist_def)
    7.28 +
    7.29 +lemma setdist_pos_le: "0 \<le> setdist s t"
    7.30 +  by (auto simp: setdist_def ex_in_conv [symmetric] intro: cInf_greatest)
    7.31 +
    7.32 +lemma le_setdistI:
    7.33 +  assumes "s \<noteq> {}" "t \<noteq> {}" "\<And>x y. \<lbrakk>x \<in> s; y \<in> t\<rbrakk> \<Longrightarrow> d \<le> dist x y"
    7.34 +    shows "d \<le> setdist s t"
    7.35 +  using assms
    7.36 +  by (auto simp: setdist_def Set.ex_in_conv [symmetric] intro: cInf_greatest)
    7.37 +
    7.38 +lemma setdist_le_dist: "\<lbrakk>x \<in> s; y \<in> t\<rbrakk> \<Longrightarrow> setdist s t \<le> dist x y"
    7.39 +  unfolding setdist_def
    7.40 +  by (auto intro!: bdd_belowI [where m=0] cInf_lower)
    7.41 +
    7.42 +lemma le_setdist_iff: 
    7.43 +        "d \<le> setdist s t \<longleftrightarrow>
    7.44 +        (\<forall>x \<in> s. \<forall>y \<in> t. d \<le> dist x y) \<and> (s = {} \<or> t = {} \<longrightarrow> d \<le> 0)"
    7.45 +  apply (cases "s = {} \<or> t = {}")
    7.46 +  apply (force simp add: setdist_def)
    7.47 +  apply (intro iffI conjI)
    7.48 +  using setdist_le_dist apply fastforce
    7.49 +  apply (auto simp: intro: le_setdistI)
    7.50 +  done
    7.51 +
    7.52 +lemma setdist_ltE: 
    7.53 +  assumes "setdist s t < b" "s \<noteq> {}" "t \<noteq> {}"
    7.54 +    obtains x y where "x \<in> s" "y \<in> t" "dist x y < b"
    7.55 +using assms
    7.56 +by (auto simp: not_le [symmetric] le_setdist_iff)
    7.57 +
    7.58 +lemma setdist_refl: "setdist s s = 0"
    7.59 +  apply (cases "s = {}")
    7.60 +  apply (force simp add: setdist_def)
    7.61 +  apply (rule antisym [OF _ setdist_pos_le])
    7.62 +  apply (metis all_not_in_conv dist_self setdist_le_dist)
    7.63 +  done
    7.64 +
    7.65 +lemma setdist_sym: "setdist s t = setdist t s"
    7.66 +  by (force simp: setdist_def dist_commute intro!: arg_cong [where f=Inf])
    7.67 +
    7.68 +lemma setdist_triangle: "setdist s t \<le> setdist s {a} + setdist {a} t"
    7.69 +proof (cases "s = {} \<or> t = {}")
    7.70 +  case True then show ?thesis
    7.71 +    using setdist_pos_le by fastforce
    7.72 +next
    7.73 +  case False
    7.74 +  have "\<And>x. x \<in> s \<Longrightarrow> setdist s t - dist x a \<le> setdist {a} t" 
    7.75 +    apply (rule le_setdistI, blast)
    7.76 +    using False apply (fastforce intro: le_setdistI)
    7.77 +    apply (simp add: algebra_simps)
    7.78 +    apply (metis dist_commute dist_triangle_alt order_trans [OF setdist_le_dist])
    7.79 +    done
    7.80 +  then have "setdist s t - setdist {a} t \<le> setdist s {a}"
    7.81 +    using False by (fastforce intro: le_setdistI)
    7.82 +  then show ?thesis
    7.83 +    by (simp add: algebra_simps)
    7.84 +qed
    7.85 +
    7.86 +lemma setdist_singletons [simp]: "setdist {x} {y} = dist x y"
    7.87 +  by (simp add: setdist_def)
    7.88 +
    7.89 +lemma setdist_Lipschitz: "abs(setdist {x} s - setdist {y} s) \<le> dist x y"
    7.90 +  apply (subst setdist_singletons [symmetric])
    7.91 +  by (metis abs_diff_le_iff diff_le_eq setdist_triangle setdist_sym)
    7.92 +
    7.93 +lemma continuous_at_setdist: "continuous (at x) (\<lambda>y. (setdist {y} s))"
    7.94 +  by (force simp: continuous_at_eps_delta dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
    7.95 +
    7.96 +lemma continuous_on_setdist: "continuous_on t (\<lambda>y. (setdist {y} s))"
    7.97 +  by (metis continuous_at_setdist continuous_at_imp_continuous_on)
    7.98 +
    7.99 +lemma uniformly_continuous_on_setdist: "uniformly_continuous_on t (\<lambda>y. (setdist {y} s))"
   7.100 +  by (force simp: uniformly_continuous_on_def dist_real_def intro: le_less_trans [OF setdist_Lipschitz])
   7.101 +
   7.102 +lemma setdist_subset_right: "\<lbrakk>t \<noteq> {}; t \<subseteq> u\<rbrakk> \<Longrightarrow> setdist s u \<le> setdist s t"
   7.103 +  apply (cases "s = {} \<or> u = {}", force)
   7.104 +  apply (auto simp: setdist_def intro!: bdd_belowI [where m=0] cInf_superset_mono)
   7.105 +  done
   7.106 +
   7.107 +lemma setdist_subset_left: "\<lbrakk>s \<noteq> {}; s \<subseteq> t\<rbrakk> \<Longrightarrow> setdist t u \<le> setdist s u"
   7.108 +  by (metis setdist_subset_right setdist_sym)
   7.109 +
   7.110 +lemma setdist_closure_1 [simp]: "setdist (closure s) t = setdist s t"
   7.111 +proof (cases "s = {} \<or> t = {}")
   7.112 +  case True then show ?thesis by force
   7.113 +next
   7.114 +  case False
   7.115 +  { fix y
   7.116 +    assume "y \<in> t"
   7.117 +    have "continuous_on (closure s) (\<lambda>a. dist a y)"
   7.118 +      by (auto simp: continuous_intros dist_norm)
   7.119 +    then have *: "\<And>x. x \<in> closure s \<Longrightarrow> setdist s t \<le> dist x y"
   7.120 +      apply (rule continuous_ge_on_closure)
   7.121 +      apply assumption
   7.122 +      apply (blast intro: setdist_le_dist `y \<in> t` )
   7.123 +      done
   7.124 +  } note * = this
   7.125 +  show ?thesis
   7.126 +    apply (rule antisym)
   7.127 +     using False closure_subset apply (blast intro: setdist_subset_left)
   7.128 +    using False *
   7.129 +    apply (force simp add: closure_eq_empty intro!: le_setdistI)
   7.130 +    done
   7.131 +qed
   7.132 +
   7.133 +lemma setdist_closure_2 [simp]: "setdist t (closure s) = setdist t s"
   7.134 +by (metis setdist_closure_1 setdist_sym)
   7.135 +
   7.136 +lemma setdist_compact_closed:
   7.137 +  fixes s :: "'a::euclidean_space set"
   7.138 +  assumes s: "compact s" and t: "closed t"
   7.139 +      and "s \<noteq> {}" "t \<noteq> {}"
   7.140 +    shows "\<exists>x \<in> s. \<exists>y \<in> t. dist x y = setdist s t"
   7.141 +proof -
   7.142 +  have "{x - y |x y. x \<in> s \<and> y \<in> t} \<noteq> {}"
   7.143 +    using assms by blast
   7.144 +  then
   7.145 +  have "\<exists>x \<in> s. \<exists>y \<in> t. dist x y \<le> setdist s t"
   7.146 +    using  distance_attains_inf [where a=0, OF compact_closed_differences [OF s t]] assms
   7.147 +    apply (clarsimp simp: dist_norm le_setdist_iff, blast)
   7.148 +    done
   7.149 +  then show ?thesis
   7.150 +    by (blast intro!: antisym [OF _ setdist_le_dist] )
   7.151 +qed
   7.152 +
   7.153 +lemma setdist_closed_compact:
   7.154 +  fixes s :: "'a::euclidean_space set"
   7.155 +  assumes s: "closed s" and t: "compact t"
   7.156 +      and "s \<noteq> {}" "t \<noteq> {}"
   7.157 +    shows "\<exists>x \<in> s. \<exists>y \<in> t. dist x y = setdist s t"
   7.158 +  using setdist_compact_closed [OF t s `t \<noteq> {}` `s \<noteq> {}`]
   7.159 +  by (metis dist_commute setdist_sym)
   7.160 +
   7.161 +lemma setdist_eq_0I: "\<lbrakk>x \<in> s; x \<in> t\<rbrakk> \<Longrightarrow> setdist s t = 0"
   7.162 +  by (metis antisym dist_self setdist_le_dist setdist_pos_le)
   7.163 +
   7.164 +lemma setdist_eq_0_compact_closed:
   7.165 +  fixes s :: "'a::euclidean_space set"
   7.166 +  assumes s: "compact s" and t: "closed t"
   7.167 +    shows "setdist s t = 0 \<longleftrightarrow> s = {} \<or> t = {} \<or> s \<inter> t \<noteq> {}"
   7.168 +  apply (cases "s = {} \<or> t = {}", force)
   7.169 +  using setdist_compact_closed [OF s t]  
   7.170 +  apply (force intro: setdist_eq_0I )
   7.171 +  done
   7.172 +
   7.173 +corollary setdist_gt_0_compact_closed:
   7.174 +  fixes s :: "'a::euclidean_space set"
   7.175 +  assumes s: "compact s" and t: "closed t"
   7.176 +    shows "setdist s t > 0 \<longleftrightarrow> (s \<noteq> {} \<and> t \<noteq> {} \<and> s \<inter> t = {})"
   7.177 +  using setdist_pos_le [of s t] setdist_eq_0_compact_closed [OF assms]
   7.178 +  by linarith
   7.179 +
   7.180 +lemma setdist_eq_0_closed_compact:
   7.181 +  fixes s :: "'a::euclidean_space set"
   7.182 +  assumes s: "closed s" and t: "compact t"
   7.183 +    shows "setdist s t = 0 \<longleftrightarrow> s = {} \<or> t = {} \<or> s \<inter> t \<noteq> {}"
   7.184 +  using setdist_eq_0_compact_closed [OF t s]
   7.185 +  by (metis Int_commute setdist_sym)
   7.186 +
   7.187 +lemma setdist_eq_0_bounded:
   7.188 +  fixes s :: "'a::euclidean_space set"
   7.189 +  assumes "bounded s \<or> bounded t"
   7.190 +    shows "setdist s t = 0 \<longleftrightarrow> s = {} \<or> t = {} \<or> closure s \<inter> closure t \<noteq> {}"
   7.191 +  apply (cases "s = {} \<or> t = {}", force)
   7.192 +  using setdist_eq_0_compact_closed [of "closure s" "closure t"] 
   7.193 +        setdist_eq_0_closed_compact [of "closure s" "closure t"] assms 
   7.194 +  apply (force simp add:  bounded_closure compact_eq_bounded_closed)
   7.195 +  done
   7.196 +
   7.197 +lemma setdist_unique: 
   7.198 +  "\<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>
   7.199 +   \<Longrightarrow> setdist s t = dist a b"
   7.200 +  by (force simp add: setdist_le_dist le_setdist_iff intro: antisym)
   7.201 +
   7.202 +lemma setdist_closest_point: 
   7.203 +    "\<lbrakk>closed s; s \<noteq> {}\<rbrakk> \<Longrightarrow> setdist {a} s = dist a (closest_point s a)"
   7.204 +  apply (rule setdist_unique)
   7.205 +  using closest_point_le
   7.206 +  apply (auto simp: closest_point_in_set)
   7.207 +  done
   7.208 +
   7.209 +lemma setdist_eq_0_sing_1 [simp]: 
   7.210 +  fixes s :: "'a::euclidean_space set"
   7.211 +  shows "setdist {x} s = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
   7.212 +by (auto simp: setdist_eq_0_bounded)
   7.213 +
   7.214 +lemma setdist_eq_0_sing_2 [simp]: 
   7.215 +  fixes s :: "'a::euclidean_space set"
   7.216 +  shows "setdist s {x} = 0 \<longleftrightarrow> s = {} \<or> x \<in> closure s"
   7.217 +by (auto simp: setdist_eq_0_bounded)
   7.218 +
   7.219 +lemma setdist_sing_in_set:
   7.220 +  fixes s :: "'a::euclidean_space set"
   7.221 +  shows "x \<in> s \<Longrightarrow> setdist {x} s = 0"
   7.222 +using closure_subset by force
   7.223 +
   7.224 +lemma setdist_le_sing: "x \<in> s ==> setdist s t \<le> setdist {x} t"
   7.225 +  using setdist_subset_left by auto
   7.226 +
   7.227 +
   7.228  end
     8.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Aug 19 15:40:59 2015 +0200
     8.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Aug 19 19:18:19 2015 +0100
     8.3 @@ -92,6 +92,18 @@
     8.4      by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"])
     8.5  qed auto
     8.6  
     8.7 +lemma (in euclidean_space) euclidean_representation_setsum_fun: 
     8.8 +    "(\<lambda>x. \<Sum>b\<in>Basis. inner (f x) b *\<^sub>R b) = f"
     8.9 +  by (rule ext) (simp add: euclidean_representation_setsum)
    8.10 +
    8.11 +lemma euclidean_isCont:
    8.12 +  assumes "\<And>b. b \<in> Basis \<Longrightarrow> isCont (\<lambda>x. (inner (f x) b) *\<^sub>R b) x"
    8.13 +    shows "isCont f x"
    8.14 +  apply (subst euclidean_representation_setsum_fun [symmetric])
    8.15 +  apply (rule isCont_setsum)
    8.16 +  apply (blast intro: assms)
    8.17 +  done
    8.18 +
    8.19  lemma DIM_positive: "0 < DIM('a::euclidean_space)"
    8.20    by (simp add: card_gt_0_iff)
    8.21  
     9.1 --- a/src/HOL/Multivariate_Analysis/L2_Norm.thy	Wed Aug 19 15:40:59 2015 +0200
     9.2 +++ b/src/HOL/Multivariate_Analysis/L2_Norm.thy	Wed Aug 19 19:18:19 2015 +0100
     9.3 @@ -70,13 +70,6 @@
     9.4    apply (simp add: real_sqrt_mult setsum_nonneg)
     9.5    done
     9.6  
     9.7 -lemma setsum_nonneg_eq_0_iff:
     9.8 -  fixes f :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
     9.9 -  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)"
    9.10 -  apply (induct set: finite, simp)
    9.11 -  apply (simp add: add_nonneg_eq_0_iff setsum_nonneg)
    9.12 -  done
    9.13 -
    9.14  lemma setL2_eq_0_iff: "finite A \<Longrightarrow> setL2 f A = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)"
    9.15    unfolding setL2_def
    9.16    by (simp add: setsum_nonneg setsum_nonneg_eq_0_iff)
    10.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 19 15:40:59 2015 +0200
    10.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Wed Aug 19 19:18:19 2015 +0100
    10.3 @@ -562,25 +562,45 @@
    10.4    using reals_Archimedean[of e] less_trans[of 0 "1 / real n" e for n::nat]
    10.5    by (auto simp add: field_simps cong: conj_cong)
    10.6  
    10.7 -lemma real_pow_lbound: "0 \<le> x \<Longrightarrow> 1 + real n * x \<le> (1 + x) ^ n"
    10.8 +text{*Bernoulli's inequality*}
    10.9 +lemma Bernoulli_inequality:
   10.10 +  fixes x :: real
   10.11 +  assumes "-1 \<le> x"
   10.12 +    shows "1 + n * x \<le> (1 + x) ^ n"
   10.13  proof (induct n)
   10.14    case 0
   10.15    then show ?case by simp
   10.16  next
   10.17    case (Suc n)
   10.18 -  then have h: "1 + real n * x \<le> (1 + x) ^ n"
   10.19 -    by simp
   10.20 -  from h have p: "1 \<le> (1 + x) ^ n"
   10.21 -    using Suc.prems by simp
   10.22 -  from h have "1 + real n * x + x \<le> (1 + x) ^ n + x"
   10.23 +  have "1 + Suc n * x \<le> 1 + (Suc n)*x + n * x^2"
   10.24 +    by (simp add: algebra_simps)
   10.25 +  also have "... = (1 + x) * (1 + n*x)"
   10.26 +    by (auto simp: power2_eq_square algebra_simps  real_of_nat_Suc)
   10.27 +  also have "... \<le> (1 + x) ^ Suc n"
   10.28 +    using Suc.hyps assms mult_left_mono by fastforce
   10.29 +  finally show ?case .
   10.30 +qed
   10.31 +
   10.32 +lemma Bernoulli_inequality_even:
   10.33 +  fixes x :: real
   10.34 +  assumes "even n"
   10.35 +    shows "1 + n * x \<le> (1 + x) ^ n"
   10.36 +proof (cases "-1 \<le> x \<or> n=0")
   10.37 +  case True
   10.38 +  then show ?thesis
   10.39 +    by (auto simp: Bernoulli_inequality)
   10.40 +next
   10.41 +  case False
   10.42 +  then have "real n \<ge> 1"
   10.43      by simp
   10.44 -  also have "\<dots> \<le> (1 + x) ^ Suc n"
   10.45 -    apply (subst diff_le_0_iff_le[symmetric])
   10.46 -    using mult_left_mono[OF p Suc.prems]
   10.47 -    apply (simp add: field_simps)
   10.48 -    done
   10.49 -  finally show ?case
   10.50 -    by (simp add: real_of_nat_Suc field_simps)
   10.51 +  with False have "n * x \<le> -1"
   10.52 +    by (metis linear minus_zero mult.commute mult.left_neutral mult_left_mono_neg neg_le_iff_le order_trans zero_le_one)
   10.53 +  then have "1 + n * x \<le> 0"
   10.54 +    by auto
   10.55 +  also have "... \<le> (1 + x) ^ n"
   10.56 +    using assms
   10.57 +    using zero_le_even_power by blast
   10.58 +  finally show ?thesis .
   10.59  qed
   10.60  
   10.61  lemma real_arch_pow:
   10.62 @@ -592,8 +612,8 @@
   10.63      by arith
   10.64    from reals_Archimedean3[OF x0, rule_format, of y]
   10.65    obtain n :: nat where n: "y < real n * (x - 1)" by metis
   10.66 -  from x0 have x00: "x- 1 \<ge> 0" by arith
   10.67 -  from real_pow_lbound[OF x00, of n] n
   10.68 +  from x0 have x00: "x- 1 \<ge> -1" by arith
   10.69 +  from Bernoulli_inequality[OF x00, of n] n
   10.70    have "y < x^n" by auto
   10.71    then show ?thesis by metis
   10.72  qed
   10.73 @@ -1417,7 +1437,7 @@
   10.74    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>)"
   10.75      by (rule setsum.commute)
   10.76    also have "\<dots> \<le> of_nat (card (Basis :: 'n set)) * (2 * e)"
   10.77 -  proof (rule setsum_bounded)
   10.78 +  proof (rule setsum_bounded_above)
   10.79      fix i :: 'n
   10.80      assume i: "i \<in> Basis"
   10.81      have "norm (\<Sum>x\<in>P. \<bar>f x \<bullet> i\<bar>) \<le>
   10.82 @@ -2828,7 +2848,7 @@
   10.83      unfolding real_of_nat_def
   10.84      apply (subst euclidean_inner)
   10.85      apply (subst power2_abs[symmetric])
   10.86 -    apply (rule order_trans[OF setsum_bounded[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
   10.87 +    apply (rule order_trans[OF setsum_bounded_above[where K="\<bar>infnorm x\<bar>\<^sup>2"]])
   10.88      apply (auto simp add: power2_eq_square[symmetric])
   10.89      apply (subst power2_abs[symmetric])
   10.90      apply (rule power_mono)
    11.1 --- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Aug 19 15:40:59 2015 +0200
    11.2 +++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Wed Aug 19 19:18:19 2015 +0100
    11.3 @@ -175,7 +175,7 @@
    11.4  lemma simple_path_eq_arc: "pathfinish g \<noteq> pathstart g \<Longrightarrow> (simple_path g = arc g)"
    11.5    by (simp add: arc_simple_path)
    11.6  
    11.7 -lemma path_image_nonempty: "path_image g \<noteq> {}"
    11.8 +lemma path_image_nonempty [simp]: "path_image g \<noteq> {}"
    11.9    unfolding path_image_def image_is_empty box_eq_empty
   11.10    by auto
   11.11  
    12.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 19 15:40:59 2015 +0200
    12.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 19 19:18:19 2015 +0100
    12.3 @@ -1602,7 +1602,7 @@
    12.4  lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
    12.5    unfolding closure_interior by simp
    12.6  
    12.7 -lemma closure_eq_empty: "closure S = {} \<longleftrightarrow> S = {}"
    12.8 +lemma closure_eq_empty [iff]: "closure S = {} \<longleftrightarrow> S = {}"
    12.9    using closure_empty closure_subset[of S]
   12.10    by blast
   12.11  
   12.12 @@ -1826,7 +1826,7 @@
   12.13  
   12.14  text\<open>Interrelations between restricted and unrestricted limits.\<close>
   12.15  
   12.16 -lemma Lim_at_imp_Lim_at_within: 
   12.17 +lemma Lim_at_imp_Lim_at_within:
   12.18    "(f ---> l) (at x) \<Longrightarrow> (f ---> l) (at x within S)"
   12.19    by (metis order_refl filterlim_mono subset_UNIV at_le)
   12.20  
   12.21 @@ -2831,12 +2831,12 @@
   12.22       (metis abs_le_D1 add.commute diff_le_eq)
   12.23  
   12.24  lemma bounded_inner_imp_bdd_above:
   12.25 -  assumes "bounded s" 
   12.26 +  assumes "bounded s"
   12.27      shows "bdd_above ((\<lambda>x. x \<bullet> a) ` s)"
   12.28  by (simp add: assms bounded_imp_bdd_above bounded_linear_image bounded_linear_inner_left)
   12.29  
   12.30  lemma bounded_inner_imp_bdd_below:
   12.31 -  assumes "bounded s" 
   12.32 +  assumes "bounded s"
   12.33      shows "bdd_below ((\<lambda>x. x \<bullet> a) ` s)"
   12.34  by (simp add: assms bounded_imp_bdd_below bounded_linear_image bounded_linear_inner_left)
   12.35  
   12.36 @@ -4635,6 +4635,12 @@
   12.37  
   12.38  text\<open>Some simple consequential lemmas.\<close>
   12.39  
   12.40 +lemma uniformly_continuous_onE:
   12.41 +  assumes "uniformly_continuous_on s f" "0 < e"
   12.42 +  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"
   12.43 +using assms
   12.44 +by (auto simp: uniformly_continuous_on_def)
   12.45 +
   12.46  lemma uniformly_continuous_imp_continuous:
   12.47    "uniformly_continuous_on s f \<Longrightarrow> continuous_on s f"
   12.48    unfolding uniformly_continuous_on_def continuous_on_iff by blast
   12.49 @@ -6166,6 +6172,19 @@
   12.50    finally show ?thesis .
   12.51  qed
   12.52  
   12.53 +lemma continuous_on_closed_Collect_le:
   12.54 +  fixes f g :: "'a::t2_space \<Rightarrow> real"
   12.55 +  assumes f: "continuous_on s f" and g: "continuous_on s g" and s: "closed s"
   12.56 +  shows "closed {x \<in> s. f x \<le> g x}"
   12.57 +proof -
   12.58 +  have "closed ((\<lambda>x. g x - f x) -` {0..} \<inter> s)"
   12.59 +    using closed_real_atLeast continuous_on_diff [OF g f]
   12.60 +    by (simp add: continuous_on_closed_vimage [OF s])
   12.61 +  also have "((\<lambda>x. g x - f x) -` {0..} \<inter> s) = {x\<in>s. f x \<le> g x}"
   12.62 +    by auto
   12.63 +  finally show ?thesis .
   12.64 +qed
   12.65 +
   12.66  lemma continuous_at_inner: "continuous (at x) (inner a)"
   12.67    unfolding continuous_at by (intro tendsto_intros)
   12.68  
   12.69 @@ -6194,6 +6213,25 @@
   12.70    shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
   12.71    by (simp add: Collect_ball_eq closed_INT closed_Collect_le)
   12.72  
   12.73 +lemma continuous_le_on_closure:
   12.74 +  fixes a::real
   12.75 +  assumes f: "continuous_on (closure s) f"
   12.76 +      and x: "x \<in> closure(s)"
   12.77 +      and xlo: "\<And>x. x \<in> s ==> f(x) \<le> a"
   12.78 +    shows "f(x) \<le> a"
   12.79 +    using image_closure_subset [OF f] 
   12.80 +  using image_closure_subset [OF f] closed_halfspace_le [of "1::real" a] assms
   12.81 +  by force
   12.82 +
   12.83 +lemma continuous_ge_on_closure:
   12.84 +  fixes a::real
   12.85 +  assumes f: "continuous_on (closure s) f"
   12.86 +      and x: "x \<in> closure(s)"
   12.87 +      and xlo: "\<And>x. x \<in> s ==> f(x) \<ge> a"
   12.88 +    shows "f(x) \<ge> a"
   12.89 +  using image_closure_subset [OF f] closed_halfspace_ge [of a "1::real"] assms
   12.90 +  by force
   12.91 +
   12.92  text \<open>Openness of halfspaces.\<close>
   12.93  
   12.94  lemma open_halfspace_lt: "open {x. inner a x < b}"
   12.95 @@ -7320,7 +7358,7 @@
   12.96  
   12.97  subsection \<open>Banach fixed point theorem (not really topological...)\<close>
   12.98  
   12.99 -lemma banach_fix:
  12.100 +theorem banach_fix:
  12.101    assumes s: "complete s" "s \<noteq> {}"
  12.102      and c: "0 \<le> c" "c < 1"
  12.103      and f: "(f ` s) \<subseteq> s"
  12.104 @@ -7501,7 +7539,7 @@
  12.105  
  12.106  subsection \<open>Edelstein fixed point theorem\<close>
  12.107  
  12.108 -lemma edelstein_fix:
  12.109 +theorem edelstein_fix:
  12.110    fixes s :: "'a::metric_space set"
  12.111    assumes s: "compact s" "s \<noteq> {}"
  12.112      and gs: "(g ` s) \<subseteq> s"
    13.1 --- a/src/HOL/Power.thy	Wed Aug 19 15:40:59 2015 +0200
    13.2 +++ b/src/HOL/Power.thy	Wed Aug 19 19:18:19 2015 +0100
    13.3 @@ -762,6 +762,10 @@
    13.4    "(x - y)\<^sup>2 = x\<^sup>2 + y\<^sup>2 - 2 * x * y"
    13.5    by (simp add: algebra_simps power2_eq_square mult_2_right)
    13.6  
    13.7 +lemma (in comm_ring_1) power2_commute:
    13.8 +  "(x - y)\<^sup>2 = (y - x)\<^sup>2"
    13.9 +  by (simp add: algebra_simps power2_eq_square)
   13.10 +
   13.11  
   13.12  text \<open>Simprules for comparisons where common factors can be cancelled.\<close>
   13.13