src/HOL/Analysis/Finite_Function_Topology.thy
changeset 70125 b601c2c87076
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Analysis/Finite_Function_Topology.thy	Thu Apr 11 15:26:04 2019 +0100
     1.3 @@ -0,0 +1,145 @@
     1.4 +section\<open>Poly Mappings as a Real Normed Vector\<close>
     1.5 +
     1.6 +(*  Author:  LC Paulson
     1.7 +*)
     1.8 +
     1.9 +theory Finite_Function_Topology
    1.10 +  imports Function_Topology  "HOL-Library.Poly_Mapping" 
    1.11 +           
    1.12 +begin
    1.13 +
    1.14 +instantiation "poly_mapping" :: (type, real_vector) real_vector
    1.15 +begin
    1.16 +
    1.17 +definition scaleR_poly_mapping_def:
    1.18 +  "scaleR r x \<equiv> Abs_poly_mapping (\<lambda>i. (scaleR r (Poly_Mapping.lookup x i)))"
    1.19 +
    1.20 +instance
    1.21 +proof 
    1.22 +qed (simp_all add: scaleR_poly_mapping_def plus_poly_mapping.abs_eq eq_onp_def lookup_add scaleR_add_left scaleR_add_right)
    1.23 +
    1.24 +end
    1.25 +
    1.26 +instantiation "poly_mapping" :: (type, real_normed_vector) metric_space
    1.27 +begin
    1.28 +
    1.29 +definition dist_poly_mapping :: "['a \<Rightarrow>\<^sub>0 'b,'a \<Rightarrow>\<^sub>0 'b] \<Rightarrow> real"
    1.30 +  where dist_poly_mapping_def:
    1.31 +    "dist_poly_mapping \<equiv> \<lambda>x y. (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup y n))"
    1.32 +
    1.33 +definition uniformity_poly_mapping:: "(('a \<Rightarrow>\<^sub>0 'b) \<times> ('a \<Rightarrow>\<^sub>0 'b)) filter"
    1.34 +  where uniformity_poly_mapping_def:
    1.35 +    "uniformity_poly_mapping \<equiv> INF e\<in>{0<..}. principal {(x, y). dist (x::'a\<Rightarrow>\<^sub>0'b) y < e}"
    1.36 +
    1.37 +definition open_poly_mapping:: "('a \<Rightarrow>\<^sub>0 'b)set \<Rightarrow> bool"
    1.38 +  where open_poly_mapping_def:
    1.39 +    "open_poly_mapping U \<equiv> (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
    1.40 +
    1.41 +instance
    1.42 +proof
    1.43 +  show "uniformity = (INF e\<in>{0<..}. principal {(x, y::'a \<Rightarrow>\<^sub>0 'b). dist x y < e})"
    1.44 +    by (simp add: uniformity_poly_mapping_def)
    1.45 +next
    1.46 +  fix U :: "('a \<Rightarrow>\<^sub>0 'b) set"
    1.47 +  show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
    1.48 +    by (simp add: open_poly_mapping_def)
    1.49 +next
    1.50 +  fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b"
    1.51 +  show "dist x y = 0 \<longleftrightarrow> x = y"
    1.52 +  proof
    1.53 +    assume "dist x y = 0"
    1.54 +    then have "(\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. dist (poly_mapping.lookup x n) (poly_mapping.lookup y n)) = 0"
    1.55 +      by (simp add: dist_poly_mapping_def)
    1.56 +    then have "poly_mapping.lookup x n = poly_mapping.lookup y n"
    1.57 +      if "n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y" for n
    1.58 +      using that by (simp add: ordered_comm_monoid_add_class.sum_nonneg_eq_0_iff)
    1.59 +    then show "x = y"
    1.60 +      by (metis Un_iff in_keys_iff poly_mapping_eqI)
    1.61 +  qed (simp add: dist_poly_mapping_def)
    1.62 +next
    1.63 +  fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b" and z :: "'a \<Rightarrow>\<^sub>0 'b"
    1.64 +  have "dist x y = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y \<union> Poly_Mapping.keys z. dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup y n))"
    1.65 +    by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_left)
    1.66 +  also have "... \<le> (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y \<union> Poly_Mapping.keys z. 
    1.67 +                     dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup z n) + dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
    1.68 +    by (simp add: ordered_comm_monoid_add_class.sum_mono dist_triangle2)
    1.69 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y \<union> Poly_Mapping.keys z. dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup z n))
    1.70 +                 + (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y \<union> Poly_Mapping.keys z. dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
    1.71 +    by (simp add: sum.distrib)
    1.72 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys z. dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup z n))
    1.73 +                 + (\<Sum>n \<in> Poly_Mapping.keys y \<union> Poly_Mapping.keys z. dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
    1.74 +    by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_right arg_cong2 [where f = "(+)"])
    1.75 +  also have "... = dist x z + dist y z"
    1.76 +    by (simp add: dist_poly_mapping_def)
    1.77 +  finally show "dist x y \<le> dist x z + dist y z" .
    1.78 +qed
    1.79 +
    1.80 +end
    1.81 +
    1.82 +instantiation "poly_mapping" :: (type, real_normed_vector) real_normed_vector
    1.83 +begin
    1.84 +
    1.85 +definition norm_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> real"
    1.86 +  where norm_poly_mapping_def:
    1.87 +    "norm_poly_mapping \<equiv> \<lambda>x. dist x 0"
    1.88 +
    1.89 +definition sgn_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b)"
    1.90 +  where sgn_poly_mapping_def:
    1.91 +    "sgn_poly_mapping \<equiv> \<lambda>x. x /\<^sub>R norm x"
    1.92 +
    1.93 +instance
    1.94 +proof 
    1.95 +  fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b"
    1.96 +  have 0: "\<forall>i\<in>Poly_Mapping.keys x \<union> Poly_Mapping.keys y - Poly_Mapping.keys (x - y). norm (poly_mapping.lookup (x - y) i) = 0"
    1.97 +    by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_left)
    1.98 +  have "dist x y = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. dist (poly_mapping.lookup x n) (poly_mapping.lookup y n))"
    1.99 +    by (simp add: dist_poly_mapping_def)  
   1.100 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup x n - poly_mapping.lookup y n))"
   1.101 +    by (simp add: dist_norm)
   1.102 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup (x-y) n))"
   1.103 +    by (simp add: lookup_minus)
   1.104 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys (x-y). norm (poly_mapping.lookup (x-y) n))"
   1.105 +    by (simp add: "0" sum.mono_neutral_cong_right keys_diff)
   1.106 +  also have "... = norm (x - y)"
   1.107 +    by (simp add: norm_poly_mapping_def dist_poly_mapping_def)  
   1.108 +  finally show "dist x y = norm (x - y)" .
   1.109 +next
   1.110 +  fix x :: "'a \<Rightarrow>\<^sub>0 'b"
   1.111 +  show "sgn x = x /\<^sub>R norm x"
   1.112 +    by (simp add: sgn_poly_mapping_def)
   1.113 +next
   1.114 +  fix x :: "'a \<Rightarrow>\<^sub>0 'b"
   1.115 +  show "norm x = 0 \<longleftrightarrow> x = 0"
   1.116 +    by (simp add: norm_poly_mapping_def)  
   1.117 +next
   1.118 +  fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b"
   1.119 +  have "norm (x + y) = (\<Sum>n \<in> Poly_Mapping.keys (x + y). norm (poly_mapping.lookup x n + poly_mapping.lookup y n))"
   1.120 +    by (simp add: norm_poly_mapping_def dist_poly_mapping_def lookup_add)
   1.121 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup x n + poly_mapping.lookup y n))"
   1.122 +    by (auto simp: simp add: plus_poly_mapping.rep_eq in_keys_iff intro: sum.mono_neutral_left)
   1.123 +  also have "... \<le> (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup x n) + norm (poly_mapping.lookup y n))"
   1.124 +    by (simp add: norm_triangle_ineq sum_mono)
   1.125 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup x n))
   1.126 +                 + (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup y n))"
   1.127 +    by (simp add: sum.distrib)
   1.128 +  also have "... = (\<Sum>n \<in> Poly_Mapping.keys x. norm (poly_mapping.lookup x n))
   1.129 +                 + (\<Sum>n \<in> Poly_Mapping.keys y. norm (poly_mapping.lookup y n))"
   1.130 +    by (force simp add: in_keys_iff intro: arg_cong2 [where f = "(+)"] sum.mono_neutral_right)
   1.131 +  also have "... = norm x + norm y"
   1.132 +    by (simp add: norm_poly_mapping_def dist_poly_mapping_def)
   1.133 +  finally show "norm (x + y) \<le> norm x + norm y" .
   1.134 +next
   1.135 +  fix a :: "real" and x :: "'a \<Rightarrow>\<^sub>0 'b"
   1.136 +  show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
   1.137 +  proof (cases "a = 0")
   1.138 +    case False
   1.139 +    then have [simp]: "Poly_Mapping.keys (a *\<^sub>R x) = Poly_Mapping.keys x"
   1.140 +      by (auto simp add: scaleR_poly_mapping_def in_keys_iff)
   1.141 +    then show ?thesis
   1.142 +      by (simp add: norm_poly_mapping_def dist_poly_mapping_def scaleR_poly_mapping_def sum_distrib_left)
   1.143 +  qed (simp add: norm_poly_mapping_def)
   1.144 +qed
   1.145 +
   1.146 +end
   1.147 +
   1.148 +end