More mainly topological results
authorpaulson <lp15@cam.ac.uk>
Thu Sep 22 15:44:47 2016 +0100 (2016-09-22)
changeset 63938f6ce08859d4c
parent 63928 d81fb5b46a5c
child 63939 d4b89572ae71
More mainly topological results
src/HOL/Analysis/Bounded_Linear_Function.thy
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Euclidean_Space.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/L2_Norm.thy
src/HOL/Analysis/Linear_Algebra.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Analysis/Weierstrass_Theorems.thy
src/HOL/Groups_Big.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Wed Sep 21 16:59:51 2016 +0100
     1.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Sep 22 15:44:47 2016 +0100
     1.3 @@ -391,7 +391,7 @@
     1.4    also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))"
     1.5      using b by (simp add: setsum.delta)
     1.6    also have "\<dots> = f x \<bullet> b"
     1.7 -    by (subst linear_componentwise[symmetric]) (unfold_locales, rule)
     1.8 +    by (metis (mono_tags, lifting) Linear_Algebra.linear_componentwise linear_axioms)
     1.9    finally show "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b = f x \<bullet> b" .
    1.10  qed
    1.11  
     2.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Sep 21 16:59:51 2016 +0100
     2.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Sep 22 15:44:47 2016 +0100
     2.3 @@ -1,7 +1,7 @@
     2.4  section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
     2.5  
     2.6  theory Cartesian_Euclidean_Space
     2.7 -imports Finite_Cartesian_Product Derivative (* Henstock_Kurzweil_Integration *)
     2.8 +imports Finite_Cartesian_Product Derivative 
     2.9  begin
    2.10  
    2.11  lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
    2.12 @@ -11,6 +11,7 @@
    2.13    "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)"
    2.14    by simp
    2.15  
    2.16 +(*move up?*)
    2.17  lemma setsum_UNIV_sum:
    2.18    fixes g :: "'a::finite + 'b::finite \<Rightarrow> _"
    2.19    shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))"
    2.20 @@ -33,7 +34,6 @@
    2.21    qed simp
    2.22  qed simp
    2.23  
    2.24 -
    2.25  subsection\<open>Basic componentwise operations on vectors.\<close>
    2.26  
    2.27  instantiation vec :: (times, finite) times
    2.28 @@ -598,7 +598,7 @@
    2.29  lemma basis_expansion: "setsum (\<lambda>i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)"
    2.30    by (auto simp add: axis_def vec_eq_iff if_distrib setsum.If_cases cong del: if_weak_cong)
    2.31  
    2.32 -lemma linear_componentwise:
    2.33 +lemma linear_componentwise_expansion:
    2.34    fixes f:: "real ^'m \<Rightarrow> real ^ _"
    2.35    assumes lf: "linear f"
    2.36    shows "(f x)$j = setsum (\<lambda>i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
    2.37 @@ -636,9 +636,7 @@
    2.38    assumes lf: "linear f"
    2.39    shows "matrix f *v x = f (x::real ^ 'n)"
    2.40    apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute)
    2.41 -  apply clarify
    2.42 -  apply (rule linear_componentwise[OF lf, symmetric])
    2.43 -  done
    2.44 +  by (simp add: linear_componentwise_expansion lf)
    2.45  
    2.46  lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))"
    2.47    by (simp add: ext matrix_works)
     3.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Wed Sep 21 16:59:51 2016 +0100
     3.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Sep 22 15:44:47 2016 +0100
     3.3 @@ -2163,7 +2163,7 @@
     3.4      { fix x y z n
     3.5        assume At: "At x y z n"
     3.6        then have contf': "continuous_on (convex hull {x,y,z}) f"
     3.7 -        using contf At_def continuous_on_subset by blast
     3.8 +        using contf At_def continuous_on_subset by metis
     3.9        have "\<exists>x' y' z'. At x' y' z' (Suc n) \<and> convex hull {x',y',z'} \<subseteq> convex hull {x,y,z}"
    3.10          using At
    3.11          apply (simp add: At_def)
    3.12 @@ -3213,11 +3213,6 @@
    3.13    using contour_integral_nearby [OF assms, where atends=False]
    3.14    unfolding linked_paths_def by simp_all
    3.15  
    3.16 -corollary differentiable_polynomial_function:
    3.17 -  fixes p :: "real \<Rightarrow> 'a::euclidean_space"
    3.18 -  shows "polynomial_function p \<Longrightarrow> p differentiable_on s"
    3.19 -by (meson has_vector_derivative_polynomial_function differentiable_at_imp_differentiable_on differentiable_def has_vector_derivative_def)
    3.20 -
    3.21  lemma C1_differentiable_polynomial_function:
    3.22    fixes p :: "real \<Rightarrow> 'a::euclidean_space"
    3.23    shows "polynomial_function p \<Longrightarrow> p C1_differentiable_on s"
    3.24 @@ -3255,7 +3250,7 @@
    3.25    done
    3.26  then obtain p' where p': "polynomial_function p'"
    3.27           "\<And>x. (p has_vector_derivative (p' x)) (at x)"
    3.28 -  using has_vector_derivative_polynomial_function by force
    3.29 +  by (blast intro: has_vector_derivative_polynomial_function that elim: )
    3.30  then have "bounded(p' ` {0..1})"
    3.31    using continuous_on_polymonial_function
    3.32    by (force simp: intro!: compact_imp_bounded compact_continuous_image)
     4.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Sep 21 16:59:51 2016 +0100
     4.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Sep 22 15:44:47 2016 +0100
     4.3 @@ -1,5 +1,5 @@
     4.4 -(*  Title:      HOL/Analysis/Convex_Euclidean_Space.thy
     4.5 -    Authors: Robert Himmelmann, TU Muenchen; Bogdan Grechuk, University of Edinburgh; LCP
     4.6 +(*  Author:     L C Paulson, University of Cambridge
     4.7 +    Authors: Robert Himmelmann, TU Muenchen; Bogdan Grechuk, University of Edinburgh
     4.8  *)
     4.9  
    4.10  section \<open>Convex sets, functions and related things\<close>
    4.11 @@ -219,7 +219,7 @@
    4.12      from gxy have th0: "g (x - y) = 0"
    4.13        by (simp add: linear_diff[OF g(1)])
    4.14      have th1: "x - y \<in> span B" using x' y'
    4.15 -      by (metis span_sub)
    4.16 +      by (metis span_diff)
    4.17      have "x = y" using g0[OF th1 th0] by simp
    4.18    }
    4.19    then have giS: "inj_on g S" unfolding inj_on_def by blast
    4.20 @@ -2267,7 +2267,7 @@
    4.21      apply (rule subset_le_dim)
    4.22      unfolding subset_eq
    4.23      using \<open>a\<in>s\<close>
    4.24 -    apply (auto simp add:span_superset span_sub)
    4.25 +    apply (auto simp add:span_superset span_diff)
    4.26      done
    4.27    also have "\<dots> < dim s + 1" by auto
    4.28    also have "\<dots> \<le> card (s - {a})"
     5.1 --- a/src/HOL/Analysis/Derivative.thy	Wed Sep 21 16:59:51 2016 +0100
     5.2 +++ b/src/HOL/Analysis/Derivative.thy	Thu Sep 22 15:44:47 2016 +0100
     5.3 @@ -9,29 +9,7 @@
     5.4  imports Brouwer_Fixpoint Operator_Norm Uniform_Limit Bounded_Linear_Function
     5.5  begin
     5.6  
     5.7 -lemma bounded_linear_component [intro]: "bounded_linear (\<lambda>x::'a::euclidean_space. x \<bullet> k)"
     5.8 -  by (rule bounded_linear_inner_left)
     5.9 -
    5.10 -lemma onorm_inner_left:
    5.11 -  assumes "bounded_linear r"
    5.12 -  shows "onorm (\<lambda>x. r x \<bullet> f) \<le> onorm r * norm f"
    5.13 -proof (rule onorm_bound)
    5.14 -  fix x
    5.15 -  have "norm (r x \<bullet> f) \<le> norm (r x) * norm f"
    5.16 -    by (simp add: Cauchy_Schwarz_ineq2)
    5.17 -  also have "\<dots> \<le> onorm r * norm x * norm f"
    5.18 -    by (intro mult_right_mono onorm assms norm_ge_zero)
    5.19 -  finally show "norm (r x \<bullet> f) \<le> onorm r * norm f * norm x"
    5.20 -    by (simp add: ac_simps)
    5.21 -qed (intro mult_nonneg_nonneg norm_ge_zero onorm_pos_le assms)
    5.22 -
    5.23 -lemma onorm_inner_right:
    5.24 -  assumes "bounded_linear r"
    5.25 -  shows "onorm (\<lambda>x. f \<bullet> r x) \<le> norm f * onorm r"
    5.26 -  apply (subst inner_commute)
    5.27 -  apply (rule onorm_inner_left[OF assms, THEN order_trans])
    5.28 -  apply simp
    5.29 -  done
    5.30 +declare bounded_linear_inner_left [intro]
    5.31  
    5.32  declare has_derivative_bounded_linear[dest]
    5.33  
     6.1 --- a/src/HOL/Analysis/Euclidean_Space.thy	Wed Sep 21 16:59:51 2016 +0100
     6.2 +++ b/src/HOL/Analysis/Euclidean_Space.thy	Thu Sep 22 15:44:47 2016 +0100
     6.3 @@ -105,10 +105,10 @@
     6.4    apply (blast intro: assms)
     6.5    done
     6.6  
     6.7 -lemma DIM_positive: "0 < DIM('a::euclidean_space)"
     6.8 +lemma DIM_positive [simp]: "0 < DIM('a::euclidean_space)"
     6.9    by (simp add: card_gt_0_iff)
    6.10  
    6.11 -lemma DIM_ge_Suc0 [iff]: "Suc 0 \<le> card Basis"
    6.12 +lemma DIM_ge_Suc0 [simp]: "Suc 0 \<le> card Basis"
    6.13    by (meson DIM_positive Suc_leI)
    6.14  
    6.15  
     7.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Sep 21 16:59:51 2016 +0100
     7.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 22 15:44:47 2016 +0100
     7.3 @@ -2902,7 +2902,7 @@
     7.4    fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space"
     7.5    assumes "f integrable_on s"
     7.6    shows "integral s (\<lambda>x. f x \<bullet> k) = integral s f \<bullet> k"
     7.7 -  unfolding integral_linear[OF assms(1) bounded_linear_component,unfolded o_def] ..
     7.8 +  unfolding integral_linear[OF assms(1) bounded_linear_inner_left,unfolded o_def] ..
     7.9  
    7.10  lemma has_integral_setsum:
    7.11    assumes "finite t"
    7.12 @@ -3090,7 +3090,7 @@
    7.13    shows "(f has_integral y) A \<longleftrightarrow> (\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
    7.14  proof safe
    7.15    fix b :: 'b assume "(f has_integral y) A"
    7.16 -  from has_integral_linear[OF this(1) bounded_linear_component, of b]
    7.17 +  from has_integral_linear[OF this(1) bounded_linear_inner_left, of b]
    7.18      show "((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A" by (simp add: o_def)
    7.19  next
    7.20    assume "(\<forall>b\<in>Basis. ((\<lambda>x. f x \<bullet> b) has_integral (y \<bullet> b)) A)"
    7.21 @@ -3148,7 +3148,7 @@
    7.22  
    7.23  lemma integrable_component:
    7.24    "f integrable_on A \<Longrightarrow> (\<lambda>x. f x \<bullet> (y :: 'b :: euclidean_space)) integrable_on A"
    7.25 -  by (drule integrable_linear[OF _ bounded_linear_component[of y]]) (simp add: o_def)
    7.26 +  by (drule integrable_linear[OF _ bounded_linear_inner_left[of y]]) (simp add: o_def)
    7.27  
    7.28  
    7.29  
     8.1 --- a/src/HOL/Analysis/L2_Norm.thy	Wed Sep 21 16:59:51 2016 +0100
     8.2 +++ b/src/HOL/Analysis/L2_Norm.thy	Thu Sep 22 15:44:47 2016 +0100
     8.3 @@ -165,12 +165,7 @@
     8.4    done
     8.5  
     8.6  lemma member_le_setL2: "\<lbrakk>finite A; i \<in> A\<rbrakk> \<Longrightarrow> f i \<le> setL2 f A"
     8.7 -  apply (rule_tac s="insert i (A - {i})" and t="A" in subst)
     8.8 -  apply fast
     8.9 -  apply (subst setL2_insert)
    8.10 -  apply simp
    8.11 -  apply simp
    8.12 -  apply simp
    8.13 -  done
    8.14 +  unfolding setL2_def
    8.15 +  by (auto intro!: member_le_setsum real_le_rsqrt)
    8.16  
    8.17  end
     9.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Wed Sep 21 16:59:51 2016 +0100
     9.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 22 15:44:47 2016 +0100
     9.3 @@ -457,7 +457,7 @@
     9.4  lemma span_neg: "x \<in> span S \<Longrightarrow> - x \<in> span S"
     9.5    by (metis subspace_neg subspace_span)
     9.6  
     9.7 -lemma span_sub: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
     9.8 +lemma span_diff: "x \<in> span S \<Longrightarrow> y \<in> span S \<Longrightarrow> x - y \<in> span S"
     9.9    by (metis subspace_span subspace_diff)
    9.10  
    9.11  lemma (in real_vector) span_setsum: "(\<And>x. x \<in> A \<Longrightarrow> f x \<in> span S) \<Longrightarrow> setsum f A \<in> span S"
    9.12 @@ -2615,7 +2615,7 @@
    9.13      from gxy have th0: "g (x - y) = 0"
    9.14        by (simp add: linear_diff[OF g(1)])
    9.15      have th1: "x - y \<in> span B"
    9.16 -      using x' y' by (metis span_sub)
    9.17 +      using x' y' by (metis span_diff)
    9.18      have "x = y"
    9.19        using g0[OF th1 th0] by simp
    9.20    }
    10.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Wed Sep 21 16:59:51 2016 +0100
    10.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Sep 22 15:44:47 2016 +0100
    10.3 @@ -1,4 +1,4 @@
    10.4 -(*  title:      HOL/Library/Topology_Euclidian_Space.thy
    10.5 +(*  Author:     L C Paulson, University of Cambridge
    10.6      Author:     Amine Chaieb, University of Cambridge
    10.7      Author:     Robert Himmelmann, TU Muenchen
    10.8      Author:     Brian Huffman, Portland State University
    10.9 @@ -4040,6 +4040,11 @@
   10.10      by auto
   10.11  qed
   10.12  
   10.13 +corollary infinite_openin:
   10.14 +  fixes S :: "'a :: t1_space set"
   10.15 +  shows "\<lbrakk>openin (subtopology euclidean U) S; x \<in> S; x islimpt U\<rbrakk> \<Longrightarrow> infinite S"
   10.16 +  by (clarsimp simp add: openin_open islimpt_eq_acc_point inf_commute)
   10.17 +
   10.18  lemma islimpt_range_imp_convergent_subsequence:
   10.19    fixes l :: "'a :: {t1_space, first_countable_topology}"
   10.20    assumes l: "l islimpt (range f)"
   10.21 @@ -6906,7 +6911,7 @@
   10.22    show "\<exists>e>0. \<forall>y. dist y (f x) < e \<longrightarrow> y \<in> f ` A"
   10.23    proof (intro exI conjI)
   10.24      show "\<delta> > 0"
   10.25 -      using \<open>e > 0\<close> \<open>B > 0\<close>  by (simp add: \<delta>_def divide_simps) (simp add: mult_less_0_iff)
   10.26 +      using \<open>e > 0\<close> \<open>B > 0\<close>  by (simp add: \<delta>_def divide_simps)
   10.27      have "y \<in> f ` A" if "dist y (f x) * (B * real DIM('b)) < e" for y
   10.28      proof -
   10.29        define u where "u \<equiv> y - f x"
   10.30 @@ -9712,6 +9717,126 @@
   10.31  apply (simp add: convergent_imp_bounded)
   10.32  by (simp add: closed_limpt islimpt_insert sequence_unique_limpt)
   10.33  
   10.34 +
   10.35 +subsection\<open>Componentwise limits and continuity\<close>
   10.36 +
   10.37 +text\<open>But is the premise really necessary? Need to generalise @{thm euclidean_dist_l2}\<close>
   10.38 +lemma Euclidean_dist_upper: "i \<in> Basis \<Longrightarrow> dist (x \<bullet> i) (y \<bullet> i) \<le> dist x y"
   10.39 +  by (metis (no_types) member_le_setL2 euclidean_dist_l2 finite_Basis)
   10.40 +
   10.41 +text\<open>But is the premise @{term \<open>i \<in> Basis\<close>} really necessary?\<close>
   10.42 +lemma open_preimage_inner:
   10.43 +  assumes "open S" "i \<in> Basis"
   10.44 +    shows "open {x. x \<bullet> i \<in> S}"
   10.45 +proof (rule openI, simp)
   10.46 +  fix x
   10.47 +  assume x: "x \<bullet> i \<in> S"
   10.48 +  with assms obtain e where "0 < e" and e: "ball (x \<bullet> i) e \<subseteq> S"
   10.49 +    by (auto simp: open_contains_ball_eq)
   10.50 +  have "\<exists>e>0. ball (y \<bullet> i) e \<subseteq> S" if dxy: "dist x y < e / 2" for y
   10.51 +  proof (intro exI conjI)
   10.52 +    have "dist (x \<bullet> i) (y \<bullet> i) < e / 2"
   10.53 +      by (meson \<open>i \<in> Basis\<close> dual_order.trans Euclidean_dist_upper not_le that)
   10.54 +    then have "dist (x \<bullet> i) z < e" if "dist (y \<bullet> i) z < e / 2" for z
   10.55 +      by (metis dist_commute dist_triangle_half_l that)
   10.56 +    then have "ball (y \<bullet> i) (e / 2) \<subseteq> ball (x \<bullet> i) e"
   10.57 +      using mem_ball by blast
   10.58 +      with e show "ball (y \<bullet> i) (e / 2) \<subseteq> S"
   10.59 +        by (metis order_trans)
   10.60 +  qed (simp add: \<open>0 < e\<close>)
   10.61 +  then show "\<exists>e>0. ball x e \<subseteq> {s. s \<bullet> i \<in> S}"
   10.62 +    by (metis (no_types, lifting) \<open>0 < e\<close> \<open>open S\<close> half_gt_zero_iff mem_Collect_eq mem_ball open_contains_ball_eq subsetI)
   10.63 +qed
   10.64 +
   10.65 +proposition tendsto_componentwise_iff:
   10.66 +  fixes f :: "_ \<Rightarrow> 'b::euclidean_space"
   10.67 +  shows "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>i \<in> Basis. ((\<lambda>x. (f x \<bullet> i)) \<longlongrightarrow> (l \<bullet> i)) F)"
   10.68 +         (is "?lhs = ?rhs")
   10.69 +proof
   10.70 +  assume ?lhs
   10.71 +  then show ?rhs
   10.72 +    unfolding tendsto_def
   10.73 +    apply clarify
   10.74 +    apply (drule_tac x="{s. s \<bullet> i \<in> S}" in spec)
   10.75 +    apply (auto simp: open_preimage_inner)
   10.76 +    done
   10.77 +next
   10.78 +  assume R: ?rhs
   10.79 +  then have "\<And>e. e > 0 \<Longrightarrow> \<forall>i\<in>Basis. \<forall>\<^sub>F x in F. dist (f x \<bullet> i) (l \<bullet> i) < e"
   10.80 +    unfolding tendsto_iff by blast
   10.81 +  then have R': "\<And>e. e > 0 \<Longrightarrow> \<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e"
   10.82 +      by (simp add: eventually_ball_finite_distrib [symmetric])
   10.83 +  show ?lhs
   10.84 +  unfolding tendsto_iff
   10.85 +  proof clarify
   10.86 +    fix e::real
   10.87 +    assume "0 < e"
   10.88 +    have *: "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e"
   10.89 +             if "\<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / real DIM('b)" for x
   10.90 +    proof -
   10.91 +      have "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis \<le> setsum (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis"
   10.92 +        by (simp add: setL2_le_setsum)
   10.93 +      also have "... < DIM('b) * (e / real DIM('b))"
   10.94 +        apply (rule setsum_bounded_above_strict)
   10.95 +        using that by auto
   10.96 +      also have "... = e"
   10.97 +        by (simp add: field_simps)
   10.98 +      finally show "setL2 (\<lambda>i. dist (f x \<bullet> i) (l \<bullet> i)) Basis < e" .
   10.99 +    qed
  10.100 +    have "\<forall>\<^sub>F x in F. \<forall>i\<in>Basis. dist (f x \<bullet> i) (l \<bullet> i) < e / DIM('b)"
  10.101 +      apply (rule R')
  10.102 +      using \<open>0 < e\<close> by simp
  10.103 +    then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
  10.104 +      apply (rule eventually_mono)
  10.105 +      apply (subst euclidean_dist_l2)
  10.106 +      using * by blast
  10.107 +  qed
  10.108 +qed
  10.109 +
  10.110 +
  10.111 +corollary continuous_componentwise:
  10.112 +   "continuous F f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous F (\<lambda>x. (f x \<bullet> i)))"
  10.113 +by (simp add: continuous_def tendsto_componentwise_iff [symmetric])
  10.114 +
  10.115 +corollary continuous_on_componentwise:
  10.116 +  fixes S :: "'a :: t2_space set"
  10.117 +  shows "continuous_on S f \<longleftrightarrow> (\<forall>i \<in> Basis. continuous_on S (\<lambda>x. (f x \<bullet> i)))"
  10.118 +  apply (simp add: continuous_on_eq_continuous_within)
  10.119 +  using continuous_componentwise by blast
  10.120 +
  10.121 +lemma linear_componentwise_iff:
  10.122 +     "(linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. linear (\<lambda>x. f' x \<bullet> i))"
  10.123 +  apply (auto simp: linear_iff inner_left_distrib)
  10.124 +   apply (metis inner_left_distrib euclidean_eq_iff)
  10.125 +  by (metis euclidean_eqI inner_scaleR_left)
  10.126 +
  10.127 +lemma bounded_linear_componentwise_iff:
  10.128 +     "(bounded_linear f') \<longleftrightarrow> (\<forall>i\<in>Basis. bounded_linear (\<lambda>x. f' x \<bullet> i))"
  10.129 +     (is "?lhs = ?rhs")
  10.130 +proof
  10.131 +  assume ?lhs then show ?rhs
  10.132 +    by (simp add: bounded_linear_inner_left_comp)
  10.133 +next
  10.134 +  assume ?rhs
  10.135 +  then have "(\<forall>i\<in>Basis. \<exists>K. \<forall>x. \<bar>f' x \<bullet> i\<bar> \<le> norm x * K)" "linear f'"
  10.136 +    by (auto simp: bounded_linear_def bounded_linear_axioms_def linear_componentwise_iff [symmetric] ball_conj_distrib)
  10.137 +  then obtain F where F: "\<And>i x. i \<in> Basis \<Longrightarrow> \<bar>f' x \<bullet> i\<bar> \<le> norm x * F i"
  10.138 +    by metis
  10.139 +  have "norm (f' x) \<le> norm x * setsum F Basis" for x
  10.140 +  proof -
  10.141 +    have "norm (f' x) \<le> (\<Sum>i\<in>Basis. \<bar>f' x \<bullet> i\<bar>)"
  10.142 +      by (rule norm_le_l1)
  10.143 +    also have "... \<le> (\<Sum>i\<in>Basis. norm x * F i)"
  10.144 +      by (metis F setsum_mono)
  10.145 +    also have "... = norm x * setsum F Basis"
  10.146 +      by (simp add: setsum_distrib_left)
  10.147 +    finally show ?thesis .
  10.148 +  qed
  10.149 +  then show ?lhs
  10.150 +    by (force simp: bounded_linear_def bounded_linear_axioms_def \<open>linear f'\<close>)
  10.151 +qed
  10.152 +
  10.153 +
  10.154  no_notation
  10.155    eucl_less (infix "<e" 50)
  10.156  
    11.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Sep 21 16:59:51 2016 +0100
    11.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Sep 22 15:44:47 2016 +0100
    11.3 @@ -3,7 +3,7 @@
    11.4  text\<open>By L C Paulson (2015)\<close>
    11.5  
    11.6  theory Weierstrass_Theorems
    11.7 -imports Uniform_Limit Path_Connected
    11.8 +imports Uniform_Limit Path_Connected Derivative
    11.9  begin
   11.10  
   11.11  subsection \<open>Bernstein polynomials\<close>
   11.12 @@ -171,13 +171,13 @@
   11.13  DOI: 10.2307/2043993  http://www.jstor.org/stable/2043993\<close>
   11.14  
   11.15  locale function_ring_on =
   11.16 -  fixes R :: "('a::t2_space \<Rightarrow> real) set" and s :: "'a set"
   11.17 -  assumes compact: "compact s"
   11.18 -  assumes continuous: "f \<in> R \<Longrightarrow> continuous_on s f"
   11.19 +  fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set"
   11.20 +  assumes compact: "compact S"
   11.21 +  assumes continuous: "f \<in> R \<Longrightarrow> continuous_on S f"
   11.22    assumes add: "f \<in> R \<Longrightarrow> g \<in> R \<Longrightarrow> (\<lambda>x. f x + g x) \<in> R"
   11.23    assumes mult: "f \<in> R \<Longrightarrow> g \<in> R \<Longrightarrow> (\<lambda>x. f x * g x) \<in> R"
   11.24    assumes const: "(\<lambda>_. c) \<in> R"
   11.25 -  assumes separable: "x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x \<noteq> y \<Longrightarrow> \<exists>f\<in>R. f x \<noteq> f y"
   11.26 +  assumes separable: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> \<exists>f\<in>R. f x \<noteq> f y"
   11.27  
   11.28  begin
   11.29    lemma minus: "f \<in> R \<Longrightarrow> (\<lambda>x. - f x) \<in> R"
   11.30 @@ -196,24 +196,24 @@
   11.31      by (induct I rule: finite_induct; simp add: const mult)
   11.32  
   11.33    definition normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real"
   11.34 -    where "normf f \<equiv> SUP x:s. \<bar>f x\<bar>"
   11.35 +    where "normf f \<equiv> SUP x:S. \<bar>f x\<bar>"
   11.36  
   11.37 -  lemma normf_upper: "\<lbrakk>continuous_on s f; x \<in> s\<rbrakk> \<Longrightarrow> \<bar>f x\<bar> \<le> normf f"
   11.38 +  lemma normf_upper: "\<lbrakk>continuous_on S f; x \<in> S\<rbrakk> \<Longrightarrow> \<bar>f x\<bar> \<le> normf f"
   11.39      apply (simp add: normf_def)
   11.40      apply (rule cSUP_upper, assumption)
   11.41      by (simp add: bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs)
   11.42  
   11.43 -  lemma normf_least: "s \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> s \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M"
   11.44 +  lemma normf_least: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M"
   11.45      by (simp add: normf_def cSUP_least)
   11.46  
   11.47  end
   11.48  
   11.49  lemma (in function_ring_on) one:
   11.50 -  assumes U: "open U" and t0: "t0 \<in> s" "t0 \<in> U" and t1: "t1 \<in> s-U"
   11.51 -    shows "\<exists>V. open V \<and> t0 \<in> V \<and> s \<inter> V \<subseteq> U \<and>
   11.52 -               (\<forall>e>0. \<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>t \<in> s \<inter> V. f t < e) \<and> (\<forall>t \<in> s - U. f t > 1 - e))"
   11.53 +  assumes U: "open U" and t0: "t0 \<in> S" "t0 \<in> U" and t1: "t1 \<in> S-U"
   11.54 +    shows "\<exists>V. open V \<and> t0 \<in> V \<and> S \<inter> V \<subseteq> U \<and>
   11.55 +               (\<forall>e>0. \<exists>f \<in> R. f ` S \<subseteq> {0..1} \<and> (\<forall>t \<in> S \<inter> V. f t < e) \<and> (\<forall>t \<in> S - U. f t > 1 - e))"
   11.56  proof -
   11.57 -  have "\<exists>pt \<in> R. pt t0 = 0 \<and> pt t > 0 \<and> pt ` s \<subseteq> {0..1}" if t: "t \<in> s - U" for t
   11.58 +  have "\<exists>pt \<in> R. pt t0 = 0 \<and> pt t > 0 \<and> pt ` S \<subseteq> {0..1}" if t: "t \<in> S - U" for t
   11.59    proof -
   11.60      have "t \<noteq> t0" using t t0 by auto
   11.61      then obtain g where g: "g \<in> R" "g t \<noteq> g t0"
   11.62 @@ -239,28 +239,28 @@
   11.63        by (simp add: p_def h_def)
   11.64      moreover have "p t > 0"
   11.65        using nfp ht2 by (simp add: p_def)
   11.66 -    moreover have "\<And>x. x \<in> s \<Longrightarrow> p x \<in> {0..1}"
   11.67 +    moreover have "\<And>x. x \<in> S \<Longrightarrow> p x \<in> {0..1}"
   11.68        using nfp normf_upper [OF continuous [OF hsq] ] by (auto simp: p_def)
   11.69 -    ultimately show "\<exists>pt \<in> R. pt t0 = 0 \<and> pt t > 0 \<and> pt ` s \<subseteq> {0..1}"
   11.70 +    ultimately show "\<exists>pt \<in> R. pt t0 = 0 \<and> pt t > 0 \<and> pt ` S \<subseteq> {0..1}"
   11.71        by auto
   11.72    qed
   11.73 -  then obtain pf where pf: "\<And>t. t \<in> s-U \<Longrightarrow> pf t \<in> R \<and> pf t t0 = 0 \<and> pf t t > 0"
   11.74 -                   and pf01: "\<And>t. t \<in> s-U \<Longrightarrow> pf t ` s \<subseteq> {0..1}"
   11.75 +  then obtain pf where pf: "\<And>t. t \<in> S-U \<Longrightarrow> pf t \<in> R \<and> pf t t0 = 0 \<and> pf t t > 0"
   11.76 +                   and pf01: "\<And>t. t \<in> S-U \<Longrightarrow> pf t ` S \<subseteq> {0..1}"
   11.77      by metis
   11.78 -  have com_sU: "compact (s-U)"
   11.79 +  have com_sU: "compact (S-U)"
   11.80      using compact closed_Int_compact U by (simp add: Diff_eq compact_Int_closed open_closed)
   11.81 -  have "\<And>t. t \<in> s-U \<Longrightarrow> \<exists>A. open A \<and> A \<inter> s = {x\<in>s. 0 < pf t x}"
   11.82 +  have "\<And>t. t \<in> S-U \<Longrightarrow> \<exists>A. open A \<and> A \<inter> S = {x\<in>S. 0 < pf t x}"
   11.83      apply (rule open_Collect_positive)
   11.84      by (metis pf continuous)
   11.85 -  then obtain Uf where Uf: "\<And>t. t \<in> s-U \<Longrightarrow> open (Uf t) \<and> (Uf t) \<inter> s = {x\<in>s. 0 < pf t x}"
   11.86 +  then obtain Uf where Uf: "\<And>t. t \<in> S-U \<Longrightarrow> open (Uf t) \<and> (Uf t) \<inter> S = {x\<in>S. 0 < pf t x}"
   11.87      by metis
   11.88 -  then have open_Uf: "\<And>t. t \<in> s-U \<Longrightarrow> open (Uf t)"
   11.89 +  then have open_Uf: "\<And>t. t \<in> S-U \<Longrightarrow> open (Uf t)"
   11.90      by blast
   11.91 -  have tUft: "\<And>t. t \<in> s-U \<Longrightarrow> t \<in> Uf t"
   11.92 +  have tUft: "\<And>t. t \<in> S-U \<Longrightarrow> t \<in> Uf t"
   11.93      using pf Uf by blast
   11.94 -  then have *: "s-U \<subseteq> (\<Union>x \<in> s-U. Uf x)"
   11.95 +  then have *: "S-U \<subseteq> (\<Union>x \<in> S-U. Uf x)"
   11.96      by blast
   11.97 -  obtain subU where subU: "subU \<subseteq> s - U" "finite subU" "s - U \<subseteq> (\<Union>x \<in> subU. Uf x)"
   11.98 +  obtain subU where subU: "subU \<subseteq> S - U" "finite subU" "S - U \<subseteq> (\<Union>x \<in> subU. Uf x)"
   11.99      by (blast intro: that open_Uf compactE_image [OF com_sU _ *])
  11.100    then have [simp]: "subU \<noteq> {}"
  11.101      using t1 by auto
  11.102 @@ -271,7 +271,7 @@
  11.103      unfolding p_def using subU pf by (fast intro: pf const mult setsum)
  11.104    have pt0 [simp]: "p t0 = 0"
  11.105      using subU pf by (auto simp: p_def intro: setsum.neutral)
  11.106 -  have pt_pos: "p t > 0" if t: "t \<in> s-U" for t
  11.107 +  have pt_pos: "p t > 0" if t: "t \<in> S-U" for t
  11.108    proof -
  11.109      obtain i where i: "i \<in> subU" "t \<in> Uf i" using subU t by blast
  11.110      show ?thesis
  11.111 @@ -282,7 +282,7 @@
  11.112        apply (force elim!: subsetCE)
  11.113        done
  11.114    qed
  11.115 -  have p01: "p x \<in> {0..1}" if t: "x \<in> s" for x
  11.116 +  have p01: "p x \<in> {0..1}" if t: "x \<in> S" for x
  11.117    proof -
  11.118      have "0 \<le> p x"
  11.119        using subU cardp t
  11.120 @@ -297,26 +297,26 @@
  11.121      ultimately show ?thesis
  11.122        by auto
  11.123    qed
  11.124 -  have "compact (p ` (s-U))"
  11.125 +  have "compact (p ` (S-U))"
  11.126      by (meson Diff_subset com_sU compact_continuous_image continuous continuous_on_subset pR)
  11.127 -  then have "open (- (p ` (s-U)))"
  11.128 +  then have "open (- (p ` (S-U)))"
  11.129      by (simp add: compact_imp_closed open_Compl)
  11.130 -  moreover have "0 \<in> - (p ` (s-U))"
  11.131 +  moreover have "0 \<in> - (p ` (S-U))"
  11.132      by (metis (no_types) ComplI image_iff not_less_iff_gr_or_eq pt_pos)
  11.133 -  ultimately obtain delta0 where delta0: "delta0 > 0" "ball 0 delta0 \<subseteq> - (p ` (s-U))"
  11.134 +  ultimately obtain delta0 where delta0: "delta0 > 0" "ball 0 delta0 \<subseteq> - (p ` (S-U))"
  11.135      by (auto simp: elim!: openE)
  11.136 -  then have pt_delta: "\<And>x. x \<in> s-U \<Longrightarrow> p x \<ge> delta0"
  11.137 +  then have pt_delta: "\<And>x. x \<in> S-U \<Longrightarrow> p x \<ge> delta0"
  11.138      by (force simp: ball_def dist_norm dest: p01)
  11.139    define \<delta> where "\<delta> = delta0/2"
  11.140    have "delta0 \<le> 1" using delta0 p01 [of t1] t1
  11.141        by (force simp: ball_def dist_norm dest: p01)
  11.142    with delta0 have \<delta>01: "0 < \<delta>" "\<delta> < 1"
  11.143      by (auto simp: \<delta>_def)
  11.144 -  have pt_\<delta>: "\<And>x. x \<in> s-U \<Longrightarrow> p x \<ge> \<delta>"
  11.145 +  have pt_\<delta>: "\<And>x. x \<in> S-U \<Longrightarrow> p x \<ge> \<delta>"
  11.146      using pt_delta delta0 by (force simp: \<delta>_def)
  11.147 -  have "\<exists>A. open A \<and> A \<inter> s = {x\<in>s. p x < \<delta>/2}"
  11.148 +  have "\<exists>A. open A \<and> A \<inter> S = {x\<in>S. p x < \<delta>/2}"
  11.149      by (rule open_Collect_less_Int [OF continuous [OF pR] continuous_on_const])
  11.150 -  then obtain V where V: "open V" "V \<inter> s = {x\<in>s. p x < \<delta>/2}"
  11.151 +  then obtain V where V: "open V" "V \<inter> S = {x\<in>S. p x < \<delta>/2}"
  11.152      by blast
  11.153    define k where "k = nat\<lfloor>1/\<delta>\<rfloor> + 1"
  11.154    have "k>0"  by (simp add: k_def)
  11.155 @@ -334,12 +334,12 @@
  11.156    define q where [abs_def]: "q n t = (1 - p t ^ n) ^ (k^n)" for n t
  11.157    have qR: "q n \<in> R" for n
  11.158      by (simp add: q_def const diff power pR)
  11.159 -  have q01: "\<And>n t. t \<in> s \<Longrightarrow> q n t \<in> {0..1}"
  11.160 +  have q01: "\<And>n t. t \<in> S \<Longrightarrow> q n t \<in> {0..1}"
  11.161      using p01 by (simp add: q_def power_le_one algebra_simps)
  11.162    have qt0 [simp]: "\<And>n. n>0 \<Longrightarrow> q n t0 = 1"
  11.163      using t0 pf by (simp add: q_def power_0_left)
  11.164    { fix t and n::nat
  11.165 -    assume t: "t \<in> s \<inter> V"
  11.166 +    assume t: "t \<in> S \<inter> V"
  11.167      with \<open>k>0\<close> V have "k * p t < k * \<delta> / 2"
  11.168         by force
  11.169      then have "1 - (k * \<delta> / 2)^n \<le> 1 - (k * p t)^n"
  11.170 @@ -351,7 +351,7 @@
  11.171      finally have "1 - (k * \<delta> / 2) ^ n \<le> q n t" .
  11.172    } note limitV = this
  11.173    { fix t and n::nat
  11.174 -    assume t: "t \<in> s - U"
  11.175 +    assume t: "t \<in> S - U"
  11.176      with \<open>k>0\<close> U have "k * \<delta> \<le> k * p t"
  11.177        by (simp add: pt_\<delta>)
  11.178      with k\<delta> have kpt: "1 < k * p t"
  11.179 @@ -406,20 +406,20 @@
  11.180      done
  11.181    { fix t and e::real
  11.182      assume "e>0"
  11.183 -    have "t \<in> s \<inter> V \<Longrightarrow> 1 - q (NN e) t < e" "t \<in> s - U \<Longrightarrow> q (NN e) t < e"
  11.184 +    have "t \<in> S \<inter> V \<Longrightarrow> 1 - q (NN e) t < e" "t \<in> S - U \<Longrightarrow> q (NN e) t < e"
  11.185      proof -
  11.186 -      assume t: "t \<in> s \<inter> V"
  11.187 +      assume t: "t \<in> S \<inter> V"
  11.188        show "1 - q (NN e) t < e"
  11.189          by (metis add.commute diff_le_eq not_le limitV [OF t] less_le_trans [OF NN1 [OF \<open>e>0\<close>]])
  11.190      next
  11.191 -      assume t: "t \<in> s - U"
  11.192 +      assume t: "t \<in> S - U"
  11.193        show "q (NN e) t < e"
  11.194        using  limitNonU [OF t] less_le_trans [OF NN0 [OF \<open>e>0\<close>]] not_le by blast
  11.195      qed
  11.196 -  } then have "\<And>e. e > 0 \<Longrightarrow> \<exists>f\<in>R. f ` s \<subseteq> {0..1} \<and> (\<forall>t \<in> s \<inter> V. f t < e) \<and> (\<forall>t \<in> s - U. 1 - e < f t)"
  11.197 +  } then have "\<And>e. e > 0 \<Longrightarrow> \<exists>f\<in>R. f ` S \<subseteq> {0..1} \<and> (\<forall>t \<in> S \<inter> V. f t < e) \<and> (\<forall>t \<in> S - U. 1 - e < f t)"
  11.198      using q01
  11.199      by (rule_tac x="\<lambda>x. 1 - q (NN e) x" in bexI) (auto simp: algebra_simps intro: diff const qR)
  11.200 -  moreover have t0V: "t0 \<in> V"  "s \<inter> V \<subseteq> U"
  11.201 +  moreover have t0V: "t0 \<in> V"  "S \<inter> V \<subseteq> U"
  11.202      using pt_\<delta> t0 U V \<delta>01  by fastforce+
  11.203    ultimately show ?thesis using V t0V
  11.204      by blast
  11.205 @@ -427,23 +427,23 @@
  11.206  
  11.207  text\<open>Non-trivial case, with @{term A} and @{term B} both non-empty\<close>
  11.208  lemma (in function_ring_on) two_special:
  11.209 -  assumes A: "closed A" "A \<subseteq> s" "a \<in> A"
  11.210 -      and B: "closed B" "B \<subseteq> s" "b \<in> B"
  11.211 +  assumes A: "closed A" "A \<subseteq> S" "a \<in> A"
  11.212 +      and B: "closed B" "B \<subseteq> S" "b \<in> B"
  11.213        and disj: "A \<inter> B = {}"
  11.214        and e: "0 < e" "e < 1"
  11.215 -    shows "\<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> A. f x < e) \<and> (\<forall>x \<in> B. f x > 1 - e)"
  11.216 +    shows "\<exists>f \<in> R. f ` S \<subseteq> {0..1} \<and> (\<forall>x \<in> A. f x < e) \<and> (\<forall>x \<in> B. f x > 1 - e)"
  11.217  proof -
  11.218    { fix w
  11.219      assume "w \<in> A"
  11.220 -    then have "open ( - B)" "b \<in> s" "w \<notin> B" "w \<in> s"
  11.221 +    then have "open ( - B)" "b \<in> S" "w \<notin> B" "w \<in> S"
  11.222        using assms by auto
  11.223 -    then have "\<exists>V. open V \<and> w \<in> V \<and> s \<inter> V \<subseteq> -B \<and>
  11.224 -               (\<forall>e>0. \<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> s \<inter> V. f x < e) \<and> (\<forall>x \<in> s \<inter> B. f x > 1 - e))"
  11.225 +    then have "\<exists>V. open V \<and> w \<in> V \<and> S \<inter> V \<subseteq> -B \<and>
  11.226 +               (\<forall>e>0. \<exists>f \<in> R. f ` S \<subseteq> {0..1} \<and> (\<forall>x \<in> S \<inter> V. f x < e) \<and> (\<forall>x \<in> S \<inter> B. f x > 1 - e))"
  11.227        using one [of "-B" w b] assms \<open>w \<in> A\<close> by simp
  11.228    }
  11.229    then obtain Vf where Vf:
  11.230 -         "\<And>w. w \<in> A \<Longrightarrow> open (Vf w) \<and> w \<in> Vf w \<and> s \<inter> Vf w \<subseteq> -B \<and>
  11.231 -                         (\<forall>e>0. \<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> s \<inter> Vf w. f x < e) \<and> (\<forall>x \<in> s \<inter> B. f x > 1 - e))"
  11.232 +         "\<And>w. w \<in> A \<Longrightarrow> open (Vf w) \<and> w \<in> Vf w \<and> S \<inter> Vf w \<subseteq> -B \<and>
  11.233 +                         (\<forall>e>0. \<exists>f \<in> R. f ` S \<subseteq> {0..1} \<and> (\<forall>x \<in> S \<inter> Vf w. f x < e) \<and> (\<forall>x \<in> S \<inter> B. f x > 1 - e))"
  11.234      by metis
  11.235    then have open_Vf: "\<And>w. w \<in> A \<Longrightarrow> open (Vf w)"
  11.236      by blast
  11.237 @@ -459,17 +459,17 @@
  11.238      using \<open>a \<in> A\<close> by auto
  11.239    then have cardp: "card subA > 0" using subA
  11.240      by (simp add: card_gt_0_iff)
  11.241 -  have "\<And>w. w \<in> A \<Longrightarrow> \<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> s \<inter> Vf w. f x < e / card subA) \<and> (\<forall>x \<in> s \<inter> B. f x > 1 - e / card subA)"
  11.242 +  have "\<And>w. w \<in> A \<Longrightarrow> \<exists>f \<in> R. f ` S \<subseteq> {0..1} \<and> (\<forall>x \<in> S \<inter> Vf w. f x < e / card subA) \<and> (\<forall>x \<in> S \<inter> B. f x > 1 - e / card subA)"
  11.243      using Vf e cardp by simp
  11.244    then obtain ff where ff:
  11.245 -         "\<And>w. w \<in> A \<Longrightarrow> ff w \<in> R \<and> ff w ` s \<subseteq> {0..1} \<and>
  11.246 -                         (\<forall>x \<in> s \<inter> Vf w. ff w x < e / card subA) \<and> (\<forall>x \<in> s \<inter> B. ff w x > 1 - e / card subA)"
  11.247 +         "\<And>w. w \<in> A \<Longrightarrow> ff w \<in> R \<and> ff w ` S \<subseteq> {0..1} \<and>
  11.248 +                         (\<forall>x \<in> S \<inter> Vf w. ff w x < e / card subA) \<and> (\<forall>x \<in> S \<inter> B. ff w x > 1 - e / card subA)"
  11.249      by metis
  11.250    define pff where [abs_def]: "pff x = (\<Prod>w \<in> subA. ff w x)" for x
  11.251    have pffR: "pff \<in> R"
  11.252      unfolding pff_def using subA ff by (auto simp: intro: setprod)
  11.253    moreover
  11.254 -  have pff01: "pff x \<in> {0..1}" if t: "x \<in> s" for x
  11.255 +  have pff01: "pff x \<in> {0..1}" if t: "x \<in> S" for x
  11.256    proof -
  11.257      have "0 \<le> pff x"
  11.258        using subA cardp t
  11.259 @@ -486,7 +486,7 @@
  11.260    qed
  11.261    moreover
  11.262    { fix v x
  11.263 -    assume v: "v \<in> subA" and x: "x \<in> Vf v" "x \<in> s"
  11.264 +    assume v: "v \<in> subA" and x: "x \<in> Vf v" "x \<in> S"
  11.265      from subA v have "pff x = ff v x * (\<Prod>w \<in> subA - {v}. ff w x)"
  11.266        unfolding pff_def  by (metis setprod.remove)
  11.267      also have "... \<le> ff v x * 1"
  11.268 @@ -509,7 +509,7 @@
  11.269    moreover
  11.270    { fix x
  11.271      assume x: "x \<in> B"
  11.272 -    then have "x \<in> s"
  11.273 +    then have "x \<in> S"
  11.274        using B by auto
  11.275      have "1 - e \<le> (1 - e / card subA) ^ card subA"
  11.276        using Bernoulli_inequality [of "-e / card subA" "card subA"] e cardp
  11.277 @@ -532,11 +532,11 @@
  11.278  qed
  11.279  
  11.280  lemma (in function_ring_on) two:
  11.281 -  assumes A: "closed A" "A \<subseteq> s"
  11.282 -      and B: "closed B" "B \<subseteq> s"
  11.283 +  assumes A: "closed A" "A \<subseteq> S"
  11.284 +      and B: "closed B" "B \<subseteq> S"
  11.285        and disj: "A \<inter> B = {}"
  11.286        and e: "0 < e" "e < 1"
  11.287 -    shows "\<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> A. f x < e) \<and> (\<forall>x \<in> B. f x > 1 - e)"
  11.288 +    shows "\<exists>f \<in> R. f ` S \<subseteq> {0..1} \<and> (\<forall>x \<in> A. f x < e) \<and> (\<forall>x \<in> B. f x > 1 - e)"
  11.289  proof (cases "A \<noteq> {} \<and> B \<noteq> {}")
  11.290    case True then show ?thesis
  11.291      apply (simp add: ex_in_conv [symmetric])
  11.292 @@ -556,57 +556,57 @@
  11.293  
  11.294  text\<open>The special case where @{term f} is non-negative and @{term"e<1/3"}\<close>
  11.295  lemma (in function_ring_on) Stone_Weierstrass_special:
  11.296 -  assumes f: "continuous_on s f" and fpos: "\<And>x. x \<in> s \<Longrightarrow> f x \<ge> 0"
  11.297 +  assumes f: "continuous_on S f" and fpos: "\<And>x. x \<in> S \<Longrightarrow> f x \<ge> 0"
  11.298        and e: "0 < e" "e < 1/3"
  11.299 -  shows "\<exists>g \<in> R. \<forall>x\<in>s. \<bar>f x - g x\<bar> < 2*e"
  11.300 +  shows "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>f x - g x\<bar> < 2*e"
  11.301  proof -
  11.302    define n where "n = 1 + nat \<lceil>normf f / e\<rceil>"
  11.303 -  define A where "A j = {x \<in> s. f x \<le> (j - 1/3)*e}" for j :: nat
  11.304 -  define B where "B j = {x \<in> s. f x \<ge> (j + 1/3)*e}" for j :: nat
  11.305 +  define A where "A j = {x \<in> S. f x \<le> (j - 1/3)*e}" for j :: nat
  11.306 +  define B where "B j = {x \<in> S. f x \<ge> (j + 1/3)*e}" for j :: nat
  11.307    have ngt: "(n-1) * e \<ge> normf f" "n\<ge>1"
  11.308      using e
  11.309      apply (simp_all add: n_def field_simps of_nat_Suc)
  11.310      by (metis real_nat_ceiling_ge mult.commute not_less pos_less_divide_eq)
  11.311 -  then have ge_fx: "(n-1) * e \<ge> f x" if "x \<in> s" for x
  11.312 +  then have ge_fx: "(n-1) * e \<ge> f x" if "x \<in> S" for x
  11.313      using f normf_upper that by fastforce
  11.314    { fix j
  11.315 -    have A: "closed (A j)" "A j \<subseteq> s"
  11.316 +    have A: "closed (A j)" "A j \<subseteq> S"
  11.317        apply (simp_all add: A_def Collect_restrict)
  11.318        apply (rule continuous_on_closed_Collect_le [OF f continuous_on_const])
  11.319        apply (simp add: compact compact_imp_closed)
  11.320        done
  11.321 -    have B: "closed (B j)" "B j \<subseteq> s"
  11.322 +    have B: "closed (B j)" "B j \<subseteq> S"
  11.323        apply (simp_all add: B_def Collect_restrict)
  11.324        apply (rule continuous_on_closed_Collect_le [OF continuous_on_const f])
  11.325        apply (simp add: compact compact_imp_closed)
  11.326        done
  11.327      have disj: "(A j) \<inter> (B j) = {}"
  11.328        using e by (auto simp: A_def B_def field_simps)
  11.329 -    have "\<exists>f \<in> R. f ` s \<subseteq> {0..1} \<and> (\<forall>x \<in> A j. f x < e/n) \<and> (\<forall>x \<in> B j. f x > 1 - e/n)"
  11.330 +    have "\<exists>f \<in> R. f ` S \<subseteq> {0..1} \<and> (\<forall>x \<in> A j. f x < e/n) \<and> (\<forall>x \<in> B j. f x > 1 - e/n)"
  11.331        apply (rule two)
  11.332        using e A B disj ngt
  11.333        apply simp_all
  11.334        done
  11.335    }
  11.336 -  then obtain xf where xfR: "\<And>j. xf j \<in> R" and xf01: "\<And>j. xf j ` s \<subseteq> {0..1}"
  11.337 +  then obtain xf where xfR: "\<And>j. xf j \<in> R" and xf01: "\<And>j. xf j ` S \<subseteq> {0..1}"
  11.338                     and xfA: "\<And>x j. x \<in> A j \<Longrightarrow> xf j x < e/n"
  11.339                     and xfB: "\<And>x j. x \<in> B j \<Longrightarrow> xf j x > 1 - e/n"
  11.340      by metis
  11.341    define g where [abs_def]: "g x = e * (\<Sum>i\<le>n. xf i x)" for x
  11.342    have gR: "g \<in> R"
  11.343      unfolding g_def by (fast intro: mult const setsum xfR)
  11.344 -  have gge0: "\<And>x. x \<in> s \<Longrightarrow> g x \<ge> 0"
  11.345 +  have gge0: "\<And>x. x \<in> S \<Longrightarrow> g x \<ge> 0"
  11.346      using e xf01 by (simp add: g_def zero_le_mult_iff image_subset_iff setsum_nonneg)
  11.347    have A0: "A 0 = {}"
  11.348      using fpos e by (fastforce simp: A_def)
  11.349 -  have An: "A n = s"
  11.350 +  have An: "A n = S"
  11.351      using e ngt f normf_upper by (fastforce simp: A_def field_simps of_nat_diff)
  11.352    have Asub: "A j \<subseteq> A i" if "i\<ge>j" for i j
  11.353      using e that apply (clarsimp simp: A_def)
  11.354      apply (erule order_trans, simp)
  11.355      done
  11.356    { fix t
  11.357 -    assume t: "t \<in> s"
  11.358 +    assume t: "t \<in> S"
  11.359      define j where "j = (LEAST j. t \<in> A j)"
  11.360      have jn: "j \<le> n"
  11.361        using t An by (simp add: Least_le j_def)
  11.362 @@ -701,16 +701,16 @@
  11.363  
  11.364  text\<open>The ``unpretentious'' formulation\<close>
  11.365  lemma (in function_ring_on) Stone_Weierstrass_basic:
  11.366 -  assumes f: "continuous_on s f" and e: "e > 0"
  11.367 -  shows "\<exists>g \<in> R. \<forall>x\<in>s. \<bar>f x - g x\<bar> < e"
  11.368 +  assumes f: "continuous_on S f" and e: "e > 0"
  11.369 +  shows "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>f x - g x\<bar> < e"
  11.370  proof -
  11.371 -  have "\<exists>g \<in> R. \<forall>x\<in>s. \<bar>(f x + normf f) - g x\<bar> < 2 * min (e/2) (1/4)"
  11.372 +  have "\<exists>g \<in> R. \<forall>x\<in>S. \<bar>(f x + normf f) - g x\<bar> < 2 * min (e/2) (1/4)"
  11.373      apply (rule Stone_Weierstrass_special)
  11.374      apply (rule Limits.continuous_on_add [OF f Topological_Spaces.continuous_on_const])
  11.375      using normf_upper [OF f] apply force
  11.376      apply (simp add: e, linarith)
  11.377      done
  11.378 -  then obtain g where "g \<in> R" "\<forall>x\<in>s. \<bar>g x - (f x + normf f)\<bar> < e"
  11.379 +  then obtain g where "g \<in> R" "\<forall>x\<in>S. \<bar>g x - (f x + normf f)\<bar> < e"
  11.380      by force
  11.381    then show ?thesis
  11.382      apply (rule_tac x="\<lambda>x. g x - normf f" in bexI)
  11.383 @@ -720,16 +720,16 @@
  11.384  
  11.385  
  11.386  theorem (in function_ring_on) Stone_Weierstrass:
  11.387 -  assumes f: "continuous_on s f"
  11.388 -  shows "\<exists>F\<in>UNIV \<rightarrow> R. LIM n sequentially. F n :> uniformly_on s f"
  11.389 +  assumes f: "continuous_on S f"
  11.390 +  shows "\<exists>F\<in>UNIV \<rightarrow> R. LIM n sequentially. F n :> uniformly_on S f"
  11.391  proof -
  11.392    { fix e::real
  11.393      assume e: "0 < e"
  11.394      then obtain N::nat where N: "0 < N" "0 < inverse N" "inverse N < e"
  11.395        by (auto simp: real_arch_inverse [of e])
  11.396      { fix n :: nat and x :: 'a and g :: "'a \<Rightarrow> real"
  11.397 -      assume n: "N \<le> n"  "\<forall>x\<in>s. \<bar>f x - g x\<bar> < 1 / (1 + real n)"
  11.398 -      assume x: "x \<in> s"
  11.399 +      assume n: "N \<le> n"  "\<forall>x\<in>S. \<bar>f x - g x\<bar> < 1 / (1 + real n)"
  11.400 +      assume x: "x \<in> S"
  11.401        have "\<not> real (Suc n) < inverse e"
  11.402          using \<open>N \<le> n\<close> N using less_imp_inverse_less by force
  11.403        then have "1 / (1 + real n) \<le> e"
  11.404 @@ -737,13 +737,13 @@
  11.405        then have "\<bar>f x - g x\<bar> < e"
  11.406          using n(2) x by auto
  11.407      } note * = this
  11.408 -    have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>s. \<bar>f x - (SOME g. g \<in> R \<and> (\<forall>x\<in>s. \<bar>f x - g x\<bar> < 1 / (1 + real n))) x\<bar> < e"
  11.409 +    have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>S. \<bar>f x - (SOME g. g \<in> R \<and> (\<forall>x\<in>S. \<bar>f x - g x\<bar> < 1 / (1 + real n))) x\<bar> < e"
  11.410        apply (rule eventually_sequentiallyI [of N])
  11.411        apply (auto intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]] *)
  11.412        done
  11.413    } then
  11.414    show ?thesis
  11.415 -    apply (rule_tac x="\<lambda>n::nat. SOME g. g \<in> R \<and> (\<forall>x\<in>s. \<bar>f x - g x\<bar> < 1 / (1 + n))" in bexI)
  11.416 +    apply (rule_tac x="\<lambda>n::nat. SOME g. g \<in> R \<and> (\<forall>x\<in>S. \<bar>f x - g x\<bar> < 1 / (1 + n))" in bexI)
  11.417      prefer 2  apply (force intro: someI2_bex [OF Stone_Weierstrass_basic [OF f]])
  11.418      unfolding uniform_limit_iff
  11.419      apply (auto simp: dist_norm abs_minus_commute)
  11.420 @@ -752,21 +752,21 @@
  11.421  
  11.422  text\<open>A HOL Light formulation\<close>
  11.423  corollary Stone_Weierstrass_HOL:
  11.424 -  fixes R :: "('a::t2_space \<Rightarrow> real) set" and s :: "'a set"
  11.425 -  assumes "compact s"  "\<And>c. P(\<lambda>x. c::real)"
  11.426 -          "\<And>f. P f \<Longrightarrow> continuous_on s f"
  11.427 +  fixes R :: "('a::t2_space \<Rightarrow> real) set" and S :: "'a set"
  11.428 +  assumes "compact S"  "\<And>c. P(\<lambda>x. c::real)"
  11.429 +          "\<And>f. P f \<Longrightarrow> continuous_on S f"
  11.430            "\<And>f g. P(f) \<and> P(g) \<Longrightarrow> P(\<lambda>x. f x + g x)"  "\<And>f g. P(f) \<and> P(g) \<Longrightarrow> P(\<lambda>x. f x * g x)"
  11.431 -          "\<And>x y. x \<in> s \<and> y \<in> s \<and> ~(x = y) \<Longrightarrow> \<exists>f. P(f) \<and> ~(f x = f y)"
  11.432 -          "continuous_on s f"
  11.433 +          "\<And>x y. x \<in> S \<and> y \<in> S \<and> ~(x = y) \<Longrightarrow> \<exists>f. P(f) \<and> ~(f x = f y)"
  11.434 +          "continuous_on S f"
  11.435         "0 < e"
  11.436 -    shows "\<exists>g. P(g) \<and> (\<forall>x \<in> s. \<bar>f x - g x\<bar> < e)"
  11.437 +    shows "\<exists>g. P(g) \<and> (\<forall>x \<in> S. \<bar>f x - g x\<bar> < e)"
  11.438  proof -
  11.439    interpret PR: function_ring_on "Collect P"
  11.440      apply unfold_locales
  11.441      using assms
  11.442      by auto
  11.443    show ?thesis
  11.444 -    using PR.Stone_Weierstrass_basic [OF \<open>continuous_on s f\<close> \<open>0 < e\<close>]
  11.445 +    using PR.Stone_Weierstrass_basic [OF \<open>continuous_on S f\<close> \<open>0 < e\<close>]
  11.446      by blast
  11.447  qed
  11.448  
  11.449 @@ -994,7 +994,7 @@
  11.450  lemma continuous_on_polymonial_function:
  11.451    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
  11.452    assumes "polynomial_function f"
  11.453 -    shows "continuous_on s f"
  11.454 +    shows "continuous_on S f"
  11.455    using continuous_polymonial_function [OF assms] continuous_at_imp_continuous_on
  11.456    by blast
  11.457  
  11.458 @@ -1035,8 +1035,7 @@
  11.459  lemma has_vector_derivative_polynomial_function:
  11.460    fixes p :: "real \<Rightarrow> 'a::euclidean_space"
  11.461    assumes "polynomial_function p"
  11.462 -    shows "\<exists>p'. polynomial_function p' \<and>
  11.463 -                 (\<forall>x. (p has_vector_derivative (p' x)) (at x))"
  11.464 +  obtains p' where "polynomial_function p'" "\<And>x. (p has_vector_derivative (p' x)) (at x)"
  11.465  proof -
  11.466    { fix b :: 'a
  11.467      assume "b \<in> Basis"
  11.468 @@ -1057,9 +1056,10 @@
  11.469        "\<And>b x. b \<in> Basis \<Longrightarrow> ((\<lambda>u. (p u \<bullet> b) *\<^sub>R b) has_vector_derivative qf b x) (at x)"
  11.470      by metis
  11.471    show ?thesis
  11.472 +    apply (rule_tac p'="\<lambda>x. \<Sum>b\<in>Basis. qf b x" in that)
  11.473 +     apply (force intro: qf)
  11.474      apply (subst euclidean_representation_setsum_fun [of p, symmetric])
  11.475 -    apply (rule_tac x="\<lambda>x. \<Sum>b\<in>Basis. qf b x" in exI)
  11.476 -    apply (auto intro: has_vector_derivative_setsum qf)
  11.477 +     apply (auto intro: has_vector_derivative_setsum qf)
  11.478      done
  11.479  qed
  11.480  
  11.481 @@ -1081,8 +1081,8 @@
  11.482  
  11.483  lemma Stone_Weierstrass_real_polynomial_function:
  11.484    fixes f :: "'a::euclidean_space \<Rightarrow> real"
  11.485 -  assumes "compact s" "continuous_on s f" "0 < e"
  11.486 -    shows "\<exists>g. real_polynomial_function g \<and> (\<forall>x \<in> s. \<bar>f x - g x\<bar> < e)"
  11.487 +  assumes "compact S" "continuous_on S f" "0 < e"
  11.488 +  obtains g where "real_polynomial_function g" "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x - g x\<bar> < e"
  11.489  proof -
  11.490    interpret PR: function_ring_on "Collect real_polynomial_function"
  11.491      apply unfold_locales
  11.492 @@ -1090,27 +1090,27 @@
  11.493      apply (auto intro: real_polynomial_function_separable)
  11.494      done
  11.495    show ?thesis
  11.496 -    using PR.Stone_Weierstrass_basic [OF \<open>continuous_on s f\<close> \<open>0 < e\<close>]
  11.497 +    using PR.Stone_Weierstrass_basic [OF \<open>continuous_on S f\<close> \<open>0 < e\<close>] that
  11.498      by blast
  11.499  qed
  11.500  
  11.501  lemma Stone_Weierstrass_polynomial_function:
  11.502    fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  11.503 -  assumes s: "compact s"
  11.504 -      and f: "continuous_on s f"
  11.505 +  assumes S: "compact S"
  11.506 +      and f: "continuous_on S f"
  11.507        and e: "0 < e"
  11.508 -    shows "\<exists>g. polynomial_function g \<and> (\<forall>x \<in> s. norm(f x - g x) < e)"
  11.509 +    shows "\<exists>g. polynomial_function g \<and> (\<forall>x \<in> S. norm(f x - g x) < e)"
  11.510  proof -
  11.511    { fix b :: 'b
  11.512      assume "b \<in> Basis"
  11.513 -    have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> s. \<bar>f x \<bullet> b - p x\<bar> < e / DIM('b))"
  11.514 -      apply (rule exE [OF Stone_Weierstrass_real_polynomial_function [OF s _, of "\<lambda>x. f x \<bullet> b" "e / card Basis"]])
  11.515 +    have "\<exists>p. real_polynomial_function p \<and> (\<forall>x \<in> S. \<bar>f x \<bullet> b - p x\<bar> < e / DIM('b))"
  11.516 +      apply (rule exE [OF Stone_Weierstrass_real_polynomial_function [OF S _, of "\<lambda>x. f x \<bullet> b" "e / card Basis"]])
  11.517        using e f
  11.518        apply (auto simp: Euclidean_Space.DIM_positive intro: continuous_intros)
  11.519        done
  11.520    }
  11.521    then obtain pf where pf:
  11.522 -      "\<And>b. b \<in> Basis \<Longrightarrow> real_polynomial_function (pf b) \<and> (\<forall>x \<in> s. \<bar>f x \<bullet> b - pf b x\<bar> < e / DIM('b))"
  11.523 +      "\<And>b. b \<in> Basis \<Longrightarrow> real_polynomial_function (pf b) \<and> (\<forall>x \<in> S. \<bar>f x \<bullet> b - pf b x\<bar> < e / DIM('b))"
  11.524        apply (rule bchoice [rule_format, THEN exE])
  11.525        apply assumption
  11.526        apply (force simp add: intro: that)
  11.527 @@ -1120,12 +1120,12 @@
  11.528      by (simp add: polynomial_function_setsum polynomial_function_mult real_polynomial_function_eq)
  11.529    moreover
  11.530    { fix x
  11.531 -    assume "x \<in> s"
  11.532 +    assume "x \<in> S"
  11.533      have "norm (\<Sum>b\<in>Basis. (f x \<bullet> b) *\<^sub>R b - pf b x *\<^sub>R b) \<le> (\<Sum>b\<in>Basis. norm ((f x \<bullet> b) *\<^sub>R b - pf b x *\<^sub>R b))"
  11.534        by (rule norm_setsum)
  11.535      also have "... < of_nat DIM('b) * (e / DIM('b))"
  11.536        apply (rule setsum_bounded_above_strict)
  11.537 -      apply (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf \<open>x \<in> s\<close>)
  11.538 +      apply (simp add: Real_Vector_Spaces.scaleR_diff_left [symmetric] pf \<open>x \<in> S\<close>)
  11.539        apply (rule DIM_positive)
  11.540        done
  11.541      also have "... = e"
  11.542 @@ -1178,31 +1178,31 @@
  11.543  qed
  11.544  
  11.545  lemma connected_open_polynomial_connected:
  11.546 -  fixes s :: "'a::euclidean_space set"
  11.547 -  assumes s: "open s" "connected s"
  11.548 -      and "x \<in> s" "y \<in> s"
  11.549 -    shows "\<exists>g. polynomial_function g \<and> path_image g \<subseteq> s \<and>
  11.550 +  fixes S :: "'a::euclidean_space set"
  11.551 +  assumes S: "open S" "connected S"
  11.552 +      and "x \<in> S" "y \<in> S"
  11.553 +    shows "\<exists>g. polynomial_function g \<and> path_image g \<subseteq> S \<and>
  11.554                 pathstart g = x \<and> pathfinish g = y"
  11.555  proof -
  11.556 -  have "path_connected s" using assms
  11.557 +  have "path_connected S" using assms
  11.558      by (simp add: connected_open_path_connected)
  11.559 -  with \<open>x \<in> s\<close> \<open>y \<in> s\<close> obtain p where p: "path p" "path_image p \<subseteq> s" "pathstart p = x" "pathfinish p = y"
  11.560 +  with \<open>x \<in> S\<close> \<open>y \<in> S\<close> obtain p where p: "path p" "path_image p \<subseteq> S" "pathstart p = x" "pathfinish p = y"
  11.561      by (force simp: path_connected_def)
  11.562 -  have "\<exists>e. 0 < e \<and> (\<forall>x \<in> path_image p. ball x e \<subseteq> s)"
  11.563 -  proof (cases "s = UNIV")
  11.564 +  have "\<exists>e. 0 < e \<and> (\<forall>x \<in> path_image p. ball x e \<subseteq> S)"
  11.565 +  proof (cases "S = UNIV")
  11.566      case True then show ?thesis
  11.567        by (simp add: gt_ex)
  11.568    next
  11.569      case False
  11.570 -    then have "- s \<noteq> {}" by blast
  11.571 +    then have "- S \<noteq> {}" by blast
  11.572      then show ?thesis
  11.573 -      apply (rule_tac x="setdist (path_image p) (-s)" in exI)
  11.574 -      using s p
  11.575 +      apply (rule_tac x="setdist (path_image p) (-S)" in exI)
  11.576 +      using S p
  11.577        apply (simp add: setdist_gt_0_compact_closed compact_path_image open_closed)
  11.578 -      using setdist_le_dist [of _ "path_image p" _ "-s"]
  11.579 +      using setdist_le_dist [of _ "path_image p" _ "-S"]
  11.580        by fastforce
  11.581    qed
  11.582 -  then obtain e where "0 < e"and eb: "\<And>x. x \<in> path_image p \<Longrightarrow> ball x e \<subseteq> s"
  11.583 +  then obtain e where "0 < e"and eb: "\<And>x. x \<in> path_image p \<Longrightarrow> ball x e \<subseteq> S"
  11.584      by auto
  11.585    show ?thesis
  11.586      using path_approx_polynomial_function [OF \<open>path p\<close> \<open>0 < e\<close>]
  11.587 @@ -1213,6 +1213,179 @@
  11.588      done
  11.589  qed
  11.590  
  11.591 +lemma has_derivative_componentwise_within:
  11.592 +   "(f has_derivative f') (at a within S) \<longleftrightarrow>
  11.593 +    (\<forall>i \<in> Basis. ((\<lambda>x. f x \<bullet> i) has_derivative (\<lambda>x. f' x \<bullet> i)) (at a within S))"
  11.594 +  apply (simp add: has_derivative_within)
  11.595 +  apply (subst tendsto_componentwise_iff)
  11.596 +  apply (simp add: bounded_linear_componentwise_iff [symmetric] ball_conj_distrib)
  11.597 +  apply (simp add: algebra_simps)
  11.598 +  done
  11.599 +
  11.600 +lemma differentiable_componentwise_within:
  11.601 +   "f differentiable (at a within S) \<longleftrightarrow>
  11.602 +    (\<forall>i \<in> Basis. (\<lambda>x. f x \<bullet> i) differentiable at a within S)"
  11.603 +proof -
  11.604 +  { assume "\<forall>i\<in>Basis. \<exists>D. ((\<lambda>x. f x \<bullet> i) has_derivative D) (at a within S)"
  11.605 +    then obtain f' where f':
  11.606 +           "\<And>i. i \<in> Basis \<Longrightarrow> ((\<lambda>x. f x \<bullet> i) has_derivative f' i) (at a within S)"
  11.607 +      by metis
  11.608 +    have eq: "(\<lambda>x. (\<Sum>j\<in>Basis. f' j x *\<^sub>R j) \<bullet> i) = f' i" if "i \<in> Basis" for i
  11.609 +      using that by (simp add: inner_add_left inner_add_right)
  11.610 +    have "\<exists>D. \<forall>i\<in>Basis. ((\<lambda>x. f x \<bullet> i) has_derivative (\<lambda>x. D x \<bullet> i)) (at a within S)"
  11.611 +      apply (rule_tac x="\<lambda>x::'a. (\<Sum>j\<in>Basis. f' j x *\<^sub>R j) :: 'b" in exI)
  11.612 +      apply (simp add: eq f')
  11.613 +      done
  11.614 +  }
  11.615 +  then show ?thesis
  11.616 +    apply (simp add: differentiable_def)
  11.617 +    using has_derivative_componentwise_within
  11.618 +    by blast
  11.619 +qed
  11.620 +
  11.621 +lemma polynomial_function_inner [intro]:
  11.622 +  fixes i :: "'a::euclidean_space"
  11.623 +  shows "polynomial_function g \<Longrightarrow> polynomial_function (\<lambda>x. g x \<bullet> i)"
  11.624 +  apply (subst euclidean_representation [where x=i, symmetric])
  11.625 +  apply (force simp: inner_setsum_right polynomial_function_iff_Basis_inner polynomial_function_setsum)
  11.626 +  done
  11.627 +
  11.628 +text\<open> Differentiability of real and vector polynomial functions.\<close>
  11.629 +
  11.630 +lemma differentiable_at_real_polynomial_function:
  11.631 +   "real_polynomial_function f \<Longrightarrow> f differentiable (at a within S)"
  11.632 +  by (induction f rule: real_polynomial_function.induct)
  11.633 +     (simp_all add: bounded_linear_imp_differentiable)
  11.634 +
  11.635 +lemma differentiable_on_real_polynomial_function:
  11.636 +   "real_polynomial_function p \<Longrightarrow> p differentiable_on S"
  11.637 +by (simp add: differentiable_at_imp_differentiable_on differentiable_at_real_polynomial_function)
  11.638 +
  11.639 +lemma differentiable_at_polynomial_function:
  11.640 +  fixes f :: "_ \<Rightarrow> 'a::euclidean_space"
  11.641 +  shows "polynomial_function f \<Longrightarrow> f differentiable (at a within S)"
  11.642 +  by (metis differentiable_at_real_polynomial_function polynomial_function_iff_Basis_inner differentiable_componentwise_within)
  11.643 +
  11.644 +lemma differentiable_on_polynomial_function:
  11.645 +  fixes f :: "_ \<Rightarrow> 'a::euclidean_space"
  11.646 +  shows "polynomial_function f \<Longrightarrow> f differentiable_on S"
  11.647 +by (simp add: differentiable_at_polynomial_function differentiable_on_def)
  11.648 +
  11.649 +lemma vector_eq_dot_span:
  11.650 +  assumes "x \<in> span B" "y \<in> span B" and i: "\<And>i. i \<in> B \<Longrightarrow> i \<bullet> x = i \<bullet> y"
  11.651 +  shows "x = y"
  11.652 +proof -
  11.653 +  have "\<And>i. i \<in> B \<Longrightarrow> orthogonal (x - y) i"
  11.654 +    by (simp add: i inner_commute inner_diff_right orthogonal_def)
  11.655 +  moreover have "x - y \<in> span B"
  11.656 +    by (simp add: assms span_diff)
  11.657 +  ultimately have "x - y = 0"
  11.658 +    using orthogonal_to_span orthogonal_self by blast
  11.659 +    then show ?thesis by simp
  11.660 +qed
  11.661 +
  11.662 +lemma orthonormal_basis_expand:
  11.663 +  assumes B: "pairwise orthogonal B"
  11.664 +      and 1: "\<And>i. i \<in> B \<Longrightarrow> norm i = 1"
  11.665 +      and "x \<in> span B"
  11.666 +      and "finite B"
  11.667 +    shows "(\<Sum>i\<in>B. (x \<bullet> i) *\<^sub>R i) = x"
  11.668 +proof (rule vector_eq_dot_span [OF _ \<open>x \<in> span B\<close>])
  11.669 +  show "(\<Sum>i\<in>B. (x \<bullet> i) *\<^sub>R i) \<in> span B"
  11.670 +    by (simp add: span_clauses span_setsum)
  11.671 +  show "i \<bullet> (\<Sum>i\<in>B. (x \<bullet> i) *\<^sub>R i) = i \<bullet> x" if "i \<in> B" for i
  11.672 +  proof -
  11.673 +    have [simp]: "i \<bullet> j = (if j = i then 1 else 0)" if "j \<in> B" for j
  11.674 +      using B 1 that \<open>i \<in> B\<close>
  11.675 +      by (force simp: norm_eq_1 orthogonal_def pairwise_def)
  11.676 +    have "i \<bullet> (\<Sum>i\<in>B. (x \<bullet> i) *\<^sub>R i) = (\<Sum>j\<in>B. x \<bullet> j * (i \<bullet> j))"
  11.677 +      by (simp add: inner_setsum_right)
  11.678 +    also have "... = (\<Sum>j\<in>B. if j = i then x \<bullet> i else 0)"
  11.679 +      by (rule setsum.cong; simp)
  11.680 +    also have "... = i \<bullet> x"
  11.681 +      by (simp add: \<open>finite B\<close> that inner_commute setsum.delta)
  11.682 +    finally show ?thesis .
  11.683 +  qed
  11.684 +qed
  11.685 +
  11.686 +
  11.687 +lemma Stone_Weierstrass_polynomial_function_subspace:
  11.688 +  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
  11.689 +  assumes "compact S"
  11.690 +      and contf: "continuous_on S f"
  11.691 +      and "0 < e"
  11.692 +      and "subspace T" "f ` S \<subseteq> T"
  11.693 +    obtains g where "polynomial_function g" "g ` S \<subseteq> T"
  11.694 +                    "\<And>x. x \<in> S \<Longrightarrow> norm(f x - g x) < e"
  11.695 +proof -
  11.696 +  obtain B where "B \<subseteq> T" and orthB: "pairwise orthogonal B"
  11.697 +             and B1: "\<And>x. x \<in> B \<Longrightarrow> norm x = 1"
  11.698 +             and "independent B" and cardB: "card B = dim T"
  11.699 +             and spanB: "span B = T"
  11.700 +    using orthonormal_basis_subspace \<open>subspace T\<close> by metis
  11.701 +  then have "finite B"
  11.702 +    by (simp add: independent_imp_finite)
  11.703 +  then obtain n::nat and b where "B = b ` {i. i < n}" "inj_on b {i. i < n}"
  11.704 +    using finite_imp_nat_seg_image_inj_on by metis
  11.705 +  with cardB have "n = card B" "dim T = n"
  11.706 +    by (auto simp: card_image)
  11.707 +  have fx: "(\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i) = f x" if "x \<in> S" for x
  11.708 +    apply (rule orthonormal_basis_expand [OF orthB B1 _ \<open>finite B\<close>])
  11.709 +    using \<open>f ` S \<subseteq> T\<close> spanB that by auto
  11.710 +  have cont: "continuous_on S (\<lambda>x. \<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i)"
  11.711 +    by (intro continuous_intros contf)
  11.712 +  obtain g where "polynomial_function g"
  11.713 +             and g: "\<And>x. x \<in> S \<Longrightarrow> norm ((\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i) - g x) < e / (n+2)"
  11.714 +    using Stone_Weierstrass_polynomial_function [OF \<open>compact S\<close> cont, of "e / real (n + 2)"] \<open>0 < e\<close>
  11.715 +    by auto
  11.716 +  with fx have g: "\<And>x. x \<in> S \<Longrightarrow> norm (f x - g x) < e / (n+2)"
  11.717 +    by auto
  11.718 +  show ?thesis
  11.719 +  proof
  11.720 +    show "polynomial_function (\<lambda>x. \<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i)"
  11.721 +      apply (rule polynomial_function_setsum)
  11.722 +       apply (simp add: \<open>finite B\<close>)
  11.723 +      using \<open>polynomial_function g\<close>  by auto
  11.724 +    show "(\<lambda>x. \<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i) ` S \<subseteq> T"
  11.725 +      using \<open>B \<subseteq> T\<close> by (blast intro: subspace_setsum subspace_mul \<open>subspace T\<close>)
  11.726 +    show "norm (f x - (\<Sum>i\<in>B. (g x \<bullet> i) *\<^sub>R i)) < e" if "x \<in> S" for x
  11.727 +    proof -
  11.728 +      have orth': "pairwise (\<lambda>i j. orthogonal ((f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i)
  11.729 +                                              ((f x \<bullet> j) *\<^sub>R j - (g x \<bullet> j) *\<^sub>R j)) B"
  11.730 +        apply (rule pairwise_mono [OF orthB])
  11.731 +        apply (auto simp: orthogonal_def inner_diff_right inner_diff_left)
  11.732 +        done
  11.733 +      then have "(norm (\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i))\<^sup>2 =
  11.734 +                 (\<Sum>i\<in>B. (norm ((f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i))\<^sup>2)"
  11.735 +        by (simp add:  norm_setsum_Pythagorean [OF \<open>finite B\<close> orth'])
  11.736 +      also have "... = (\<Sum>i\<in>B. (norm (((f x - g x) \<bullet> i) *\<^sub>R i))\<^sup>2)"
  11.737 +        by (simp add: algebra_simps)
  11.738 +      also have "... \<le> (\<Sum>i\<in>B. (norm (f x - g x))\<^sup>2)"
  11.739 +        apply (rule setsum_mono)
  11.740 +        apply (simp add: B1)
  11.741 +        apply (rule order_trans [OF Cauchy_Schwarz_ineq])
  11.742 +        by (simp add: B1 dot_square_norm)
  11.743 +      also have "... = n * norm (f x - g x)^2"
  11.744 +        by (simp add: \<open>n = card B\<close>)
  11.745 +      also have "... \<le> n * (e / (n+2))^2"
  11.746 +        apply (rule mult_left_mono)
  11.747 +         apply (meson dual_order.order_iff_strict g norm_ge_zero power_mono that, simp)
  11.748 +        done
  11.749 +      also have "... \<le> e^2 / (n+2)"
  11.750 +        using \<open>0 < e\<close> by (simp add: divide_simps power2_eq_square)
  11.751 +      also have "... < e^2"
  11.752 +        using \<open>0 < e\<close> by (simp add: divide_simps)
  11.753 +      finally have "(norm (\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i))\<^sup>2 < e^2" .
  11.754 +      then have "(norm (\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i)) < e"
  11.755 +        apply (rule power2_less_imp_less)
  11.756 +        using  \<open>0 < e\<close> by auto
  11.757 +      then show ?thesis
  11.758 +        using fx that by (simp add: setsum_subtractf)
  11.759 +    qed
  11.760 +  qed
  11.761 +qed
  11.762 +
  11.763 +
  11.764  hide_fact linear add mult const
  11.765  
  11.766  end
    12.1 --- a/src/HOL/Groups_Big.thy	Wed Sep 21 16:59:51 2016 +0100
    12.2 +++ b/src/HOL/Groups_Big.thy	Thu Sep 22 15:44:47 2016 +0100
    12.3 @@ -624,6 +624,24 @@
    12.4    with eq show False by simp
    12.5  qed
    12.6  
    12.7 +lemma member_le_setsum:
    12.8 +  fixes f :: "_ \<Rightarrow> 'b::{semiring_1, ordered_comm_monoid_add}"
    12.9 +  assumes le: "\<And>x. x \<in> A \<Longrightarrow> 0 \<le> f x"
   12.10 +    and "i \<in> A"
   12.11 +    and "finite A"
   12.12 +  shows "f i \<le> setsum f A"
   12.13 +proof -
   12.14 +  have "f i \<le> setsum f (A \<inter> {i})"
   12.15 +    by (simp add: assms)
   12.16 +  also have "... = (\<Sum>x\<in>A. if x \<in> {i} then f x else 0)"
   12.17 +    using assms setsum.inter_restrict by blast
   12.18 +  also have "... \<le> setsum f A"
   12.19 +    apply (rule setsum_mono)
   12.20 +    apply (auto simp: le)
   12.21 +    done
   12.22 +  finally show ?thesis .
   12.23 +qed
   12.24 +
   12.25  lemma setsum_negf: "(\<Sum>x\<in>A. - f x) = - (\<Sum>x\<in>A. f x)"
   12.26    for f :: "'b \<Rightarrow> 'a::ab_group_add"
   12.27    by (induct A rule: infinite_finite_induct) auto
    13.1 --- a/src/HOL/Set.thy	Wed Sep 21 16:59:51 2016 +0100
    13.2 +++ b/src/HOL/Set.thy	Thu Sep 22 15:44:47 2016 +0100
    13.3 @@ -1852,6 +1852,9 @@
    13.4  lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T"
    13.5    by (force simp: pairwise_def)
    13.6  
    13.7 +lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A"
    13.8 +  by (auto simp: pairwise_def)
    13.9 +
   13.10  definition disjnt :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   13.11    where "disjnt A B \<longleftrightarrow> A \<inter> B = {}"
   13.12