(* 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 (\<Union>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))⇧^{2}+ (dist (snd x) (snd y))⇧^{2})" lemma dist_Pair_Pair: "dist (a, b) (c, d) = sqrt ((dist a c)⇧^{2}+ (dist b d)⇧^{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⇧^{2}+ s⇧^{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⇧^{2}+ s⇧^{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))⇧^{2}+ (norm (snd x))⇧^{2})" definition sgn_prod_def: "sgn (x::'a × 'b) = scaleR (inverse (norm x)) x" lemma norm_Pair: "norm (a, b) = sqrt ((norm a)⇧^{2}+ (norm b)⇧^{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 *⇩_{R}x), g (r *⇩_{R}x)) = r *⇩_{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