Theory Finite_Function_Topology

section‹Poly Mappings as a Real Normed Vector›

(*  Author:  LC Paulson
*)

theory Finite_Function_Topology
  imports Function_Topology  "HOL-Library.Poly_Mapping" 
           
begin

instantiation "poly_mapping" :: (type, real_vector) real_vector
begin

definition scaleR_poly_mapping_def:
  "scaleR r x ≡ Abs_poly_mapping (λi. (scaleR r (Poly_Mapping.lookup x i)))"

instance
proof 
qed (simp_all add: scaleR_poly_mapping_def plus_poly_mapping.abs_eq eq_onp_def lookup_add scaleR_add_left scaleR_add_right)

end

instantiation "poly_mapping" :: (type, real_normed_vector) metric_space
begin

definition dist_poly_mapping :: "['a ⇒⇩0 'b,'a ⇒⇩0 'b] ⇒ real"
  where dist_poly_mapping_def:
    "dist_poly_mapping ≡ λx y. (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y. dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup y n))"

definition uniformity_poly_mapping:: "(('a ⇒⇩0 'b) × ('a ⇒⇩0 'b)) filter"
  where uniformity_poly_mapping_def:
    "uniformity_poly_mapping ≡ INF e∈{0<..}. principal {(x, y). dist (x::'a⇒⇩0'b) y < e}"

definition open_poly_mapping:: "('a ⇒⇩0 'b)set ⇒ bool"
  where open_poly_mapping_def:
    "open_poly_mapping U ≡ (∀x∈U. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ U)"

instance
proof
  show "uniformity = (INF e∈{0<..}. principal {(x, y::'a ⇒⇩0 'b). dist x y < e})"
    by (simp add: uniformity_poly_mapping_def)
next
  fix U :: "('a ⇒⇩0 'b) set"
  show "open U = (∀x∈U. ∀⇩F (x', y) in uniformity. x' = x ⟶ y ∈ U)"
    by (simp add: open_poly_mapping_def)
next
  fix x :: "'a ⇒⇩0 'b" and y :: "'a ⇒⇩0 'b"
  show "dist x y = 0 ⟷ x = y"
  proof
    assume "dist x y = 0"
    then have "(∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y. dist (poly_mapping.lookup x n) (poly_mapping.lookup y n)) = 0"
      by (simp add: dist_poly_mapping_def)
    then have "poly_mapping.lookup x n = poly_mapping.lookup y n"
      if "n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y" for n
      using that by (simp add: ordered_comm_monoid_add_class.sum_nonneg_eq_0_iff)
    then show "x = y"
      by (metis Un_iff in_keys_iff poly_mapping_eqI)
  qed (simp add: dist_poly_mapping_def)
next
  fix x :: "'a ⇒⇩0 'b" and y :: "'a ⇒⇩0 'b" and z :: "'a ⇒⇩0 'b"
  have "dist x y = (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y ∪ Poly_Mapping.keys z. dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup y n))"
    by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_left)
  also have "... ≤ (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y ∪ Poly_Mapping.keys z. 
                     dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup z n) + dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
    by (simp add: ordered_comm_monoid_add_class.sum_mono dist_triangle2)
  also have "... = (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y ∪ Poly_Mapping.keys z. dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup z n))
                 + (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y ∪ Poly_Mapping.keys z. dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
    by (simp add: sum.distrib)
  also have "... = (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys z. dist (Poly_Mapping.lookup x n) (Poly_Mapping.lookup z n))
                 + (∑n ∈ Poly_Mapping.keys y ∪ Poly_Mapping.keys z. dist (Poly_Mapping.lookup y n) (Poly_Mapping.lookup z n))"
    by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_right arg_cong2 [where f = "(+)"])
  also have "... = dist x z + dist y z"
    by (simp add: dist_poly_mapping_def)
  finally show "dist x y ≤ dist x z + dist y z" .
qed

end

instantiation "poly_mapping" :: (type, real_normed_vector) real_normed_vector
begin

definition norm_poly_mapping :: "('a ⇒⇩0 'b) ⇒ real"
  where norm_poly_mapping_def:
    "norm_poly_mapping ≡ λx. dist x 0"

definition sgn_poly_mapping :: "('a ⇒⇩0 'b) ⇒ ('a ⇒⇩0 'b)"
  where sgn_poly_mapping_def:
    "sgn_poly_mapping ≡ λx. x /⇩R norm x"

instance
proof 
  fix x :: "'a ⇒⇩0 'b" and y :: "'a ⇒⇩0 'b"
  have 0: "∀i∈Poly_Mapping.keys x ∪ Poly_Mapping.keys y - Poly_Mapping.keys (x - y). norm (poly_mapping.lookup (x - y) i) = 0"
    by (force simp add: dist_poly_mapping_def in_keys_iff intro: sum.mono_neutral_left)
  have "dist x y = (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y. dist (poly_mapping.lookup x n) (poly_mapping.lookup y n))"
    by (simp add: dist_poly_mapping_def)  
  also have "... = (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y. norm (poly_mapping.lookup x n - poly_mapping.lookup y n))"
    by (simp add: dist_norm)
  also have "... = (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y. norm (poly_mapping.lookup (x-y) n))"
    by (simp add: lookup_minus)
  also have "... = (∑n ∈ Poly_Mapping.keys (x-y). norm (poly_mapping.lookup (x-y) n))"
    by (simp add: "0" sum.mono_neutral_cong_right keys_diff)
  also have "... = norm (x - y)"
    by (simp add: norm_poly_mapping_def dist_poly_mapping_def)  
  finally show "dist x y = norm (x - y)" .
next
  fix x :: "'a ⇒⇩0 'b"
  show "sgn x = x /⇩R norm x"
    by (simp add: sgn_poly_mapping_def)
next
  fix x :: "'a ⇒⇩0 'b"
  show "norm x = 0 ⟷ x = 0"
    by (simp add: norm_poly_mapping_def)  
next
  fix x :: "'a ⇒⇩0 'b" and y :: "'a ⇒⇩0 'b"
  have "norm (x + y) = (∑n ∈ Poly_Mapping.keys (x + y). norm (poly_mapping.lookup x n + poly_mapping.lookup y n))"
    by (simp add: norm_poly_mapping_def dist_poly_mapping_def lookup_add)
  also have "... = (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y. norm (poly_mapping.lookup x n + poly_mapping.lookup y n))"
    by (auto simp: simp add: plus_poly_mapping.rep_eq in_keys_iff intro: sum.mono_neutral_left)
  also have "... ≤ (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y. norm (poly_mapping.lookup x n) + norm (poly_mapping.lookup y n))"
    by (simp add: norm_triangle_ineq sum_mono)
  also have "... = (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y. norm (poly_mapping.lookup x n))
                 + (∑n ∈ Poly_Mapping.keys x ∪ Poly_Mapping.keys y. norm (poly_mapping.lookup y n))"
    by (simp add: sum.distrib)
  also have "... = (∑n ∈ Poly_Mapping.keys x. norm (poly_mapping.lookup x n))
                 + (∑n ∈ Poly_Mapping.keys y. norm (poly_mapping.lookup y n))"
    by (force simp add: in_keys_iff intro: arg_cong2 [where f = "(+)"] sum.mono_neutral_right)
  also have "... = norm x + norm y"
    by (simp add: norm_poly_mapping_def dist_poly_mapping_def)
  finally show "norm (x + y) ≤ norm x + norm y" .
next
  fix a :: "real" and x :: "'a ⇒⇩0 'b"
  show "norm (a *⇩R x) = ¦a¦ * norm x"
  proof (cases "a = 0")
    case False
    then have [simp]: "Poly_Mapping.keys (a *⇩R x) = Poly_Mapping.keys x"
      by (auto simp add: scaleR_poly_mapping_def in_keys_iff)
    then show ?thesis
      by (simp add: norm_poly_mapping_def dist_poly_mapping_def scaleR_poly_mapping_def sum_distrib_left)
  qed (simp add: norm_poly_mapping_def)
qed

end

end