667 lemma%unimportant rank_mul_le_left: |
667 lemma%unimportant rank_mul_le_left: |
668 fixes A :: "real^'n^'m" and B :: "real^'p^'n" |
668 fixes A :: "real^'n^'m" and B :: "real^'p^'n" |
669 shows "rank(A ** B) \<le> rank A" |
669 shows "rank(A ** B) \<le> rank A" |
670 by (metis matrix_transpose_mul rank_mul_le_right rank_transpose) |
670 by (metis matrix_transpose_mul rank_mul_le_right rank_transpose) |
671 |
671 |
|
672 |
|
673 subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3\<close>\<close> |
|
674 |
|
675 lemma exhaust_2: |
|
676 fixes x :: 2 |
|
677 shows "x = 1 \<or> x = 2" |
|
678 proof (induct x) |
|
679 case (of_int z) |
|
680 then have "0 \<le> z" and "z < 2" by simp_all |
|
681 then have "z = 0 | z = 1" by arith |
|
682 then show ?case by auto |
|
683 qed |
|
684 |
|
685 lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2" |
|
686 by (metis exhaust_2) |
|
687 |
|
688 lemma exhaust_3: |
|
689 fixes x :: 3 |
|
690 shows "x = 1 \<or> x = 2 \<or> x = 3" |
|
691 proof (induct x) |
|
692 case (of_int z) |
|
693 then have "0 \<le> z" and "z < 3" by simp_all |
|
694 then have "z = 0 \<or> z = 1 \<or> z = 2" by arith |
|
695 then show ?case by auto |
|
696 qed |
|
697 |
|
698 lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3" |
|
699 by (metis exhaust_3) |
|
700 |
|
701 lemma UNIV_1 [simp]: "UNIV = {1::1}" |
|
702 by (auto simp add: num1_eq_iff) |
|
703 |
|
704 lemma UNIV_2: "UNIV = {1::2, 2::2}" |
|
705 using exhaust_2 by auto |
|
706 |
|
707 lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}" |
|
708 using exhaust_3 by auto |
|
709 |
|
710 lemma sum_1: "sum f (UNIV::1 set) = f 1" |
|
711 unfolding UNIV_1 by simp |
|
712 |
|
713 lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2" |
|
714 unfolding UNIV_2 by simp |
|
715 |
|
716 lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3" |
|
717 unfolding UNIV_3 by (simp add: ac_simps) |
|
718 |
|
719 subsection%unimportant\<open>The collapse of the general concepts to dimension one\<close> |
|
720 |
|
721 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))" |
|
722 by (simp add: vec_eq_iff) |
|
723 |
|
724 lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))" |
|
725 apply auto |
|
726 apply (erule_tac x= "x$1" in allE) |
|
727 apply (simp only: vector_one[symmetric]) |
|
728 done |
|
729 |
|
730 lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)" |
|
731 by (simp add: norm_vec_def) |
|
732 |
|
733 lemma dist_vector_1: |
|
734 fixes x :: "'a::real_normed_vector^1" |
|
735 shows "dist x y = dist (x$1) (y$1)" |
|
736 by (simp add: dist_norm norm_vector_1) |
|
737 |
|
738 lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>" |
|
739 by (simp add: norm_vector_1) |
|
740 |
|
741 lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>" |
|
742 by (auto simp add: norm_real dist_norm) |
|
743 |
|
744 |
|
745 subsection%unimportant\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close> |
|
746 |
|
747 lemma vector_one_nth [simp]: |
|
748 fixes x :: "'a^1" shows "vec (x $ 1) = x" |
|
749 by (metis vec_def vector_one) |
|
750 |
|
751 lemma tendsto_at_within_vector_1: |
|
752 fixes S :: "'a :: metric_space set" |
|
753 assumes "(f \<longlongrightarrow> fx) (at x within S)" |
|
754 shows "((\<lambda>y::'a^1. \<chi> i. f (y $ 1)) \<longlongrightarrow> (vec fx::'a^1)) (at (vec x) within vec ` S)" |
|
755 proof (rule topological_tendstoI) |
|
756 fix T :: "('a^1) set" |
|
757 assume "open T" "vec fx \<in> T" |
|
758 have "\<forall>\<^sub>F x in at x within S. f x \<in> (\<lambda>x. x $ 1) ` T" |
|
759 using \<open>open T\<close> \<open>vec fx \<in> T\<close> assms open_image_vec_nth tendsto_def by fastforce |
|
760 then show "\<forall>\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\<chi> i. f (x $ 1)) \<in> T" |
|
761 unfolding eventually_at dist_norm [symmetric] |
|
762 by (rule ex_forward) |
|
763 (use \<open>open T\<close> in |
|
764 \<open>fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\<close>) |
|
765 qed |
|
766 |
|
767 lemma has_derivative_vector_1: |
|
768 assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)" |
|
769 shows "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a)) |
|
770 (at ((vec a)::real^1) within vec ` S)" |
|
771 using der_g |
|
772 apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1) |
|
773 apply (drule tendsto_at_within_vector_1, vector) |
|
774 apply (auto simp: algebra_simps eventually_at tendsto_def) |
|
775 done |
|
776 |
|
777 |
|
778 subsection%unimportant\<open>Explicit vector construction from lists\<close> |
|
779 |
|
780 definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)" |
|
781 |
|
782 lemma vector_1 [simp]: "(vector[x]) $1 = x" |
|
783 unfolding vector_def by simp |
|
784 |
|
785 lemma vector_2 [simp]: "(vector[x,y]) $1 = x" "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)" |
|
786 unfolding vector_def by simp_all |
|
787 |
|
788 lemma vector_3 [simp]: |
|
789 "(vector [x,y,z] ::('a::zero)^3)$1 = x" |
|
790 "(vector [x,y,z] ::('a::zero)^3)$2 = y" |
|
791 "(vector [x,y,z] ::('a::zero)^3)$3 = z" |
|
792 unfolding vector_def by simp_all |
|
793 |
|
794 lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))" |
|
795 by (metis vector_1 vector_one) |
|
796 |
|
797 lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))" |
|
798 apply auto |
|
799 apply (erule_tac x="v$1" in allE) |
|
800 apply (erule_tac x="v$2" in allE) |
|
801 apply (subgoal_tac "vector [v$1, v$2] = v") |
|
802 apply simp |
|
803 apply (vector vector_def) |
|
804 apply (simp add: forall_2) |
|
805 done |
|
806 |
|
807 lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))" |
|
808 apply auto |
|
809 apply (erule_tac x="v$1" in allE) |
|
810 apply (erule_tac x="v$2" in allE) |
|
811 apply (erule_tac x="v$3" in allE) |
|
812 apply (subgoal_tac "vector [v$1, v$2, v$3] = v") |
|
813 apply simp |
|
814 apply (vector vector_def) |
|
815 apply (simp add: forall_3) |
|
816 done |
|
817 |
|
818 subsection%unimportant \<open>lambda skolemization on cartesian products\<close> |
|
819 |
|
820 lemma%important lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow> |
|
821 (\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs") |
|
822 proof%unimportant - |
|
823 let ?S = "(UNIV :: 'n set)" |
|
824 { assume H: "?rhs" |
|
825 then have ?lhs by auto } |
|
826 moreover |
|
827 { assume H: "?lhs" |
|
828 then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis |
|
829 let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n" |
|
830 { fix i |
|
831 from f have "P i (f i)" by metis |
|
832 then have "P i (?x $ i)" by auto |
|
833 } |
|
834 hence "\<forall>i. P i (?x$i)" by metis |
|
835 hence ?rhs by metis } |
|
836 ultimately show ?thesis by metis |
|
837 qed |
|
838 |
|
839 |
|
840 text \<open>The same result in terms of square matrices.\<close> |
|
841 |
|
842 |
|
843 text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close> |
|
844 |
|
845 definition%unimportant "rowvector v = (\<chi> i j. (v$j))" |
|
846 |
|
847 definition%unimportant "columnvector v = (\<chi> i j. (v$i))" |
|
848 |
|
849 lemma%unimportant transpose_columnvector: "transpose(columnvector v) = rowvector v" |
|
850 by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff) |
|
851 |
|
852 lemma%unimportant transpose_rowvector: "transpose(rowvector v) = columnvector v" |
|
853 by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff) |
|
854 |
|
855 lemma%unimportant dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v" |
|
856 by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) |
|
857 |
|
858 lemma%unimportant dot_matrix_product: |
|
859 "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1" |
|
860 by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def) |
|
861 |
|
862 lemma%unimportant dot_matrix_vector_mul: |
|
863 fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" |
|
864 shows "(A *v x) \<bullet> (B *v y) = |
|
865 (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1" |
|
866 unfolding dot_matrix_product transpose_columnvector[symmetric] |
|
867 dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc .. |
|
868 |
|
869 |
|
870 lemma%important dim_substandard_cart: "vec.dim {x::'a::field^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d" |
|
871 (is "vec.dim ?A = _") |
|
872 proof%unimportant (rule vec.dim_unique) |
|
873 let ?B = "((\<lambda>x. axis x 1) ` d)" |
|
874 have subset_basis: "?B \<subseteq> cart_basis" |
|
875 by (auto simp: cart_basis_def) |
|
876 show "?B \<subseteq> ?A" |
|
877 by (auto simp: axis_def) |
|
878 show "vec.independent ((\<lambda>x. axis x 1) ` d)" |
|
879 using subset_basis |
|
880 by (rule vec.independent_mono[OF vec.independent_Basis]) |
|
881 have "x \<in> vec.span ?B" if "\<forall>i. i \<notin> d \<longrightarrow> x $ i = 0" for x::"'a^'n" |
|
882 proof - |
|
883 have "finite ?B" |
|
884 using subset_basis finite_cart_basis |
|
885 by (rule finite_subset) |
|
886 have "x = (\<Sum>i\<in>UNIV. x $ i *s axis i 1)" |
|
887 by (rule basis_expansion[symmetric]) |
|
888 also have "\<dots> = (\<Sum>i\<in>d. (x $ i) *s axis i 1)" |
|
889 by (rule sum.mono_neutral_cong_right) (auto simp: that) |
|
890 also have "\<dots> \<in> vec.span ?B" |
|
891 by (simp add: vec.span_sum vec.span_clauses) |
|
892 finally show "x \<in> vec.span ?B" . |
|
893 qed |
|
894 then show "?A \<subseteq> vec.span ?B" by auto |
|
895 qed (simp add: card_image inj_on_def axis_eq_axis) |
|
896 |
|
897 lemma%unimportant affinity_inverses: |
|
898 assumes m0: "m \<noteq> (0::'a::field)" |
|
899 shows "(\<lambda>x. m *s x + c) \<circ> (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id" |
|
900 "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) \<circ> (\<lambda>x. m *s x + c) = id" |
|
901 using m0 |
|
902 by (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff) |
|
903 |
|
904 lemma%important vector_affinity_eq: |
|
905 assumes m0: "(m::'a::field) \<noteq> 0" |
|
906 shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)" |
|
907 proof%unimportant |
|
908 assume h: "m *s x + c = y" |
|
909 hence "m *s x = y - c" by (simp add: field_simps) |
|
910 hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp |
|
911 then show "x = inverse m *s y + - (inverse m *s c)" |
|
912 using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) |
|
913 next |
|
914 assume h: "x = inverse m *s y + - (inverse m *s c)" |
|
915 show "m *s x + c = y" unfolding h |
|
916 using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) |
|
917 qed |
|
918 |
|
919 lemma%unimportant vector_eq_affinity: |
|
920 "(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)" |
|
921 using vector_affinity_eq[where m=m and x=x and y=y and c=c] |
|
922 by metis |
|
923 |
|
924 lemma%unimportant vector_cart: |
|
925 fixes f :: "real^'n \<Rightarrow> real" |
|
926 shows "(\<chi> i. f (axis i 1)) = (\<Sum>i\<in>Basis. f i *\<^sub>R i)" |
|
927 unfolding euclidean_eq_iff[where 'a="real^'n"] |
|
928 by simp (simp add: Basis_vec_def inner_axis) |
|
929 |
|
930 lemma%unimportant const_vector_cart:"((\<chi> i. d)::real^'n) = (\<Sum>i\<in>Basis. d *\<^sub>R i)" |
|
931 by (rule vector_cart) |
|
932 |
672 end |
933 end |