src/HOL/Analysis/Euclidean_Space.thy
author wenzelm
Sun Sep 18 20:33:48 2016 +0200 (2016-09-18)
changeset 63915 bab633745c7f
parent 63627 6ddb43c6b711
child 63938 f6ce08859d4c
permissions -rw-r--r--
tuned proofs;
     1 (*  Title:      HOL/Analysis/Euclidean_Space.thy
     2     Author:     Johannes Hölzl, TU München
     3     Author:     Brian Huffman, Portland State University
     4 *)
     5 
     6 section \<open>Finite-Dimensional Inner Product Spaces\<close>
     7 
     8 theory Euclidean_Space
     9 imports
    10   L2_Norm
    11   "~~/src/HOL/Library/Inner_Product"
    12   "~~/src/HOL/Library/Product_Vector"
    13 begin
    14 
    15 subsection \<open>Type class of Euclidean spaces\<close>
    16 
    17 class euclidean_space = real_inner +
    18   fixes Basis :: "'a set"
    19   assumes nonempty_Basis [simp]: "Basis \<noteq> {}"
    20   assumes finite_Basis [simp]: "finite Basis"
    21   assumes inner_Basis:
    22     "\<lbrakk>u \<in> Basis; v \<in> Basis\<rbrakk> \<Longrightarrow> inner u v = (if u = v then 1 else 0)"
    23   assumes euclidean_all_zero_iff:
    24     "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
    25 
    26 syntax "_type_dimension" :: "type \<Rightarrow> nat"  ("(1DIM/(1'(_')))")
    27 translations "DIM('a)" \<rightharpoonup> "CONST card (CONST Basis :: 'a set)"
    28 typed_print_translation \<open>
    29   [(@{const_syntax card},
    30     fn ctxt => fn _ => fn [Const (@{const_syntax Basis}, Type (@{type_name set}, [T]))] =>
    31       Syntax.const @{syntax_const "_type_dimension"} $ Syntax_Phases.term_of_typ ctxt T)]
    32 \<close>
    33 
    34 lemma (in euclidean_space) norm_Basis[simp]: "u \<in> Basis \<Longrightarrow> norm u = 1"
    35   unfolding norm_eq_sqrt_inner by (simp add: inner_Basis)
    36 
    37 lemma (in euclidean_space) inner_same_Basis[simp]: "u \<in> Basis \<Longrightarrow> inner u u = 1"
    38   by (simp add: inner_Basis)
    39 
    40 lemma (in euclidean_space) inner_not_same_Basis: "u \<in> Basis \<Longrightarrow> v \<in> Basis \<Longrightarrow> u \<noteq> v \<Longrightarrow> inner u v = 0"
    41   by (simp add: inner_Basis)
    42 
    43 lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u"
    44   unfolding sgn_div_norm by (simp add: scaleR_one)
    45 
    46 lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis"
    47 proof
    48   assume "0 \<in> Basis" thus "False"
    49     using inner_Basis [of 0 0] by simp
    50 qed
    51 
    52 lemma (in euclidean_space) nonzero_Basis: "u \<in> Basis \<Longrightarrow> u \<noteq> 0"
    53   by clarsimp
    54 
    55 lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis"
    56   by (metis ex_in_conv nonempty_Basis someI_ex)
    57 
    58 lemma (in euclidean_space) inner_setsum_left_Basis[simp]:
    59     "b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b"
    60   by (simp add: inner_setsum_left inner_Basis if_distrib comm_monoid_add_class.setsum.If_cases)
    61 
    62 lemma (in euclidean_space) euclidean_eqI:
    63   assumes b: "\<And>b. b \<in> Basis \<Longrightarrow> inner x b = inner y b" shows "x = y"
    64 proof -
    65   from b have "\<forall>b\<in>Basis. inner (x - y) b = 0"
    66     by (simp add: inner_diff_left)
    67   then show "x = y"
    68     by (simp add: euclidean_all_zero_iff)
    69 qed
    70 
    71 lemma (in euclidean_space) euclidean_eq_iff:
    72   "x = y \<longleftrightarrow> (\<forall>b\<in>Basis. inner x b = inner y b)"
    73   by (auto intro: euclidean_eqI)
    74 
    75 lemma (in euclidean_space) euclidean_representation_setsum:
    76   "(\<Sum>i\<in>Basis. f i *\<^sub>R i) = b \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
    77   by (subst euclidean_eq_iff) simp
    78 
    79 lemma (in euclidean_space) euclidean_representation_setsum':
    80   "b = (\<Sum>i\<in>Basis. f i *\<^sub>R i) \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
    81   by (auto simp add: euclidean_representation_setsum[symmetric])
    82 
    83 lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
    84   unfolding euclidean_representation_setsum by simp
    85 
    86 lemma (in euclidean_space) choice_Basis_iff:
    87   fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
    88   shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))"
    89   unfolding bchoice_iff
    90 proof safe
    91   fix f assume "\<forall>i\<in>Basis. P i (f i)"
    92   then show "\<exists>x. \<forall>i\<in>Basis. P i (inner x i)"
    93     by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"])
    94 qed auto
    95 
    96 lemma (in euclidean_space) euclidean_representation_setsum_fun:
    97     "(\<lambda>x. \<Sum>b\<in>Basis. inner (f x) b *\<^sub>R b) = f"
    98   by (rule ext) (simp add: euclidean_representation_setsum)
    99 
   100 lemma euclidean_isCont:
   101   assumes "\<And>b. b \<in> Basis \<Longrightarrow> isCont (\<lambda>x. (inner (f x) b) *\<^sub>R b) x"
   102     shows "isCont f x"
   103   apply (subst euclidean_representation_setsum_fun [symmetric])
   104   apply (rule isCont_setsum)
   105   apply (blast intro: assms)
   106   done
   107 
   108 lemma DIM_positive: "0 < DIM('a::euclidean_space)"
   109   by (simp add: card_gt_0_iff)
   110 
   111 lemma DIM_ge_Suc0 [iff]: "Suc 0 \<le> card Basis"
   112   by (meson DIM_positive Suc_leI)
   113 
   114 
   115 lemma setsum_inner_Basis_scaleR [simp]:
   116   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_vector"
   117   assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) *\<^sub>R f i) = f b"
   118   by (simp add: comm_monoid_add_class.setsum.remove [OF finite_Basis assms]
   119          assms inner_not_same_Basis comm_monoid_add_class.setsum.neutral)
   120 
   121 lemma setsum_inner_Basis_eq [simp]:
   122   assumes "b \<in> Basis" shows "(\<Sum>i\<in>Basis. (inner i b) * f i) = f b"
   123   by (simp add: comm_monoid_add_class.setsum.remove [OF finite_Basis assms]
   124          assms inner_not_same_Basis comm_monoid_add_class.setsum.neutral)
   125 
   126 subsection \<open>Subclass relationships\<close>
   127 
   128 instance euclidean_space \<subseteq> perfect_space
   129 proof
   130   fix x :: 'a show "\<not> open {x}"
   131   proof
   132     assume "open {x}"
   133     then obtain e where "0 < e" and e: "\<forall>y. dist y x < e \<longrightarrow> y = x"
   134       unfolding open_dist by fast
   135     define y where "y = x + scaleR (e/2) (SOME b. b \<in> Basis)"
   136     have [simp]: "(SOME b. b \<in> Basis) \<in> Basis"
   137       by (rule someI_ex) (auto simp: ex_in_conv)
   138     from \<open>0 < e\<close> have "y \<noteq> x"
   139       unfolding y_def by (auto intro!: nonzero_Basis)
   140     from \<open>0 < e\<close> have "dist y x < e"
   141       unfolding y_def by (simp add: dist_norm)
   142     from \<open>y \<noteq> x\<close> and \<open>dist y x < e\<close> show "False"
   143       using e by simp
   144   qed
   145 qed
   146 
   147 subsection \<open>Class instances\<close>
   148 
   149 subsubsection \<open>Type @{typ real}\<close>
   150 
   151 instantiation real :: euclidean_space
   152 begin
   153 
   154 definition
   155   [simp]: "Basis = {1::real}"
   156 
   157 instance
   158   by standard auto
   159 
   160 end
   161 
   162 lemma DIM_real[simp]: "DIM(real) = 1"
   163   by simp
   164 
   165 subsubsection \<open>Type @{typ complex}\<close>
   166 
   167 instantiation complex :: euclidean_space
   168 begin
   169 
   170 definition Basis_complex_def: "Basis = {1, \<i>}"
   171 
   172 instance
   173   by standard (auto simp add: Basis_complex_def intro: complex_eqI split: if_split_asm)
   174 
   175 end
   176 
   177 lemma DIM_complex[simp]: "DIM(complex) = 2"
   178   unfolding Basis_complex_def by simp
   179 
   180 subsubsection \<open>Type @{typ "'a \<times> 'b"}\<close>
   181 
   182 instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
   183 begin
   184 
   185 definition
   186   "Basis = (\<lambda>u. (u, 0)) ` Basis \<union> (\<lambda>v. (0, v)) ` Basis"
   187 
   188 lemma setsum_Basis_prod_eq:
   189   fixes f::"('a*'b)\<Rightarrow>('a*'b)"
   190   shows "setsum f Basis = setsum (\<lambda>i. f (i, 0)) Basis + setsum (\<lambda>i. f (0, i)) Basis"
   191 proof -
   192   have "inj_on (\<lambda>u. (u::'a, 0::'b)) Basis" "inj_on (\<lambda>u. (0::'a, u::'b)) Basis"
   193     by (auto intro!: inj_onI Pair_inject)
   194   thus ?thesis
   195     unfolding Basis_prod_def
   196     by (subst setsum.union_disjoint) (auto simp: Basis_prod_def setsum.reindex)
   197 qed
   198 
   199 instance proof
   200   show "(Basis :: ('a \<times> 'b) set) \<noteq> {}"
   201     unfolding Basis_prod_def by simp
   202 next
   203   show "finite (Basis :: ('a \<times> 'b) set)"
   204     unfolding Basis_prod_def by simp
   205 next
   206   fix u v :: "'a \<times> 'b"
   207   assume "u \<in> Basis" and "v \<in> Basis"
   208   thus "inner u v = (if u = v then 1 else 0)"
   209     unfolding Basis_prod_def inner_prod_def
   210     by (auto simp add: inner_Basis split: if_split_asm)
   211 next
   212   fix x :: "'a \<times> 'b"
   213   show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
   214     unfolding Basis_prod_def ball_Un ball_simps
   215     by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff)
   216 qed
   217 
   218 lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('a) + DIM('b)"
   219   unfolding Basis_prod_def
   220   by (subst card_Un_disjoint) (auto intro!: card_image arg_cong2[where f="op +"] inj_onI)
   221 
   222 end
   223 
   224 end