SSL Finite_Function_Topology.thy Sprache: Isabelle

section\<open>Poly Mappings as a Real Normed Vector\<close>

(*  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 \\<^sub>0 'b,'a \\<^sub>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 \\<^sub>0 'b) \ ('a \\<^sub>0 'b)) filter"
  where uniformity_poly_mapping_def:
    "uniformity_poly_mapping \ INF e\{0<..}. principal {(x, y). dist (x::'a\\<^sub>0'b) y < e}"

definition open_poly_mapping:: "('a \\<^sub>0 'b)set \ bool"
  where open_poly_mapping_def:
    "open_poly_mapping U \ (\x\U. \\<^sub>F (x', y) in uniformity. x' = x \ y \ U)"

instance
proof
  show "uniformity = (INF e\{0<..}. principal {(x, y::'a \\<^sub>0 'b). dist x y < e})"
    by (simp add: uniformity_poly_mapping_def)
next
  fix U :: "('a \\<^sub>0 'b) set"
  show "open U = (\x\U. \\<^sub>F (x', y) in uniformity. x' = x \ y \ U)"
    by (simp add: open_poly_mapping_def)
next
  fix x :: "'a \\<^sub>0 'b" and y :: "'a \\<^sub>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 \\<^sub>0 'b" and y :: "'a \\<^sub>0 'b" and z :: "'a \\<^sub>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))
                 + (\<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))"
    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))
                 + (\<Sum>n \<in> Poly_Mapping.keys y \<union> 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 \\<^sub>0 'b) \ real"
  where norm_poly_mapping_def:
    "norm_poly_mapping \ \x. dist x 0"

definition sgn_poly_mapping :: "('a \\<^sub>0 'b) \ ('a \\<^sub>0 'b)"
  where sgn_poly_mapping_def:
    "sgn_poly_mapping \ \x. x /\<^sub>R norm x"

instance
proof
  fix x :: "'a \\<^sub>0 'b" and y :: "'a \\<^sub>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 \\<^sub>0 'b"
  show "sgn x = x /\<^sub>R norm x"
    by (simp add: sgn_poly_mapping_def)
next
  fix x :: "'a \\<^sub>0 'b"
  show "norm x = 0 \ x = 0"
    by (simp add: norm_poly_mapping_def)
next
  fix x :: "'a \\<^sub>0 'b" and y :: "'a \\<^sub>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))
                 + (\<Sum>n \<in> Poly_Mapping.keys x \<union> 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))
                 + (\<Sum>n \<in> 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 \\<^sub>0 'b"
  show "norm (a *\<^sub>R x) = \a\ * norm x"
  proof (cases "a = 0")
    case False
    then have [simp]: "Poly_Mapping.keys (a *\<^sub>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

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.