src/HOL/Multivariate_Analysis/Euclidean_Space.thy

 subsection {* An ordering on euclidean spaces that will allow us to talk about intervals *}
 
 class ordered_euclidean_space = ord + euclidean_space +
   assumes eucl_le: "x \<le> y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i \<le> y $$ i)"
   and eucl_less: "x < y \<longleftrightarrow> (\<forall>i < DIM('a). x $$ i < y $$ i)"
+
+lemma eucl_less_not_refl[simp, intro!]: "\<not> x < (x::'a::ordered_euclidean_space)"
+  unfolding eucl_less[where 'a='a] by auto
+
+lemma euclidean_trans[trans]:
+  fixes x y z :: "'a::ordered_euclidean_space"
+  shows "x < y \<Longrightarrow> y < z \<Longrightarrow> x < z"
+  and "x \<le> y \<Longrightarrow> y < z \<Longrightarrow> x < z"
+  and "x \<le> y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
+  by (force simp: eucl_less[where 'a='a] eucl_le[where 'a='a])+
 
 subsection {* Linearity and Bilinearity continued *}
 
 lemma linear_bounded:
   fixes f:: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"

   by (rule dimension_eq) (auto simp: basis_complex_def)
 
 instance complex :: euclidean_space
   proof qed (auto simp add: basis_complex_def inner_complex_def)
 
+section {* Products Spaces *}
+
+instantiation prod :: (real_basis, real_basis) real_basis
+begin
+
+definition "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))"
+
+instance
+proof
+  let ?b = "basis :: nat \<Rightarrow> 'a \<times> 'b"
+  let ?b_a = "basis :: nat \<Rightarrow> 'a"
+  let ?b_b = "basis :: nat \<Rightarrow> 'b"
+
+  note image_range =
+    image_add_atLeastLessThan[symmetric, of 0 "DIM('a)" "DIM('b)", simplified]
+
+  have split_range:
+    "{..<DIM('b) + DIM('a)} = {..<DIM('a)} \<union> {DIM('a)..<DIM('b) + DIM('a)}"
+    by auto
+  have *: "?b ` {DIM('a)..<DIM('b) + DIM('a)} = {0} \<times> (?b_b ` {..<DIM('b)})"
+    "?b ` {..<DIM('a)} = (?b_a ` {..<DIM('a)}) \<times> {0}"
+    unfolding image_range image_image basis_prod_def_raw range_basis
+    by (auto simp: zero_prod_def basis_eq_0_iff)
+  hence b_split:
+    "?b ` {..<DIM('b) + DIM('a)} = (?b_a ` {..<DIM('a)}) \<times> {0} \<union> {0} \<times> (?b_b ` {..<DIM('b)})" (is "_ = ?prod")
+    by (subst split_range) (simp add: image_Un)
+
+  have b_0: "?b ` {DIM('b) + DIM('a)..} = {0}" unfolding basis_prod_def_raw
+    by (auto simp: zero_prod_def image_iff basis_eq_0_iff elim!: ballE[of _ _ "DIM('a) + DIM('b)"])
+
+  have split_UNIV:
+    "UNIV = {..<DIM('b) + DIM('a)} \<union> {DIM('b)+DIM('a)..}"
+    by auto
+
+  have range_b: "range ?b = ?prod \<union> {0}"
+    by (subst split_UNIV) (simp add: image_Un b_split b_0)
+
+  have prod: "\<And>f A B. setsum f (A \<times> B) = (\<Sum>a\<in>A. \<Sum>b\<in>B. f (a, b))"
+    by (simp add: setsum_cartesian_product)
+
+  show "span (range ?b) = UNIV"
+    unfolding span_explicit range_b
+  proof safe
+    fix a::'a and b::'b
+    from in_span_basis[of a] in_span_basis[of b]
+    obtain Sa ua Sb ub where span:
+        "finite Sa" "Sa \<subseteq> basis ` {..<DIM('a)}" "a = (\<Sum>v\<in>Sa. ua v *\<^sub>R v)"
+        "finite Sb" "Sb \<subseteq> basis ` {..<DIM('b)}" "b = (\<Sum>v\<in>Sb. ub v *\<^sub>R v)"
+      unfolding span_explicit by auto
+
+    let ?S = "((Sa - {0}) \<times> {0} \<union> {0} \<times> (Sb - {0}))"
+    have *:
+      "?S \<inter> {v. fst v = 0} \<inter> {v. snd v = 0} = {}"
+      "?S \<inter> - {v. fst v = 0} \<inter> {v. snd v = 0} = (Sa - {0}) \<times> {0}"
+      "?S \<inter> {v. fst v = 0} \<inter> - {v. snd v = 0} = {0} \<times> (Sb - {0})"
+      by (auto simp: zero_prod_def)
+    show "\<exists>S u. finite S \<and> S \<subseteq> ?prod \<union> {0} \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = (a, b)"
+      apply (rule exI[of _ ?S])
+      apply (rule exI[of _ "\<lambda>(v, w). (if w = 0 then ua v else 0) + (if v = 0 then ub w else 0)"])
+      using span
+      apply (simp add: prod_case_unfold setsum_addf if_distrib cond_application_beta setsum_cases prod *)
+      by (auto simp add: setsum_prod intro!: setsum_mono_zero_cong_left)
+  qed simp
+
+  show "\<exists>d>0. ?b ` {d..} = {0} \<and> independent (?b ` {..<d}) \<and> inj_on ?b {..<d}"
+    apply (rule exI[of _ "DIM('b) + DIM('a)"]) unfolding b_0
+  proof (safe intro!: DIM_positive del: notI)
+    show inj_on: "inj_on ?b {..<DIM('b) + DIM('a)}" unfolding split_range
+      using inj_on_iff[OF basis_inj[where 'a='a]] inj_on_iff[OF basis_inj[where 'a='b]]
+      by (auto intro!: inj_onI simp: basis_prod_def basis_eq_0_iff)
+
+    show "independent (?b ` {..<DIM('b) + DIM('a)})"
+      unfolding independent_eq_inj_on[OF inj_on]
+    proof safe
+      fix i u assume i_upper: "i < DIM('b) + DIM('a)" and
+          "(\<Sum>j\<in>{..<DIM('b) + DIM('a)} - {i}. u (?b j) *\<^sub>R ?b j) = ?b i" (is "?SUM = _")
+      let ?left = "{..<DIM('a)}" and ?right = "{DIM('a)..<DIM('b) + DIM('a)}"
+      show False
+      proof cases
+        assume "i < DIM('a)"
+        hence "(basis i, 0) = ?SUM" unfolding `?SUM = ?b i` unfolding basis_prod_def by auto
+        also have "\<dots> = (\<Sum>j\<in>?left - {i}. u (?b j) *\<^sub>R ?b j) +
+          (\<Sum>j\<in>?right. u (?b j) *\<^sub>R ?b j)"
+          using `i < DIM('a)` by (subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
+        also have "\<dots> =  (\<Sum>j\<in>?left - {i}. u (?b_a j, 0) *\<^sub>R (?b_a j, 0)) +
+          (\<Sum>j\<in>?right. u (0, ?b_b (j-DIM('a))) *\<^sub>R (0, ?b_b (j-DIM('a))))"
+          unfolding basis_prod_def by auto
+        finally have "basis i = (\<Sum>j\<in>?left - {i}. u (?b_a j, 0) *\<^sub>R ?b_a j)"
+          by (simp add: setsum_prod)
+        moreover
+        note independent_basis[where 'a='a, unfolded independent_eq_inj_on[OF basis_inj]]
+        note this[rule_format, of i "\<lambda>v. u (v, 0)"]
+        ultimately show False using `i < DIM('a)` by auto
+      next
+        let ?i = "i - DIM('a)"
+        assume not: "\<not> i < DIM('a)" hence "DIM('a) \<le> i" by auto
+        hence "?i < DIM('b)" using `i < DIM('b) + DIM('a)` by auto
+
+        have inj_on: "inj_on (\<lambda>j. j - DIM('a)) {DIM('a)..<DIM('b) + DIM('a)}"
+          by (auto intro!: inj_onI)
+        with i_upper not have *: "{..<DIM('b)} - {?i} = (\<lambda>j. j-DIM('a))`(?right - {i})"
+          by (auto simp: inj_on_image_set_diff image_minus_const_atLeastLessThan_nat)
+
+        have "(0, basis ?i) = ?SUM" unfolding `?SUM = ?b i`
+          unfolding basis_prod_def using not `?i < DIM('b)` by auto
+        also have "\<dots> = (\<Sum>j\<in>?left. u (?b j) *\<^sub>R ?b j) +
+          (\<Sum>j\<in>?right - {i}. u (?b j) *\<^sub>R ?b j)"
+          using not by (subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
+        also have "\<dots> =  (\<Sum>j\<in>?left. u (?b_a j, 0) *\<^sub>R (?b_a j, 0)) +
+          (\<Sum>j\<in>?right - {i}. u (0, ?b_b (j-DIM('a))) *\<^sub>R (0, ?b_b (j-DIM('a))))"
+          unfolding basis_prod_def by auto
+        finally have "basis ?i = (\<Sum>j\<in>{..<DIM('b)} - {?i}. u (0, ?b_b j) *\<^sub>R ?b_b j)"
+          unfolding *
+          by (subst setsum_reindex[OF inj_on[THEN subset_inj_on]])
+             (auto simp: setsum_prod)
+        moreover
+        note independent_basis[where 'a='b, unfolded independent_eq_inj_on[OF basis_inj]]
+        note this[rule_format, of ?i "\<lambda>v. u (0, v)"]
+        ultimately show False using `?i < DIM('b)` by auto
+      qed
+    qed
+  qed
+qed
 end
+
+lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::real_basis) + DIM('a::real_basis)"
+  by (rule dimension_eq) (auto simp: basis_prod_def zero_prod_def basis_eq_0_iff)
+
+instance prod :: (euclidean_space, euclidean_space) euclidean_space
+proof (default, safe)
+  let ?b = "basis :: nat \<Rightarrow> 'a \<times> 'b"
+  fix i j assume "i < DIM('a \<times> 'b)" "j < DIM('a \<times> 'b)"
+  thus "?b i \<bullet> ?b j = (if i = j then 1 else 0)"
+    unfolding basis_prod_def by (auto simp: dot_basis)
+qed
+
+instantiation prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
+begin
+
+definition "x \<le> (y::('a\<times>'b)) \<longleftrightarrow> (\<forall>i<DIM('a\<times>'b). x $$ i \<le> y $$ i)"
+definition "x < (y::('a\<times>'b)) \<longleftrightarrow> (\<forall>i<DIM('a\<times>'b). x $$ i < y $$ i)"
+
+instance proof qed (auto simp: less_prod_def less_eq_prod_def)
+end
+
+
+end