(* 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:

"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

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_on_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_on_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_on_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:

"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 add: divide_pos_pos)

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

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"

then have "0 < r / sqrt 2" (is "0 < ?s")

by (simp add: divide_pos_pos)

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:

"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

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: mult_nonneg_nonneg 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 FDERIV_Pair [FDERIV_intros]:

assumes f: "FDERIV f x : s :> f'" and g: "FDERIV g x : s :> g'"

shows "FDERIV (λx. (f x, g x)) x : s :> (λh. (f' h, g' h))"

proof (rule FDERIV_I_sandwich[of 1])

show "bounded_linear (λh. (f' h, g' h))"

using f g by (intro bounded_linear_Pair FDERIV_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: FDERIV_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 FDERIV_fst [FDERIV_intros] = bounded_linear.FDERIV [OF bounded_linear_fst]

lemmas FDERIV_snd [FDERIV_intros] = bounded_linear.FDERIV [OF bounded_linear_snd]

lemma FDERIV_split [FDERIV_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