(* Title: HOL/Library/Product_Vector.thy Author: Brian Huffman *) header {* Cartesian Products as Vector Spaces *} theory Product_Vector imports Inner_Product Product_plus begin subsection {* Product is a real vector space *} instantiation prod :: (real_vector, real_vector) real_vector begin definition scaleR_prod_def: "scaleR r A = (scaleR r (fst A), scaleR r (snd A))" lemma fst_scaleR [simp]: "fst (scaleR r A) = scaleR r (fst A)" unfolding scaleR_prod_def by simp lemma snd_scaleR [simp]: "snd (scaleR r A) = scaleR r (snd A)" unfolding scaleR_prod_def by simp lemma scaleR_Pair [simp]: "scaleR r (a, b) = (scaleR r a, scaleR r b)" unfolding scaleR_prod_def by simp instance proof fix a b :: real and x y :: "'a \ 'b" show "scaleR a (x + y) = scaleR a x + scaleR a y" by (simp add: prod_eq_iff scaleR_right_distrib) show "scaleR (a + b) x = scaleR a x + scaleR b x" by (simp add: prod_eq_iff scaleR_left_distrib) show "scaleR a (scaleR b x) = scaleR (a * b) x" by (simp add: prod_eq_iff) show "scaleR 1 x = x" by (simp add: prod_eq_iff) qed end subsection {* Product is a topological space *} instantiation prod :: (topological_space, topological_space) topological_space begin definition open_prod_def[code del]: "open (S :: ('a \ 'b) set) \ (\x\S. \A B. open A \ open B \ x \ A \ B \ A \ B \ S)" lemma open_prod_elim: assumes "open S" and "x \ S" obtains A B where "open A" and "open B" and "x \ A \ B" and "A \ B \ S" using assms unfolding open_prod_def by fast lemma open_prod_intro: assumes "\x. x \ S \ \A B. open A \ open B \ x \ A \ B \ A \ B \ S" shows "open S" using assms unfolding open_prod_def by fast instance proof show "open (UNIV :: ('a \ 'b) set)" unfolding open_prod_def by auto next fix S T :: "('a \ 'b) set" assume "open S" "open T" show "open (S \ T)" proof (rule open_prod_intro) fix x assume x: "x \ S \ T" from x have "x \ S" by simp obtain Sa Sb where A: "open Sa" "open Sb" "x \ Sa \ Sb" "Sa \ Sb \ S" using `open S` and `x \ S` by (rule open_prod_elim) from x have "x \ T" by simp obtain Ta Tb where B: "open Ta" "open Tb" "x \ Ta \ Tb" "Ta \ Tb \ T" using `open T` and `x \ T` by (rule open_prod_elim) let ?A = "Sa \ Ta" and ?B = "Sb \ Tb" have "open ?A \ open ?B \ x \ ?A \ ?B \ ?A \ ?B \ S \ T" using A B by (auto simp add: open_Int) thus "\A B. open A \ open B \ x \ A \ B \ A \ B \ S \ T" by fast qed next fix K :: "('a \ 'b) set set" assume "\S\K. open S" thus "open (\K)" unfolding open_prod_def by fast qed end declare [[code abort: "open::('a::topological_space*'b::topological_space) set \ bool"]] lemma open_Times: "open S \ open T \ open (S \ T)" unfolding open_prod_def by auto lemma fst_vimage_eq_Times: "fst -` S = S \ UNIV" by auto lemma snd_vimage_eq_Times: "snd -` S = UNIV \ S" by auto lemma open_vimage_fst: "open S \ open (fst -` S)" by (simp add: fst_vimage_eq_Times open_Times) lemma open_vimage_snd: "open S \ open (snd -` S)" by (simp add: snd_vimage_eq_Times open_Times) lemma closed_vimage_fst: "closed S \ closed (fst -` S)" unfolding closed_open vimage_Compl [symmetric] by (rule open_vimage_fst) lemma closed_vimage_snd: "closed S \ closed (snd -` S)" unfolding closed_open vimage_Compl [symmetric] by (rule open_vimage_snd) lemma closed_Times: "closed S \ closed T \ closed (S \ T)" proof - have "S \ T = (fst -` S) \ (snd -` T)" by auto thus "closed S \ closed T \ closed (S \ T)" by (simp add: closed_vimage_fst closed_vimage_snd closed_Int) qed lemma subset_fst_imageI: "A \ B \ S \ y \ B \ A \ fst ` S" unfolding image_def subset_eq by force lemma subset_snd_imageI: "A \ B \ S \ x \ A \ B \ snd ` S" unfolding image_def subset_eq by force lemma open_image_fst: assumes "open S" shows "open (fst ` S)" proof (rule openI) fix x assume "x \ fst ` S" then obtain y where "(x, y) \ S" by auto then obtain A B where "open A" "open B" "x \ A" "y \ B" "A \ B \ S" using `open S` unfolding open_prod_def by auto from `A \ B \ S` `y \ B` have "A \ fst ` S" by (rule subset_fst_imageI) with `open A` `x \ A` have "open A \ x \ A \ A \ fst ` S" by simp then show "\T. open T \ x \ T \ T \ fst ` S" by - (rule exI) qed lemma open_image_snd: assumes "open S" shows "open (snd ` S)" proof (rule openI) fix y assume "y \ snd ` S" then obtain x where "(x, y) \ S" by auto then obtain A B where "open A" "open B" "x \ A" "y \ B" "A \ B \ S" using `open S` unfolding open_prod_def by auto from `A \ B \ S` `x \ A` have "B \ snd ` S" by (rule subset_snd_imageI) with `open B` `y \ B` have "open B \ y \ B \ B \ snd ` S" by simp then show "\T. open T \ y \ T \ T \ snd ` S" by - (rule exI) qed subsubsection {* Continuity of operations *} lemma tendsto_fst [tendsto_intros]: assumes "(f ---> a) F" shows "((\x. fst (f x)) ---> fst a) F" proof (rule topological_tendstoI) fix S assume "open S" and "fst a \ S" then have "open (fst -` S)" and "a \ fst -` S" by (simp_all add: open_vimage_fst) with assms have "eventually (\x. f x \ fst -` S) F" by (rule topological_tendstoD) then show "eventually (\x. fst (f x) \ S) F" by simp qed lemma tendsto_snd [tendsto_intros]: assumes "(f ---> a) F" shows "((\x. snd (f x)) ---> snd a) F" proof (rule topological_tendstoI) fix S assume "open S" and "snd a \ S" then have "open (snd -` S)" and "a \ snd -` S" by (simp_all add: open_vimage_snd) with assms have "eventually (\x. f x \ snd -` S) F" by (rule topological_tendstoD) then show "eventually (\x. snd (f x) \ S) F" by simp qed lemma tendsto_Pair [tendsto_intros]: assumes "(f ---> a) F" and "(g ---> b) F" shows "((\x. (f x, g x)) ---> (a, b)) F" proof (rule topological_tendstoI) fix S assume "open S" and "(a, b) \ S" then obtain A B where "open A" "open B" "a \ A" "b \ B" "A \ B \ S" unfolding open_prod_def by fast have "eventually (\x. f x \ A) F" using `(f ---> a) F` `open A` `a \ A` by (rule topological_tendstoD) moreover have "eventually (\x. g x \ B) F" using `(g ---> b) F` `open B` `b \ B` by (rule topological_tendstoD) ultimately show "eventually (\x. (f x, g x) \ S) F" by (rule eventually_elim2) (simp add: subsetD [OF `A \ B \ S`]) qed lemma continuous_fst[continuous_intros]: "continuous F f \ continuous F (\x. fst (f x))" unfolding continuous_def by (rule tendsto_fst) lemma continuous_snd[continuous_intros]: "continuous F f \ continuous F (\x. snd (f x))" unfolding continuous_def by (rule tendsto_snd) lemma continuous_Pair[continuous_intros]: "continuous F f \ continuous F g \ continuous F (\x. (f x, g x))" unfolding continuous_def by (rule tendsto_Pair) lemma continuous_on_fst[continuous_intros]: "continuous_on s f \ continuous_on s (\x. fst (f x))" unfolding continuous_on_def by (auto intro: tendsto_fst) lemma continuous_on_snd[continuous_intros]: "continuous_on s f \ continuous_on s (\x. snd (f x))" unfolding continuous_on_def by (auto intro: tendsto_snd) lemma continuous_on_Pair[continuous_intros]: "continuous_on s f \ continuous_on s g \ continuous_on s (\x. (f x, g x))" unfolding continuous_on_def by (auto intro: tendsto_Pair) lemma isCont_fst [simp]: "isCont f a \ isCont (\x. fst (f x)) a" by (fact continuous_fst) lemma isCont_snd [simp]: "isCont f a \ isCont (\x. snd (f x)) a" by (fact continuous_snd) lemma isCont_Pair [simp]: "\isCont f a; isCont g a\ \ isCont (\x. (f x, g x)) a" by (fact continuous_Pair) subsubsection {* Separation axioms *} lemma mem_Times_iff: "x \ A \ B \ fst x \ A \ snd x \ B" by (induct x) simp (* TODO: move elsewhere *) instance prod :: (t0_space, t0_space) t0_space proof fix x y :: "'a \ 'b" assume "x \ y" hence "fst x \ fst y \ snd x \ snd y" by (simp add: prod_eq_iff) thus "\U. open U \ (x \ U) \ (y \ U)" by (fast dest: t0_space elim: open_vimage_fst open_vimage_snd) qed instance prod :: (t1_space, t1_space) t1_space proof fix x y :: "'a \ 'b" assume "x \ y" hence "fst x \ fst y \ snd x \ snd y" by (simp add: prod_eq_iff) thus "\U. open U \ x \ U \ y \ U" by (fast dest: t1_space elim: open_vimage_fst open_vimage_snd) qed instance prod :: (t2_space, t2_space) t2_space proof fix x y :: "'a \ 'b" assume "x \ y" hence "fst x \ fst y \ snd x \ snd y" by (simp add: prod_eq_iff) thus "\U V. open U \ open V \ x \ U \ y \ V \ U \ V = {}" by (fast dest: hausdorff elim: open_vimage_fst open_vimage_snd) qed subsection {* Product is a metric space *} instantiation prod :: (metric_space, metric_space) metric_space begin definition dist_prod_def[code del]: "dist x y = sqrt ((dist (fst x) (fst y))\<^sup>2 + (dist (snd x) (snd y))\<^sup>2)" lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)\<^sup>2 + (dist b d)\<^sup>2)" unfolding dist_prod_def by simp lemma dist_fst_le: "dist (fst x) (fst y) \ dist x y" unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge1) lemma dist_snd_le: "dist (snd x) (snd y) \ dist x y" unfolding dist_prod_def by (rule real_sqrt_sum_squares_ge2) instance proof fix x y :: "'a \ 'b" show "dist x y = 0 \ x = y" unfolding dist_prod_def prod_eq_iff by simp next fix x y z :: "'a \ 'b" show "dist x y \ dist x z + dist y z" unfolding dist_prod_def by (intro order_trans [OF _ real_sqrt_sum_squares_triangle_ineq] real_sqrt_le_mono add_mono power_mono dist_triangle2 zero_le_dist) next fix S :: "('a \ 'b) set" show "open S \ (\x\S. \e>0. \y. dist y x < e \ y \ S)" proof assume "open S" show "\x\S. \e>0. \y. dist y x < e \ y \ S" proof fix x assume "x \ S" obtain A B where "open A" "open B" "x \ A \ B" "A \ B \ S" using `open S` and `x \ S` by (rule open_prod_elim) obtain r where r: "0 < r" "\y. dist y (fst x) < r \ y \ A" using `open A` and `x \ A \ B` unfolding open_dist by auto obtain s where s: "0 < s" "\y. dist y (snd x) < s \ y \ B" using `open B` and `x \ A \ B` unfolding open_dist by auto let ?e = "min r s" have "0 < ?e \ (\y. dist y x < ?e \ y \ S)" proof (intro allI impI conjI) show "0 < min r s" by (simp add: r(1) s(1)) next fix y assume "dist y x < min r s" hence "dist y x < r" and "dist y x < s" by simp_all hence "dist (fst y) (fst x) < r" and "dist (snd y) (snd x) < s" by (auto intro: le_less_trans dist_fst_le dist_snd_le) hence "fst y \ A" and "snd y \ B" by (simp_all add: r(2) s(2)) hence "y \ A \ B" by (induct y, simp) with `A \ B \ S` show "y \ S" .. qed thus "\e>0. \y. dist y x < e \ y \ S" .. qed next assume *: "\x\S. \e>0. \y. dist y x < e \ y \ S" show "open S" proof (rule open_prod_intro) fix x assume "x \ S" then obtain e where "0 < e" and S: "\y. dist y x < e \ y \ S" using * by fast def r \ "e / sqrt 2" and s \ "e / sqrt 2" from `0 < e` have "0 < r" and "0 < s" unfolding r_def s_def by simp_all from `0 < e` have "e = sqrt (r\<^sup>2 + s\<^sup>2)" unfolding r_def s_def by (simp add: power_divide) def A \ "{y. dist (fst x) y < r}" and B \ "{y. dist (snd x) y < s}" have "open A" and "open B" unfolding A_def B_def by (simp_all add: open_ball) moreover have "x \ A \ B" unfolding A_def B_def mem_Times_iff using `0 < r` and `0 < s` by simp moreover have "A \ B \ S" proof (clarify) fix a b assume "a \ A" and "b \ B" hence "dist a (fst x) < r" and "dist b (snd x) < s" unfolding A_def B_def by (simp_all add: dist_commute) hence "dist (a, b) x < e" unfolding dist_prod_def `e = sqrt (r\<^sup>2 + s\<^sup>2)` by (simp add: add_strict_mono power_strict_mono) thus "(a, b) \ S" by (simp add: S) qed ultimately show "\A B. open A \ open B \ x \ A \ B \ A \ B \ S" by fast qed qed qed end declare [[code abort: "dist::('a::metric_space*'b::metric_space)\('a*'b) \ real"]] lemma Cauchy_fst: "Cauchy X \ Cauchy (\n. fst (X n))" unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_fst_le]) lemma Cauchy_snd: "Cauchy X \ Cauchy (\n. snd (X n))" unfolding Cauchy_def by (fast elim: le_less_trans [OF dist_snd_le]) lemma Cauchy_Pair: assumes "Cauchy X" and "Cauchy Y" shows "Cauchy (\n. (X n, Y n))" proof (rule metric_CauchyI) fix r :: real assume "0 < r" hence "0 < r / sqrt 2" (is "0 < ?s") by simp obtain M where M: "\m\M. \n\M. dist (X m) (X n) < ?s" using metric_CauchyD [OF `Cauchy X` `0 < ?s`] .. obtain N where N: "\m\N. \n\N. dist (Y m) (Y n) < ?s" using metric_CauchyD [OF `Cauchy Y` `0 < ?s`] .. have "\m\max M N. \n\max M N. dist (X m, Y m) (X n, Y n) < r" using M N by (simp add: real_sqrt_sum_squares_less dist_Pair_Pair) then show "\n0. \m\n0. \n\n0. dist (X m, Y m) (X n, Y n) < r" .. qed subsection {* Product is a complete metric space *} instance prod :: (complete_space, complete_space) complete_space proof fix X :: "nat \ 'a \ 'b" assume "Cauchy X" have 1: "(\n. fst (X n)) ----> lim (\n. fst (X n))" using Cauchy_fst [OF `Cauchy X`] by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) have 2: "(\n. snd (X n)) ----> lim (\n. snd (X n))" using Cauchy_snd [OF `Cauchy X`] by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) have "X ----> (lim (\n. fst (X n)), lim (\n. snd (X n)))" using tendsto_Pair [OF 1 2] by simp then show "convergent X" by (rule convergentI) qed subsection {* Product is a normed vector space *} instantiation prod :: (real_normed_vector, real_normed_vector) real_normed_vector begin definition norm_prod_def[code del]: "norm x = sqrt ((norm (fst x))\<^sup>2 + (norm (snd x))\<^sup>2)" definition sgn_prod_def: "sgn (x::'a \ 'b) = scaleR (inverse (norm x)) x" lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<^sup>2 + (norm b)\<^sup>2)" unfolding norm_prod_def by simp instance proof fix r :: real and x y :: "'a \ 'b" show "norm x = 0 \ x = 0" unfolding norm_prod_def by (simp add: prod_eq_iff) show "norm (x + y) \ norm x + norm y" unfolding norm_prod_def apply (rule order_trans [OF _ real_sqrt_sum_squares_triangle_ineq]) apply (simp add: add_mono power_mono norm_triangle_ineq) done show "norm (scaleR r x) = \r\ * norm x" unfolding norm_prod_def apply (simp add: power_mult_distrib) apply (simp add: distrib_left [symmetric]) apply (simp add: real_sqrt_mult_distrib) done show "sgn x = scaleR (inverse (norm x)) x" by (rule sgn_prod_def) show "dist x y = norm (x - y)" unfolding dist_prod_def norm_prod_def by (simp add: dist_norm) qed end declare [[code abort: "norm::('a::real_normed_vector*'b::real_normed_vector) \ real"]] instance prod :: (banach, banach) banach .. subsubsection {* Pair operations are linear *} lemma bounded_linear_fst: "bounded_linear fst" using fst_add fst_scaleR by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) lemma bounded_linear_snd: "bounded_linear snd" using snd_add snd_scaleR by (rule bounded_linear_intro [where K=1], simp add: norm_prod_def) text {* TODO: move to NthRoot *} lemma sqrt_add_le_add_sqrt: assumes x: "0 \ x" and y: "0 \ y" shows "sqrt (x + y) \ sqrt x + sqrt y" apply (rule power2_le_imp_le) apply (simp add: power2_sum x y) apply (simp add: x y) done lemma bounded_linear_Pair: assumes f: "bounded_linear f" assumes g: "bounded_linear g" shows "bounded_linear (\x. (f x, g x))" proof interpret f: bounded_linear f by fact interpret g: bounded_linear g by fact fix x y and r :: real show "(f (x + y), g (x + y)) = (f x, g x) + (f y, g y)" by (simp add: f.add g.add) show "(f (r *\<^sub>R x), g (r *\<^sub>R x)) = r *\<^sub>R (f x, g x)" by (simp add: f.scaleR g.scaleR) obtain Kf where "0 < Kf" and norm_f: "\x. norm (f x) \ norm x * Kf" using f.pos_bounded by fast obtain Kg where "0 < Kg" and norm_g: "\x. norm (g x) \ norm x * Kg" using g.pos_bounded by fast have "\x. norm (f x, g x) \ norm x * (Kf + Kg)" apply (rule allI) apply (simp add: norm_Pair) apply (rule order_trans [OF sqrt_add_le_add_sqrt], simp, simp) apply (simp add: distrib_left) apply (rule add_mono [OF norm_f norm_g]) done then show "\K. \x. norm (f x, g x) \ norm x * K" .. qed subsubsection {* Frechet derivatives involving pairs *} lemma has_derivative_Pair [derivative_intros]: assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)" shows "((\x. (f x, g x)) has_derivative (\h. (f' h, g' h))) (at x within s)" proof (rule has_derivativeI_sandwich[of 1]) show "bounded_linear (\h. (f' h, g' h))" using f g by (intro bounded_linear_Pair has_derivative_bounded_linear) let ?Rf = "\y. f y - f x - f' (y - x)" let ?Rg = "\y. g y - g x - g' (y - x)" let ?R = "\y. ((f y, g y) - (f x, g x) - (f' (y - x), g' (y - x)))" show "((\y. norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)) ---> 0) (at x within s)" using f g by (intro tendsto_add_zero) (auto simp: has_derivative_iff_norm) fix y :: 'a assume "y \ x" show "norm (?R y) / norm (y - x) \ norm (?Rf y) / norm (y - x) + norm (?Rg y) / norm (y - x)" unfolding add_divide_distrib [symmetric] by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt]) qed simp lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst] lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd] lemma has_derivative_split [derivative_intros]: "((\p. f (fst p) (snd p)) has_derivative f') F \ ((\(a, b). f a b) has_derivative f') F" unfolding split_beta' . subsection {* Product is an inner product space *} instantiation prod :: (real_inner, real_inner) real_inner begin definition inner_prod_def: "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)" lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d" unfolding inner_prod_def by simp instance proof fix r :: real fix x y z :: "'a::real_inner \ 'b::real_inner" show "inner x y = inner y x" unfolding inner_prod_def by (simp add: inner_commute) show "inner (x + y) z = inner x z + inner y z" unfolding inner_prod_def by (simp add: inner_add_left) show "inner (scaleR r x) y = r * inner x y" unfolding inner_prod_def by (simp add: distrib_left) show "0 \ inner x x" unfolding inner_prod_def by (intro add_nonneg_nonneg inner_ge_zero) show "inner x x = 0 \ x = 0" unfolding inner_prod_def prod_eq_iff by (simp add: add_nonneg_eq_0_iff) show "norm x = sqrt (inner x x)" unfolding norm_prod_def inner_prod_def by (simp add: power2_norm_eq_inner) qed end end