src/HOL/Analysis/Finite_Function_Topology.thy
 author paulson Thu Apr 11 15:26:04 2019 +0100 (6 months ago) changeset 70125 b601c2c87076 permissions -rw-r--r--
type instantiations for poly_mapping as a real_normed_vector
```     1 section\<open>Poly Mappings as a Real Normed Vector\<close>
```
```     2
```
```     3 (*  Author:  LC Paulson
```
```     4 *)
```
```     5
```
```     6 theory Finite_Function_Topology
```
```     7   imports Function_Topology  "HOL-Library.Poly_Mapping"
```
```     8
```
```     9 begin
```
```    10
```
```    11 instantiation "poly_mapping" :: (type, real_vector) real_vector
```
```    12 begin
```
```    13
```
```    14 definition scaleR_poly_mapping_def:
```
```    15   "scaleR r x \<equiv> Abs_poly_mapping (\<lambda>i. (scaleR r (Poly_Mapping.lookup x i)))"
```
```    16
```
```    17 instance
```
```    18 proof
```
```    19 qed (simp_all add: scaleR_poly_mapping_def plus_poly_mapping.abs_eq eq_onp_def lookup_add scaleR_add_left scaleR_add_right)
```
```    20
```
```    21 end
```
```    22
```
```    23 instantiation "poly_mapping" :: (type, real_normed_vector) metric_space
```
```    24 begin
```
```    25
```
```    26 definition dist_poly_mapping :: "['a \<Rightarrow>\<^sub>0 'b,'a \<Rightarrow>\<^sub>0 'b] \<Rightarrow> real"
```
```    27   where dist_poly_mapping_def:
```
```    28     "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))"
```
```    29
```
```    30 definition uniformity_poly_mapping:: "(('a \<Rightarrow>\<^sub>0 'b) \<times> ('a \<Rightarrow>\<^sub>0 'b)) filter"
```
```    31   where uniformity_poly_mapping_def:
```
```    32     "uniformity_poly_mapping \<equiv> INF e\<in>{0<..}. principal {(x, y). dist (x::'a\<Rightarrow>\<^sub>0'b) y < e}"
```
```    33
```
```    34 definition open_poly_mapping:: "('a \<Rightarrow>\<^sub>0 'b)set \<Rightarrow> bool"
```
```    35   where open_poly_mapping_def:
```
```    36     "open_poly_mapping U \<equiv> (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
```
```    37
```
```    38 instance
```
```    39 proof
```
```    40   show "uniformity = (INF e\<in>{0<..}. principal {(x, y::'a \<Rightarrow>\<^sub>0 'b). dist x y < e})"
```
```    41     by (simp add: uniformity_poly_mapping_def)
```
```    42 next
```
```    43   fix U :: "('a \<Rightarrow>\<^sub>0 'b) set"
```
```    44   show "open U = (\<forall>x\<in>U. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> U)"
```
```    45     by (simp add: open_poly_mapping_def)
```
```    46 next
```
```    47   fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b"
```
```    48   show "dist x y = 0 \<longleftrightarrow> x = y"
```
```    49   proof
```
```    50     assume "dist x y = 0"
```
```    51     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"
```
```    52       by (simp add: dist_poly_mapping_def)
```
```    53     then have "poly_mapping.lookup x n = poly_mapping.lookup y n"
```
```    54       if "n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y" for n
```
```    55       using that by (simp add: ordered_comm_monoid_add_class.sum_nonneg_eq_0_iff)
```
```    56     then show "x = y"
```
```    57       by (metis Un_iff in_keys_iff poly_mapping_eqI)
```
```    58   qed (simp add: dist_poly_mapping_def)
```
```    59 next
```
```    60   fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b" and z :: "'a \<Rightarrow>\<^sub>0 'b"
```
```    61   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))"
```
```    62     by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_left)
```
```    63   also have "... \<le> (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y \<union> Poly_Mapping.keys z.
```
```    64                      dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup z n) + dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
```
```    65     by (simp add: ordered_comm_monoid_add_class.sum_mono dist_triangle2)
```
```    66   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))
```
```    67                  + (\<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))"
```
```    68     by (simp add: sum.distrib)
```
```    69   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))
```
```    70                  + (\<Sum>n \<in> Poly_Mapping.keys y \<union> Poly_Mapping.keys z. dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
```
```    71     by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_right arg_cong2 [where f = "(+)"])
```
```    72   also have "... = dist x z + dist y z"
```
```    73     by (simp add: dist_poly_mapping_def)
```
```    74   finally show "dist x y \<le> dist x z + dist y z" .
```
```    75 qed
```
```    76
```
```    77 end
```
```    78
```
```    79 instantiation "poly_mapping" :: (type, real_normed_vector) real_normed_vector
```
```    80 begin
```
```    81
```
```    82 definition norm_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> real"
```
```    83   where norm_poly_mapping_def:
```
```    84     "norm_poly_mapping \<equiv> \<lambda>x. dist x 0"
```
```    85
```
```    86 definition sgn_poly_mapping :: "('a \<Rightarrow>\<^sub>0 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>0 'b)"
```
```    87   where sgn_poly_mapping_def:
```
```    88     "sgn_poly_mapping \<equiv> \<lambda>x. x /\<^sub>R norm x"
```
```    89
```
```    90 instance
```
```    91 proof
```
```    92   fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b"
```
```    93   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"
```
```    94     by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_left)
```
```    95   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))"
```
```    96     by (simp add: dist_poly_mapping_def)
```
```    97   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))"
```
```    98     by (simp add: dist_norm)
```
```    99   also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup (x-y) n))"
```
```   100     by (simp add: lookup_minus)
```
```   101   also have "... = (\<Sum>n \<in> Poly_Mapping.keys (x-y). norm (poly_mapping.lookup (x-y) n))"
```
```   102     by (simp add: "0" sum.mono_neutral_cong_right keys_diff)
```
```   103   also have "... = norm (x - y)"
```
```   104     by (simp add: norm_poly_mapping_def dist_poly_mapping_def)
```
```   105   finally show "dist x y = norm (x - y)" .
```
```   106 next
```
```   107   fix x :: "'a \<Rightarrow>\<^sub>0 'b"
```
```   108   show "sgn x = x /\<^sub>R norm x"
```
```   109     by (simp add: sgn_poly_mapping_def)
```
```   110 next
```
```   111   fix x :: "'a \<Rightarrow>\<^sub>0 'b"
```
```   112   show "norm x = 0 \<longleftrightarrow> x = 0"
```
```   113     by (simp add: norm_poly_mapping_def)
```
```   114 next
```
```   115   fix x :: "'a \<Rightarrow>\<^sub>0 'b" and y :: "'a \<Rightarrow>\<^sub>0 'b"
```
```   116   have "norm (x + y) = (\<Sum>n \<in> Poly_Mapping.keys (x + y). norm (poly_mapping.lookup x n + poly_mapping.lookup y n))"
```
```   117     by (simp add: norm_poly_mapping_def dist_poly_mapping_def lookup_add)
```
```   118   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))"
```
```   119     by (auto simp: simp add: plus_poly_mapping.rep_eq in_keys_iff intro: sum.mono_neutral_left)
```
```   120   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))"
```
```   121     by (simp add: norm_triangle_ineq sum_mono)
```
```   122   also have "... = (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup x n))
```
```   123                  + (\<Sum>n \<in> Poly_Mapping.keys x \<union> Poly_Mapping.keys y. norm (poly_mapping.lookup y n))"
```
```   124     by (simp add: sum.distrib)
```
```   125   also have "... = (\<Sum>n \<in> Poly_Mapping.keys x. norm (poly_mapping.lookup x n))
```
```   126                  + (\<Sum>n \<in> Poly_Mapping.keys y. norm (poly_mapping.lookup y n))"
```
```   127     by (force simp add: in_keys_iff intro: arg_cong2 [where f = "(+)"] sum.mono_neutral_right)
```
```   128   also have "... = norm x + norm y"
```
```   129     by (simp add: norm_poly_mapping_def dist_poly_mapping_def)
```
```   130   finally show "norm (x + y) \<le> norm x + norm y" .
```
```   131 next
```
```   132   fix a :: "real" and x :: "'a \<Rightarrow>\<^sub>0 'b"
```
```   133   show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
```
```   134   proof (cases "a = 0")
```
```   135     case False
```
```   136     then have [simp]: "Poly_Mapping.keys (a *\<^sub>R x) = Poly_Mapping.keys x"
```
```   137       by (auto simp add: scaleR_poly_mapping_def in_keys_iff)
```
```   138     then show ?thesis
```
```   139       by (simp add: norm_poly_mapping_def dist_poly_mapping_def scaleR_poly_mapping_def sum_distrib_left)
```
```   140   qed (simp add: norm_poly_mapping_def)
```
```   141 qed
```
```   142
```
```   143 end
```
```   144
```
```   145 end
```