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.63 -  by (simp add: inner_setsum_left inner_Basis if_distrib comm_monoid_add_class.setsum.If_cases)
    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.102 -
   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.110 -
   1.111 -lemma DIM_positive: "0 < DIM('a::euclidean_space)"
   1.112 -  by (simp add: card_gt_0_iff)
   1.113 -
   1.114 -lemma DIM_ge_Suc0 [iff]: "Suc 0 \<le> card Basis"
   1.115 -  by (meson DIM_positive Suc_leI)
   1.116 -
   1.117 -
   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.121 -  by (simp add: comm_monoid_add_class.setsum.remove [OF finite_Basis assms]
   1.122 -         assms inner_not_same_Basis comm_monoid_add_class.setsum.neutral)
   1.123 -
   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.126 -  by (simp add: comm_monoid_add_class.setsum.remove [OF finite_Basis assms]
   1.127 -         assms inner_not_same_Basis comm_monoid_add_class.setsum.neutral)
   1.128 -
   1.129 -subsection \<open>Subclass relationships\<close>
   1.130 -
   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.149 -
   1.150 -subsection \<open>Class instances\<close>
   1.151 -
   1.152 -subsubsection \<open>Type @{typ real}\<close>
   1.153 -
   1.154 -instantiation real :: euclidean_space
   1.155 -begin
   1.156 -
   1.157 -definition 
   1.158 -  [simp]: "Basis = {1::real}"
   1.159 -
   1.160 -instance
   1.161 -  by standard auto
   1.162 -
   1.163 -end
   1.164 -
   1.165 -lemma DIM_real[simp]: "DIM(real) = 1"
   1.166 -  by simp
   1.167 -
   1.168 -subsubsection \<open>Type @{typ complex}\<close>
   1.169 -
   1.170 -instantiation complex :: euclidean_space
   1.171 -begin
   1.172 -
   1.173 -definition Basis_complex_def: "Basis = {1, \<i>}"
   1.174 -
   1.175 -instance
   1.176 -  by standard (auto simp add: Basis_complex_def intro: complex_eqI split: if_split_asm)
   1.177 -
   1.178 -end
   1.179 -
   1.180 -lemma DIM_complex[simp]: "DIM(complex) = 2"
   1.181 -  unfolding Basis_complex_def by simp
   1.182 -
   1.183 -subsubsection \<open>Type @{typ "'a \<times> 'b"}\<close>
   1.184 -
   1.185 -instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
   1.186 -begin
   1.187 -
   1.188 -definition
   1.189 -  "Basis = (\<lambda>u. (u, 0)) ` Basis \<union> (\<lambda>v. (0, v)) ` Basis"
   1.190 -
   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.201 -
   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.220 -
   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.224 -
   1.225 -end
   1.226 -
   1.227 -end