# HG changeset patch
# User immler
# Date 1452522017 -3600
# Node ID d8e7738bd2e9c04bb23427fe5a983dbafba8632c
# Parent  2d187ace28274b8d7896a15a1128a8651801d7f1
generalized proofs

diff -r 2d187ace2827 -r d8e7738bd2e9 src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Mon Jan 11 13:15:15 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Bounded_Linear_Function.thy	Mon Jan 11 15:20:17 2016 +0100
@@ -467,74 +467,15 @@
   "(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)"
   by auto
 
-text \<open>TODO: generalize this and @{thm compact_lemma}?!\<close>
 lemma compact_blinfun_lemma:
   fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space"
   assumes "bounded (range f)"
   shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r.
     subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
-proof safe
-  fix d :: "'a set"
-  assume d: "d \<subseteq> Basis"
-  with finite_Basis have "finite d"
-    by (blast intro: finite_subset)
-  from this d show "\<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists>r. subseq r \<and>
-    (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)"
-  proof (induct d)
-    case empty
-    then show ?case
-      unfolding subseq_def by auto
-  next
-    case (insert k d)
-    have k[intro]: "k \<in> Basis"
-      using insert by auto
-    have s': "bounded ((\<lambda>x. blinfun_apply x k) ` range f)"
-      using \<open>bounded (range f)\<close>
-      by (auto intro!: bounded_linear_image bounded_linear_intros)
-    obtain l1::"'a \<Rightarrow>\<^sub>L 'b" and r1 where r1: "subseq r1"
-      and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) i) (l1 i) < e) sequentially"
-      using insert(3) using insert(4) by auto
-    have f': "\<forall>n. f (r1 n) k \<in> (\<lambda>x. blinfun_apply x k) ` range f"
-      by simp
-    have "bounded (range (\<lambda>i. f (r1 i) k))"
-      by (metis (lifting) bounded_subset f' image_subsetI s')
-    then obtain l2 r2
-      where r2: "subseq r2"
-      and lr2: "((\<lambda>i. f (r1 (r2 i)) k) \<longlongrightarrow> l2) sequentially"
-      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) k"]
-      by (auto simp: o_def)
-    def r \<equiv> "r1 \<circ> r2"
-    have r:"subseq r"
-      using r1 and r2 unfolding r_def o_def subseq_def by auto
-    moreover
-    def l \<equiv> "blinfun_of_matrix (\<lambda>i j. if j = k then l2 \<bullet> i else l1 j \<bullet> i)::'a \<Rightarrow>\<^sub>L 'b"
-    {
-      fix e::real
-      assume "e > 0"
-      from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n)  i) (l1  i) < e) sequentially"
-        by blast
-      from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n))  k) l2 < e) sequentially"
-        by (rule tendstoD)
-      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n))  i) (l1  i) < e) sequentially"
-        by (rule eventually_subseq)
-      have l2: "l k = l2"
-        using insert.prems
-        by (auto simp: blinfun_of_matrix.rep_eq inner_Basis l_def mult_if_delta
-          scaleR_setsum_left[symmetric] setsum.delta' intro!: euclidean_eqI[where 'a='b])
-      {
-        fix i assume "i \<in> d"
-        with insert have "i \<in> Basis" "i \<noteq> k" by auto
-        hence l1: "l i = (l1 i)"
-          by (auto simp: blinfun_of_matrix.rep_eq inner_Basis l_def mult_if_delta
-            scaleR_setsum_left[symmetric] setsum.delta' intro!: euclidean_eqI[where 'a='b])
-      } note l1 = this
-      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n)  i) (l  i) < e) sequentially"
-        using N1' N2
-        by eventually_elim (insert insert.prems, auto simp: r_def o_def l1 l2)
-    }
-    ultimately show ?case by auto
-  qed
-qed
+  by (rule compact_lemma_general[where unproj = "\<lambda>e. blinfun_of_matrix (\<lambda>i j. e j \<bullet> i)"])
+   (auto intro!: euclidean_eqI[where 'a='b] bounded_linear_image assms
+    simp: blinfun_of_matrix_works blinfun_of_matrix_apply inner_Basis mult_if_delta setsum.delta'
+      scaleR_setsum_left[symmetric])
 
 lemma blinfun_euclidean_eqI: "(\<And>i. i \<in> Basis \<Longrightarrow> blinfun_apply x i = blinfun_apply y i) \<Longrightarrow> x = y"
   apply (auto intro!: blinfun_eqI)
diff -r 2d187ace2827 -r d8e7738bd2e9 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Jan 11 13:15:15 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Mon Jan 11 15:20:17 2016 +0100
@@ -820,47 +820,14 @@
 lemma compact_lemma_cart:
   fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n"
   assumes f: "bounded (range f)"
-  shows "\<forall>d.
-        \<exists>l r. subseq r \<and>
+  shows "\<exists>l r. subseq r \<and>
         (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
-proof
-  fix d :: "'n set"
-  have "finite d" by simp
-  thus "\<exists>l::'a ^ 'n. \<exists>r. subseq r \<and>
-      (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)"
-  proof (induct d)
-    case empty
-    thus ?case unfolding subseq_def by auto
-  next
-    case (insert k d)
-    obtain l1::"'a^'n" and r1 where r1:"subseq r1"
-      and lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially"
-      using insert(3) by auto
-    have s': "bounded ((\<lambda>x. x $ k) ` range f)" using \<open>bounded (range f)\<close>
-      by (auto intro!: bounded_component_cart)
-    have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` range f" by simp
-    have "bounded (range (\<lambda>i. f (r1 i) $ k))"
-      by (metis (lifting) bounded_subset image_subsetI f' s')
-    then obtain l2 r2 where r2: "subseq r2"
-      and lr2: "((\<lambda>i. f (r1 (r2 i)) $ k) \<longlongrightarrow> l2) sequentially"
-      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) $ k"] by (auto simp: o_def)
-    def r \<equiv> "r1 \<circ> r2"
-    have r: "subseq r"
-      using r1 and r2 unfolding r_def o_def subseq_def by auto
-    moreover
-    def l \<equiv> "(\<chi> i. if i = k then l2 else l1$i)::'a^'n"
-    { fix e :: real assume "e > 0"
-      from lr1 \<open>e>0\<close> have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially"
-        by blast
-      from lr2 \<open>e>0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) $ k) l2 < e) sequentially"
-        by (rule tendstoD)
-      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) $ i) (l1 $ i) < e) sequentially"
-        by (rule eventually_subseq)
-      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) $ i) (l $ i) < e) sequentially"
-        using N1' N2 by (rule eventually_elim2, simp add: l_def r_def)
-    }
-    ultimately show ?case by auto
-  qed
+    (is "?th d")
+proof -
+  have "\<forall>d' \<subseteq> d. ?th d'"
+    by (rule compact_lemma_general[where unproj=vec_lambda])
+      (auto intro!: f bounded_component_cart simp: vec_lambda_eta)
+  then show "?th d" by simp
 qed
 
 instance vec :: (heine_borel, finite) heine_borel
diff -r 2d187ace2827 -r d8e7738bd2e9 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 11 13:15:15 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jan 11 15:20:17 2016 +0100
@@ -4443,61 +4443,75 @@
     using Bseq_monoseq_convergent[of "f \<circ> r"] by (auto simp: convergent_def)
 qed
 
-lemma compact_lemma:
-  fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
-  assumes "bounded (range f)"
-  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
-    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
+lemma compact_lemma_general:
+  fixes f :: "nat \<Rightarrow> 'a"
+  fixes proj::"'a \<Rightarrow> 'b \<Rightarrow> 'c::heine_borel" (infixl "proj" 60)
+  fixes unproj:: "('b \<Rightarrow> 'c) \<Rightarrow> 'a"
+  assumes finite_basis: "finite basis"
+  assumes bounded_proj: "\<And>k. k \<in> basis \<Longrightarrow> bounded ((\<lambda>x. x proj k) ` range f)"
+  assumes proj_unproj: "\<And>e k. k \<in> basis \<Longrightarrow> (unproj e) proj k = e k"
+  assumes unproj_proj: "\<And>x. unproj (\<lambda>k. x proj k) = x"
+  shows "\<forall>d\<subseteq>basis. \<exists>l::'a. \<exists> r.
+    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
 proof safe
-  fix d :: "'a set"
-  assume d: "d \<subseteq> Basis"
-  with finite_Basis have "finite d"
+  fix d :: "'b set"
+  assume d: "d \<subseteq> basis"
+  with finite_basis have "finite d"
     by (blast intro: finite_subset)
   from this d show "\<exists>l::'a. \<exists>r. subseq r \<and>
-    (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
+    (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) proj i) (l proj i) < e) sequentially)"
   proof (induct d)
     case empty
     then show ?case
       unfolding subseq_def by auto
   next
     case (insert k d)
-    have k[intro]: "k \<in> Basis"
+    have k[intro]: "k \<in> basis"
       using insert by auto
-    have s': "bounded ((\<lambda>x. x \<bullet> k) ` range f)"
-      using \<open>bounded (range f)\<close>
-      by (auto intro!: bounded_linear_image bounded_linear_inner_left)
+    have s': "bounded ((\<lambda>x. x proj k) ` range f)"
+      using k
+      by (rule bounded_proj)
     obtain l1::"'a" and r1 where r1: "subseq r1"
-      and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
+      and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
       using insert(3) using insert(4) by auto
-    have f': "\<forall>n. f (r1 n) \<bullet> k \<in> (\<lambda>x. x \<bullet> k) ` range f"
+    have f': "\<forall>n. f (r1 n) proj k \<in> (\<lambda>x. x proj k) ` range f"
       by simp
-    have "bounded (range (\<lambda>i. f (r1 i) \<bullet> k))"
+    have "bounded (range (\<lambda>i. f (r1 i) proj k))"
       by (metis (lifting) bounded_subset f' image_subsetI s')
-    then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) \<bullet> k) \<longlongrightarrow> l2) sequentially"
-      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) \<bullet> k"]
+    then obtain l2 r2 where r2:"subseq r2" and lr2:"((\<lambda>i. f (r1 (r2 i)) proj k) \<longlongrightarrow> l2) sequentially"
+      using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) proj k"]
       by (auto simp: o_def)
     def r \<equiv> "r1 \<circ> r2"
     have r:"subseq r"
       using r1 and r2 unfolding r_def o_def subseq_def by auto
     moreover
-    def l \<equiv> "(\<Sum>i\<in>Basis. (if i = k then l2 else l1\<bullet>i) *\<^sub>R i)::'a"
+    def l \<equiv> "unproj (\<lambda>i. if i = k then l2 else l1 proj i)::'a"
     {
       fix e::real
       assume "e > 0"
-      from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
+      from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) proj i) (l1 proj i) < e) sequentially"
         by blast
-      from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) \<bullet> k) l2 < e) sequentially"
+      from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) proj k) l2 < e) sequentially"
         by (rule tendstoD)
-      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) \<bullet> i) (l1 \<bullet> i) < e) sequentially"
+      from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) proj i) (l1 proj i) < e) sequentially"
         by (rule eventually_subseq)
-      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially"
+      have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) proj i) (l proj i) < e) sequentially"
         using N1' N2
-        by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def)
+        by eventually_elim (insert insert.prems, auto simp: l_def r_def o_def proj_unproj)
     }
     ultimately show ?case by auto
   qed
 qed
 
+lemma compact_lemma:
+  fixes f :: "nat \<Rightarrow> 'a::euclidean_space"
+  assumes "bounded (range f)"
+  shows "\<forall>d\<subseteq>Basis. \<exists>l::'a. \<exists> r.
+    subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) \<bullet> i) (l \<bullet> i) < e) sequentially)"
+  by (rule compact_lemma_general[where unproj="\<lambda>e. \<Sum>i\<in>Basis. e i *\<^sub>R i"])
+     (auto intro!: assms bounded_linear_inner_left bounded_linear_image
+       simp: euclidean_representation)
+
 instance euclidean_space \<subseteq> heine_borel
 proof
   fix f :: "nat \<Rightarrow> 'a"