465 |
465 |
466 lemma mult_if_delta: |
466 lemma mult_if_delta: |
467 "(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)" |
467 "(if P then (1::'a::comm_semiring_1) else 0) * q = (if P then q else 0)" |
468 by auto |
468 by auto |
469 |
469 |
470 text \<open>TODO: generalize this and @{thm compact_lemma}?!\<close> |
|
471 lemma compact_blinfun_lemma: |
470 lemma compact_blinfun_lemma: |
472 fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space" |
471 fixes f :: "nat \<Rightarrow> 'a::euclidean_space \<Rightarrow>\<^sub>L 'b::euclidean_space" |
473 assumes "bounded (range f)" |
472 assumes "bounded (range f)" |
474 shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r. |
473 shows "\<forall>d\<subseteq>Basis. \<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists> r. |
475 subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)" |
474 subseq r \<and> (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)" |
476 proof safe |
475 by (rule compact_lemma_general[where unproj = "\<lambda>e. blinfun_of_matrix (\<lambda>i j. e j \<bullet> i)"]) |
477 fix d :: "'a set" |
476 (auto intro!: euclidean_eqI[where 'a='b] bounded_linear_image assms |
478 assume d: "d \<subseteq> Basis" |
477 simp: blinfun_of_matrix_works blinfun_of_matrix_apply inner_Basis mult_if_delta setsum.delta' |
479 with finite_Basis have "finite d" |
478 scaleR_setsum_left[symmetric]) |
480 by (blast intro: finite_subset) |
|
481 from this d show "\<exists>l::'a \<Rightarrow>\<^sub>L 'b. \<exists>r. subseq r \<and> |
|
482 (\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) i) (l i) < e) sequentially)" |
|
483 proof (induct d) |
|
484 case empty |
|
485 then show ?case |
|
486 unfolding subseq_def by auto |
|
487 next |
|
488 case (insert k d) |
|
489 have k[intro]: "k \<in> Basis" |
|
490 using insert by auto |
|
491 have s': "bounded ((\<lambda>x. blinfun_apply x k) ` range f)" |
|
492 using \<open>bounded (range f)\<close> |
|
493 by (auto intro!: bounded_linear_image bounded_linear_intros) |
|
494 obtain l1::"'a \<Rightarrow>\<^sub>L 'b" and r1 where r1: "subseq r1" |
|
495 and lr1: "\<forall>e > 0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) i) (l1 i) < e) sequentially" |
|
496 using insert(3) using insert(4) by auto |
|
497 have f': "\<forall>n. f (r1 n) k \<in> (\<lambda>x. blinfun_apply x k) ` range f" |
|
498 by simp |
|
499 have "bounded (range (\<lambda>i. f (r1 i) k))" |
|
500 by (metis (lifting) bounded_subset f' image_subsetI s') |
|
501 then obtain l2 r2 |
|
502 where r2: "subseq r2" |
|
503 and lr2: "((\<lambda>i. f (r1 (r2 i)) k) \<longlongrightarrow> l2) sequentially" |
|
504 using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) k"] |
|
505 by (auto simp: o_def) |
|
506 def r \<equiv> "r1 \<circ> r2" |
|
507 have r:"subseq r" |
|
508 using r1 and r2 unfolding r_def o_def subseq_def by auto |
|
509 moreover |
|
510 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" |
|
511 { |
|
512 fix e::real |
|
513 assume "e > 0" |
|
514 from lr1 \<open>e > 0\<close> have N1: "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) i) (l1 i) < e) sequentially" |
|
515 by blast |
|
516 from lr2 \<open>e > 0\<close> have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) k) l2 < e) sequentially" |
|
517 by (rule tendstoD) |
|
518 from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) i) (l1 i) < e) sequentially" |
|
519 by (rule eventually_subseq) |
|
520 have l2: "l k = l2" |
|
521 using insert.prems |
|
522 by (auto simp: blinfun_of_matrix.rep_eq inner_Basis l_def mult_if_delta |
|
523 scaleR_setsum_left[symmetric] setsum.delta' intro!: euclidean_eqI[where 'a='b]) |
|
524 { |
|
525 fix i assume "i \<in> d" |
|
526 with insert have "i \<in> Basis" "i \<noteq> k" by auto |
|
527 hence l1: "l i = (l1 i)" |
|
528 by (auto simp: blinfun_of_matrix.rep_eq inner_Basis l_def mult_if_delta |
|
529 scaleR_setsum_left[symmetric] setsum.delta' intro!: euclidean_eqI[where 'a='b]) |
|
530 } note l1 = this |
|
531 have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) i) (l i) < e) sequentially" |
|
532 using N1' N2 |
|
533 by eventually_elim (insert insert.prems, auto simp: r_def o_def l1 l2) |
|
534 } |
|
535 ultimately show ?case by auto |
|
536 qed |
|
537 qed |
|
538 |
479 |
539 lemma blinfun_euclidean_eqI: "(\<And>i. i \<in> Basis \<Longrightarrow> blinfun_apply x i = blinfun_apply y i) \<Longrightarrow> x = y" |
480 lemma blinfun_euclidean_eqI: "(\<And>i. i \<in> Basis \<Longrightarrow> blinfun_apply x i = blinfun_apply y i) \<Longrightarrow> x = y" |
540 apply (auto intro!: blinfun_eqI) |
481 apply (auto intro!: blinfun_eqI) |
541 apply (subst (2) euclidean_representation[symmetric, where 'a='a]) |
482 apply (subst (2) euclidean_representation[symmetric, where 'a='a]) |
542 apply (subst (1) euclidean_representation[symmetric, where 'a='a]) |
483 apply (subst (1) euclidean_representation[symmetric, where 'a='a]) |