src/HOL/Analysis/Product_Vector.thy
changeset 68072 493b818e8e10
parent 67962 0acdcd8f4ba1
child 68607 67bb59e49834
     1.1 --- a/src/HOL/Analysis/Product_Vector.thy	Wed Apr 18 21:12:50 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Wed May 02 13:49:38 2018 +0200
     1.3 @@ -10,6 +10,52 @@
     1.4    "HOL-Library.Product_Plus"
     1.5  begin
     1.6  
     1.7 +lemma Times_eq_image_sum:
     1.8 +  fixes S :: "'a :: comm_monoid_add set" and T :: "'b :: comm_monoid_add set"
     1.9 +  shows "S \<times> T = {u + v |u v. u \<in> (\<lambda>x. (x, 0)) ` S \<and> v \<in> Pair 0 ` T}"
    1.10 +  by force
    1.11 +
    1.12 +
    1.13 +subsection \<open>Product is a module\<close>
    1.14 +
    1.15 +locale module_prod = module_pair begin
    1.16 +
    1.17 +definition scale :: "'a \<Rightarrow> 'b \<times> 'c \<Rightarrow> 'b \<times> 'c"
    1.18 +  where "scale a v = (s1 a (fst v), s2 a (snd v))"
    1.19 +
    1.20 +lemma scale_prod: "scale x (a, b) = (s1 x a, s2 x b)"
    1.21 +  by (auto simp: scale_def)
    1.22 +
    1.23 +sublocale p: module scale
    1.24 +proof qed (simp_all add: scale_def
    1.25 +  m1.scale_left_distrib m1.scale_right_distrib m2.scale_left_distrib m2.scale_right_distrib)
    1.26 +
    1.27 +lemma subspace_Times: "m1.subspace A \<Longrightarrow> m2.subspace B \<Longrightarrow> p.subspace (A \<times> B)"
    1.28 +  unfolding m1.subspace_def m2.subspace_def p.subspace_def
    1.29 +  by (auto simp: zero_prod_def scale_def)
    1.30 +
    1.31 +lemma module_hom_fst: "module_hom scale s1 fst"
    1.32 +  by unfold_locales (auto simp: scale_def)
    1.33 +
    1.34 +lemma module_hom_snd: "module_hom scale s2 snd"
    1.35 +  by unfold_locales (auto simp: scale_def)
    1.36 +
    1.37 +end
    1.38 +
    1.39 +locale vector_space_prod = vector_space_pair begin
    1.40 +
    1.41 +sublocale module_prod s1 s2
    1.42 +  rewrites "module_hom = Vector_Spaces.linear"
    1.43 +  by unfold_locales (fact module_hom_eq_linear)
    1.44 +
    1.45 +sublocale p: vector_space scale by unfold_locales (auto simp: algebra_simps)
    1.46 +
    1.47 +lemmas linear_fst = module_hom_fst
    1.48 +  and linear_snd = module_hom_snd
    1.49 +
    1.50 +end
    1.51 +
    1.52 +
    1.53  subsection \<open>Product is a real vector space\<close>
    1.54  
    1.55  instantiation%important prod :: (real_vector, real_vector) real_vector
    1.56 @@ -42,6 +88,27 @@
    1.57  
    1.58  end
    1.59  
    1.60 +lemma module_prod_scale_eq_scaleR: "module_prod.scale ( *\<^sub>R) ( *\<^sub>R) = scaleR"
    1.61 +  apply (rule ext) apply (rule ext)
    1.62 +  apply (subst module_prod.scale_def)
    1.63 +  subgoal by unfold_locales
    1.64 +  by (simp add: scaleR_prod_def)
    1.65 +
    1.66 +interpretation real_vector?: vector_space_prod "scaleR::_\<Rightarrow>_\<Rightarrow>'a::real_vector" "scaleR::_\<Rightarrow>_\<Rightarrow>'b::real_vector"
    1.67 +  rewrites "scale = (( *\<^sub>R)::_\<Rightarrow>_\<Rightarrow>('a \<times> 'b))"
    1.68 +    and "module.dependent ( *\<^sub>R) = dependent"
    1.69 +    and "module.representation ( *\<^sub>R) = representation"
    1.70 +    and "module.subspace ( *\<^sub>R) = subspace"
    1.71 +    and "module.span ( *\<^sub>R) = span"
    1.72 +    and "vector_space.extend_basis ( *\<^sub>R) = extend_basis"
    1.73 +    and "vector_space.dim ( *\<^sub>R) = dim"
    1.74 +    and "Vector_Spaces.linear ( *\<^sub>R) ( *\<^sub>R) = linear"
    1.75 +  subgoal by unfold_locales
    1.76 +  subgoal by (fact module_prod_scale_eq_scaleR)
    1.77 +  unfolding dependent_raw_def representation_raw_def subspace_raw_def span_raw_def
    1.78 +    extend_basis_raw_def dim_raw_def linear_def
    1.79 +  by (rule refl)+
    1.80 +
    1.81  subsection \<open>Product is a metric space\<close>
    1.82  
    1.83  (* TODO: Product of uniform spaces and compatibility with metric_spaces! *)
    1.84 @@ -270,7 +337,7 @@
    1.85    show "(f (x + y), g (x + y)) = (f x, g x) + (f y, g y)"
    1.86      by (simp add: f.add g.add)
    1.87    show "(f (r *\<^sub>R x), g (r *\<^sub>R x)) = r *\<^sub>R (f x, g x)"
    1.88 -    by (simp add: f.scaleR g.scaleR)
    1.89 +    by (simp add: f.scale g.scale)
    1.90    obtain Kf where "0 < Kf" and norm_f: "\<And>x. norm (f x) \<le> norm x * Kf"
    1.91      using f.pos_bounded by fast
    1.92    obtain Kg where "0 < Kg" and norm_g: "\<And>x. norm (g x) \<le> norm x * Kg"
    1.93 @@ -389,4 +456,112 @@
    1.94    unfolding norm_Pair
    1.95    by (metis norm_ge_zero sqrt_sum_squares_le_sum)
    1.96  
    1.97 +lemma (in vector_space_prod) span_Times_sing1: "p.span ({0} \<times> B) = {0} \<times> vs2.span B"
    1.98 +  apply (rule p.span_unique)
    1.99 +  subgoal by (auto intro!: vs1.span_base vs2.span_base)
   1.100 +  subgoal using vs1.subspace_single_0 vs2.subspace_span by (rule subspace_Times)
   1.101 +  subgoal for T
   1.102 +  proof safe
   1.103 +    fix b
   1.104 +    assume subset_T: "{0} \<times> B \<subseteq> T" and subspace: "p.subspace T" and b_span: "b \<in> vs2.span B"
   1.105 +    then obtain t r where b: "b = (\<Sum>a\<in>t. r a *b a)" and t: "finite t" "t \<subseteq> B"
   1.106 +      by (auto simp: vs2.span_explicit)
   1.107 +    have "(0, b) = (\<Sum>b\<in>t. scale (r b) (0, b))"
   1.108 +      unfolding b scale_prod sum_prod
   1.109 +      by simp
   1.110 +    also have "\<dots> \<in> T"
   1.111 +      using \<open>t \<subseteq> B\<close> subset_T
   1.112 +      by (auto intro!: p.subspace_sum p.subspace_scale subspace)
   1.113 +    finally show "(0, b) \<in> T" .
   1.114 +  qed
   1.115 +  done
   1.116 +
   1.117 +lemma (in vector_space_prod) span_Times_sing2: "p.span (A \<times> {0}) = vs1.span A \<times> {0}"
   1.118 +  apply (rule p.span_unique)
   1.119 +  subgoal by (auto intro!: vs1.span_base vs2.span_base)
   1.120 +  subgoal using vs1.subspace_span vs2.subspace_single_0 by (rule subspace_Times)
   1.121 +  subgoal for T
   1.122 +  proof safe
   1.123 +    fix a
   1.124 +    assume subset_T: "A \<times> {0} \<subseteq> T" and subspace: "p.subspace T" and a_span: "a \<in> vs1.span A"
   1.125 +    then obtain t r where a: "a = (\<Sum>a\<in>t. r a *a a)" and t: "finite t" "t \<subseteq> A"
   1.126 +      by (auto simp: vs1.span_explicit)
   1.127 +    have "(a, 0) = (\<Sum>a\<in>t. scale (r a) (a, 0))"
   1.128 +      unfolding a scale_prod sum_prod
   1.129 +      by simp
   1.130 +    also have "\<dots> \<in> T"
   1.131 +      using \<open>t \<subseteq> A\<close> subset_T
   1.132 +      by (auto intro!: p.subspace_sum p.subspace_scale subspace)
   1.133 +    finally show "(a, 0) \<in> T" .
   1.134 +  qed
   1.135 +  done
   1.136 +
   1.137 +lemma (in finite_dimensional_vector_space) zero_not_in_Basis[simp]: "0 \<notin> Basis"
   1.138 +  using dependent_zero local.independent_Basis by blast
   1.139 +
   1.140 +locale finite_dimensional_vector_space_prod = vector_space_prod + finite_dimensional_vector_space_pair begin
   1.141 +
   1.142 +definition "Basis_pair = B1 \<times> {0} \<union> {0} \<times> B2"
   1.143 +
   1.144 +sublocale p: finite_dimensional_vector_space scale Basis_pair
   1.145 +proof unfold_locales
   1.146 +  show "finite Basis_pair"
   1.147 +    by (auto intro!: finite_cartesian_product vs1.finite_Basis vs2.finite_Basis simp: Basis_pair_def)
   1.148 +  show "p.independent Basis_pair"
   1.149 +    unfolding p.dependent_def Basis_pair_def
   1.150 +  proof safe
   1.151 +    fix a
   1.152 +    assume a: "a \<in> B1"
   1.153 +    assume "(a, 0) \<in> p.span (B1 \<times> {0} \<union> {0} \<times> B2 - {(a, 0)})"
   1.154 +    also have "B1 \<times> {0} \<union> {0} \<times> B2 - {(a, 0)} = (B1 - {a}) \<times> {0} \<union> {0} \<times> B2"
   1.155 +      by auto
   1.156 +    finally show False
   1.157 +      using a vs1.dependent_def vs1.independent_Basis
   1.158 +      by (auto simp: p.span_Un span_Times_sing1 span_Times_sing2)
   1.159 +  next
   1.160 +    fix b
   1.161 +    assume b: "b \<in> B2"
   1.162 +    assume "(0, b) \<in> p.span (B1 \<times> {0} \<union> {0} \<times> B2 - {(0, b)})"
   1.163 +    also have "(B1 \<times> {0} \<union> {0} \<times> B2 - {(0, b)}) = B1 \<times> {0} \<union> {0} \<times> (B2 - {b})"
   1.164 +      by auto
   1.165 +    finally show False
   1.166 +      using b vs2.dependent_def vs2.independent_Basis
   1.167 +      by (auto simp: p.span_Un span_Times_sing1 span_Times_sing2)
   1.168 +  qed
   1.169 +  show "p.span Basis_pair = UNIV"
   1.170 +    by (auto simp: p.span_Un span_Times_sing2 span_Times_sing1 vs1.span_Basis vs2.span_Basis
   1.171 +        Basis_pair_def)
   1.172 +qed
   1.173 +
   1.174 +lemma dim_Times:
   1.175 +  assumes "vs1.subspace S" "vs2.subspace T"
   1.176 +  shows "p.dim(S \<times> T) = vs1.dim S + vs2.dim T"
   1.177 +proof -
   1.178 +  interpret p1: Vector_Spaces.linear s1 scale "(\<lambda>x. (x, 0))"
   1.179 +    by unfold_locales (auto simp: scale_def)
   1.180 +  interpret pair1: finite_dimensional_vector_space_pair "( *a)" B1 scale Basis_pair
   1.181 +    by unfold_locales
   1.182 +  interpret p2: Vector_Spaces.linear s2 scale "(\<lambda>x. (0, x))"
   1.183 +    by unfold_locales (auto simp: scale_def)
   1.184 +  interpret pair2: finite_dimensional_vector_space_pair "( *b)" B2 scale Basis_pair
   1.185 +    by unfold_locales
   1.186 +  have ss: "p.subspace ((\<lambda>x. (x, 0)) ` S)" "p.subspace (Pair 0 ` T)"
   1.187 +    by (rule p1.subspace_image p2.subspace_image assms)+
   1.188 +  have "p.dim(S \<times> T) = p.dim({u + v |u v. u \<in> (\<lambda>x. (x, 0)) ` S \<and> v \<in> Pair 0 ` T})"
   1.189 +    by (simp add: Times_eq_image_sum)
   1.190 +  moreover have "p.dim ((\<lambda>x. (x, 0::'c)) ` S) = vs1.dim S" "p.dim (Pair (0::'b) ` T) = vs2.dim T"
   1.191 +     by (simp_all add: inj_on_def p1.linear_axioms pair1.dim_image_eq p2.linear_axioms pair2.dim_image_eq)
   1.192 +  moreover have "p.dim ((\<lambda>x. (x, 0)) ` S \<inter> Pair 0 ` T) = 0"
   1.193 +    by (subst p.dim_eq_0) auto
   1.194 +  ultimately show ?thesis
   1.195 +    using p.dim_sums_Int [OF ss] by linarith
   1.196 +qed
   1.197 +
   1.198 +lemma dimension_pair: "p.dimension = vs1.dimension + vs2.dimension"
   1.199 +  using dim_Times[OF vs1.subspace_UNIV vs2.subspace_UNIV]
   1.200 +  by (auto simp: p.dim_UNIV vs1.dim_UNIV vs2.dim_UNIV
   1.201 +      p.dimension_def vs1.dimension_def vs2.dimension_def)
   1.202 +
   1.203  end
   1.204 +
   1.205 +end