src/HOL/Multivariate_Analysis/Euclidean_Space.thy
 changeset 63627 6ddb43c6b711 parent 63626 44ce6b524ff3 child 63631 2edc8da89edc child 63633 2accfb71e33b
1.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Aug 05 18:34:57 2016 +0200
1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,224 +0,0 @@
1.4 -(*  Title:      HOL/Multivariate_Analysis/Euclidean_Space.thy
1.5 -    Author:     Johannes Hölzl, TU München
1.6 -    Author:     Brian Huffman, Portland State University
1.7 -*)
1.8 -
1.9 -section \<open>Finite-Dimensional Inner Product Spaces\<close>
1.10 -
1.11 -theory Euclidean_Space
1.12 -imports
1.13 -  L2_Norm
1.14 -  "~~/src/HOL/Library/Inner_Product"
1.15 -  "~~/src/HOL/Library/Product_Vector"
1.16 -begin
1.17 -
1.18 -subsection \<open>Type class of Euclidean spaces\<close>
1.19 -
1.20 -class euclidean_space = real_inner +
1.21 -  fixes Basis :: "'a set"
1.22 -  assumes nonempty_Basis [simp]: "Basis \<noteq> {}"
1.23 -  assumes finite_Basis [simp]: "finite Basis"
1.24 -  assumes inner_Basis:
1.25 -    "\<lbrakk>u \<in> Basis; v \<in> Basis\<rbrakk> \<Longrightarrow> inner u v = (if u = v then 1 else 0)"
1.26 -  assumes euclidean_all_zero_iff:
1.27 -    "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
1.28 -
1.29 -syntax "_type_dimension" :: "type \<Rightarrow> nat"  ("(1DIM/(1'(_')))")
1.30 -translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)"
1.31 -typed_print_translation \<open>
1.32 -  [(@{const_syntax card},
1.33 -    fn ctxt => fn _ => fn [Const (@{const_syntax Basis}, Type (@{type_name set}, [T]))] =>
1.34 -      Syntax.const @{syntax_const "_type_dimension"} \$ Syntax_Phases.term_of_typ ctxt T)]
1.35 -\<close>
1.36 -
1.37 -lemma (in euclidean_space) norm_Basis[simp]: "u \<in> Basis \<Longrightarrow> norm u = 1"
1.38 -  unfolding norm_eq_sqrt_inner by (simp add: inner_Basis)
1.39 -
1.40 -lemma (in euclidean_space) inner_same_Basis[simp]: "u \<in> Basis \<Longrightarrow> inner u u = 1"
1.41 -  by (simp add: inner_Basis)
1.42 -
1.43 -lemma (in euclidean_space) inner_not_same_Basis: "u \<in> Basis \<Longrightarrow> v \<in> Basis \<Longrightarrow> u \<noteq> v \<Longrightarrow> inner u v = 0"
1.44 -  by (simp add: inner_Basis)
1.45 -
1.46 -lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u"
1.47 -  unfolding sgn_div_norm by (simp add: scaleR_one)
1.48 -
1.49 -lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis"
1.50 -proof
1.51 -  assume "0 \<in> Basis" thus "False"
1.52 -    using inner_Basis [of 0 0] by simp
1.53 -qed
1.54 -
1.55 -lemma (in euclidean_space) nonzero_Basis: "u \<in> Basis \<Longrightarrow> u \<noteq> 0"
1.56 -  by clarsimp
1.57 -
1.58 -lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis"
1.59 -  by (metis ex_in_conv nonempty_Basis someI_ex)
1.60 -
1.61 -lemma (in euclidean_space) inner_setsum_left_Basis[simp]:
1.62 -    "b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b"
1.64 -
1.65 -lemma (in euclidean_space) euclidean_eqI:
1.66 -  assumes b: "\<And>b. b \<in> Basis \<Longrightarrow> inner x b = inner y b" shows "x = y"
1.67 -proof -
1.68 -  from b have "\<forall>b\<in>Basis. inner (x - y) b = 0"
1.69 -    by (simp add: inner_diff_left)
1.70 -  then show "x = y"
1.71 -    by (simp add: euclidean_all_zero_iff)
1.72 -qed
1.73 -
1.74 -lemma (in euclidean_space) euclidean_eq_iff:
1.75 -  "x = y \<longleftrightarrow> (\<forall>b\<in>Basis. inner x b = inner y b)"
1.76 -  by (auto intro: euclidean_eqI)
1.77 -
1.78 -lemma (in euclidean_space) euclidean_representation_setsum:
1.79 -  "(\<Sum>i\<in>Basis. f i *\<^sub>R i) = b \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
1.80 -  by (subst euclidean_eq_iff) simp
1.81 -
1.82 -lemma (in euclidean_space) euclidean_representation_setsum':
1.83 -  "b = (\<Sum>i\<in>Basis. f i *\<^sub>R i) \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
1.84 -  by (auto simp add: euclidean_representation_setsum[symmetric])
1.85 -
1.86 -lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
1.87 -  unfolding euclidean_representation_setsum by simp
1.88 -
1.89 -lemma (in euclidean_space) choice_Basis_iff:
1.90 -  fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
1.91 -  shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))"
1.92 -  unfolding bchoice_iff
1.93 -proof safe
1.94 -  fix f assume "\<forall>i\<in>Basis. P i (f i)"
1.95 -  then show "\<exists>x. \<forall>i\<in>Basis. P i (inner x i)"
1.96 -    by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"])
1.97 -qed auto
1.98 -
1.99 -lemma (in euclidean_space) euclidean_representation_setsum_fun:
1.100 -    "(\<lambda>x. \<Sum>b\<in>Basis. inner (f x) b *\<^sub>R b) = f"
1.101 -  by (rule ext) (simp add: euclidean_representation_setsum)
1.103 -lemma euclidean_isCont:
1.104 -  assumes "\<And>b. b \<in> Basis \<Longrightarrow> isCont (\<lambda>x. (inner (f x) b) *\<^sub>R b) x"
1.105 -    shows "isCont f x"
1.106 -  apply (subst euclidean_representation_setsum_fun [symmetric])
1.107 -  apply (rule isCont_setsum)
1.108 -  apply (blast intro: assms)
1.109 -  done
1.111 -lemma DIM_positive: "0 < DIM('a::euclidean_space)"
1.112 -  by (simp add: card_gt_0_iff)
1.114 -lemma DIM_ge_Suc0 [iff]: "Suc 0 \<le> card Basis"
1.115 -  by (meson DIM_positive Suc_leI)
1.118 -lemma setsum_inner_Basis_scaleR [simp]:
1.119 -  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_vector"
1.120 -  assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) *\<^sub>R f i) = f b"
1.124 -lemma setsum_inner_Basis_eq [simp]:
1.125 -  assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) * f i) = f b"
1.129 -subsection \<open>Subclass relationships\<close>
1.131 -instance euclidean_space \<subseteq> perfect_space
1.132 -proof
1.133 -  fix x :: 'a show "\<not> open {x}"
1.134 -  proof
1.135 -    assume "open {x}"
1.136 -    then obtain e where "0 < e" and e: "\<forall>y. dist y x < e \<longrightarrow> y = x"
1.137 -      unfolding open_dist by fast
1.138 -    define y where "y = x + scaleR (e/2) (SOME b. b \<in> Basis)"
1.139 -    have [simp]: "(SOME b. b \<in> Basis) \<in> Basis"
1.140 -      by (rule someI_ex) (auto simp: ex_in_conv)
1.141 -    from \<open>0 < e\<close> have "y \<noteq> x"
1.142 -      unfolding y_def by (auto intro!: nonzero_Basis)
1.143 -    from \<open>0 < e\<close> have "dist y x < e"
1.144 -      unfolding y_def by (simp add: dist_norm)
1.145 -    from \<open>y \<noteq> x\<close> and \<open>dist y x < e\<close> show "False"
1.146 -      using e by simp
1.147 -  qed
1.148 -qed
1.150 -subsection \<open>Class instances\<close>
1.152 -subsubsection \<open>Type @{typ real}\<close>
1.154 -instantiation real :: euclidean_space
1.155 -begin
1.157 -definition
1.158 -  [simp]: "Basis = {1::real}"
1.160 -instance
1.161 -  by standard auto
1.163 -end
1.165 -lemma DIM_real[simp]: "DIM(real) = 1"
1.166 -  by simp
1.168 -subsubsection \<open>Type @{typ complex}\<close>
1.170 -instantiation complex :: euclidean_space
1.171 -begin
1.173 -definition Basis_complex_def: "Basis = {1, \<i>}"
1.175 -instance
1.176 -  by standard (auto simp add: Basis_complex_def intro: complex_eqI split: if_split_asm)
1.178 -end
1.180 -lemma DIM_complex[simp]: "DIM(complex) = 2"
1.181 -  unfolding Basis_complex_def by simp
1.183 -subsubsection \<open>Type @{typ "'a \<times> 'b"}\<close>
1.185 -instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
1.186 -begin
1.188 -definition
1.189 -  "Basis = (\<lambda>u. (u, 0)) ` Basis \<union> (\<lambda>v. (0, v)) ` Basis"
1.191 -lemma setsum_Basis_prod_eq:
1.192 -  fixes f::"('a*'b)\<Rightarrow>('a*'b)"
1.193 -  shows "setsum f Basis = setsum (\<lambda>i. f (i, 0)) Basis + setsum (\<lambda>i. f (0, i)) Basis"
1.194 -proof -
1.195 -  have "inj_on (\<lambda>u. (u::'a, 0::'b)) Basis" "inj_on (\<lambda>u. (0::'a, u::'b)) Basis"
1.196 -    by (auto intro!: inj_onI Pair_inject)
1.197 -  thus ?thesis
1.198 -    unfolding Basis_prod_def
1.199 -    by (subst setsum.union_disjoint) (auto simp: Basis_prod_def setsum.reindex)
1.200 -qed
1.202 -instance proof
1.203 -  show "(Basis :: ('a \<times> 'b) set) \<noteq> {}"
1.204 -    unfolding Basis_prod_def by simp
1.205 -next
1.206 -  show "finite (Basis :: ('a \<times> 'b) set)"
1.207 -    unfolding Basis_prod_def by simp
1.208 -next
1.209 -  fix u v :: "'a \<times> 'b"
1.210 -  assume "u \<in> Basis" and "v \<in> Basis"
1.211 -  thus "inner u v = (if u = v then 1 else 0)"
1.212 -    unfolding Basis_prod_def inner_prod_def
1.213 -    by (auto simp add: inner_Basis split: if_split_asm)
1.214 -next
1.215 -  fix x :: "'a \<times> 'b"
1.216 -  show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
1.217 -    unfolding Basis_prod_def ball_Un ball_simps
1.218 -    by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff)
1.219 -qed
1.221 -lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('a) + DIM('b)"
1.222 -  unfolding Basis_prod_def
1.223 -  by (subst card_Un_disjoint) (auto intro!: card_image arg_cong2[where f="op +"] inj_onI)
1.225 -end
1.227 -end