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