Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Abstract_Limits.thy Sprache: Isabelle

Original von: Isabelle^©

theory Abstract_Limits
  imports
    Abstract_Topology
begin

subsection\<open>nhdsin and atin\<close>

definition nhdsin :: "'a topology \ 'a \ 'a filter"
  where "nhdsin X a =
           (if a \<in> topspace X then (INF S\<in>{S. openin X S \<and> a \<in> S}. principal S) else bot)"

definition atin :: "'a topology \ 'a \ 'a filter"
  where "atin X a \ inf (nhdsin X a) (principal (topspace X - {a}))"

lemma nhdsin_degenerate [simp]: "a \ topspace X \ nhdsin X a = bot"
  and atin_degenerate [simp]: "a \ topspace X \ atin X a = bot"
  by (simp_all add: nhdsin_def atin_def)

lemma eventually_nhdsin:
  "eventually P (nhdsin X a) \ a \ topspace X \ (\S. openin X S \ a \ S \ (\x\S. P x))"
proof (cases "a \ topspace X")
  case True
  hence "nhdsin X a = (INF S\{S. openin X S \ a \ S}. principal S)"
    by (simp add: nhdsin_def)
  also have "eventually P \ \ (\S. openin X S \ a \ S \ (\x\S. P x))"
    using True by (subst eventually_INF_base) (auto simp: eventually_principal)
  finally show ?thesis using True by simp
qed auto

lemma eventually_atin:
  "eventually P (atin X a) \ a \ topspace X \
             (\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
proof (cases "a \ topspace X")
  case True
  hence "eventually P (atin X a) \ (\S. openin X S \
           a \<in> S \<and> (\<forall>x\<in>S. x \<in> topspace X \<and> x \<noteq> a \<longrightarrow> P x))"
    by (simp add: atin_def eventually_inf_principal eventually_nhdsin)
  also have "\ \ (\U. openin X U \ a \ U \ (\x \ U - {a}. P x))"
    using openin_subset by (intro ex_cong) auto
  finally show ?thesis by (simp add: True)
qed auto

subsection\<open>Limits in a topological space\<close>

definition limitin :: "'a topology \ ('b \ 'a) \ 'a \ 'b filter \ bool" where
  "limitin X f l F \ l \ topspace X \ (\U. openin X U \ l \ U \ eventually (\x. f x \ U) F)"

lemma limitin_canonical_iff [simp]: "limitin euclidean f l F \ (f \ l) F"
  by (auto simp: limitin_def tendsto_def)

lemma limitin_topspace: "limitin X f l F \ l \ topspace X"
  by (simp add: limitin_def)

lemma limitin_const_iff [simp]: "limitin X (\a. l) l F \ l \ topspace X"
  by (simp add: limitin_def)

lemma limitin_const: "limitin euclidean (\a. l) l F"
  by simp

lemma limitin_eventually:
   "\l \ topspace X; eventually (\x. f x = l) F\ \ limitin X f l F"
  by (auto simp: limitin_def eventually_mono)

lemma limitin_subsequence:
   "\strict_mono r; limitin X f l sequentially\ \ limitin X (f \ r) l sequentially"
  unfolding limitin_def using eventually_subseq by fastforce

lemma limitin_subtopology:
  "limitin (subtopology X S) f l F
   \<longleftrightarrow> l \<in> S \<and> eventually (\<lambda>a. f a \<in> S) F \<and> limitin X f l F"  (is "?lhs = ?rhs")
proof (cases "l \ S \ topspace X")
  case True
  show ?thesis
  proof
    assume L: ?lhs
    with True
    have "\\<^sub>F b in F. f b \ topspace X \ S"
      by (metis (no_types) limitin_def openin_topspace topspace_subtopology)
    with L show ?rhs
      apply (clarsimp simp add: limitin_def eventually_mono openin_subtopology_alt)
      apply (drule_tac x="S \ U" in spec, force simp: elim: eventually_mono)
      done
  next
    assume ?rhs
    then show ?lhs
      using eventually_elim2
      by (fastforce simp add: limitin_def openin_subtopology_alt)
  qed
qed (auto simp: limitin_def)

lemma limitin_canonical_iff_gen [simp]:
  assumes "open S"
  shows "limitin (top_of_set S) f l F \ (f \ l) F \ l \ S"
  using assms by (auto simp: limitin_subtopology tendsto_def)

lemma limitin_sequentially:
   "limitin X S l sequentially \
     l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> (\<exists>N. \<forall>n. N \<le> n \<longrightarrow> S n \<in> U))"
  by (simp add: limitin_def eventually_sequentially)

lemma limitin_sequentially_offset:
   "limitin X f l sequentially \ limitin X (\i. f (i + k)) l sequentially"
  unfolding limitin_sequentially
  by (metis add.commute le_add2 order_trans)

lemma limitin_sequentially_offset_rev:
  assumes "limitin X (\i. f (i + k)) l sequentially"
  shows "limitin X f l sequentially"
proof -
  have "\N. \n\N. f n \ U" if U: "openin X U" "l \ U" for U
  proof -
    obtain N where "\n. n\N \ f (n + k) \ U"
      using assms U unfolding limitin_sequentially by blast
    then have "\n\N+k. f n \ U"
      by (metis add_leD2 le_add_diff_inverse ordered_cancel_comm_monoid_diff_class.le_diff_conv2 add.commute)
    then show ?thesis ..
  qed
  with assms show ?thesis
    unfolding limitin_sequentially
    by simp
qed

lemma limitin_atin:
   "limitin Y f y (atin X x) \
        y \<in> topspace Y \<and>
        (x \<in> topspace X
        \<longrightarrow> (\<forall>V. openin Y V \<and> y \<in> V
                 \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> f ` (U - {x}) \<subseteq> V)))"
  by (auto simp: limitin_def eventually_atin image_subset_iff)

lemma limitin_atin_self:
   "limitin Y f (f a) (atin X a) \
        f a \<in> topspace Y \<and>
        (a \<in> topspace X
         \<longrightarrow> (\<forall>V. openin Y V \<and> f a \<in> V
                  \<longrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> f ` U \<subseteq> V)))"
  unfolding limitin_atin by fastforce

lemma limitin_trivial:
   "\trivial_limit F; y \ topspace X\ \ limitin X f y F"
  by (simp add: limitin_def)

lemma limitin_transform_eventually:
   "\eventually (\x. f x = g x) F; limitin X f l F\ \ limitin X g l F"
  unfolding limitin_def using eventually_elim2 by fastforce

lemma continuous_map_limit:
  assumes "continuous_map X Y g" and f: "limitin X f l F"
  shows "limitin Y (g \ f) (g l) F"
proof -
  have "g l \ topspace Y"
    by (meson assms continuous_map_def limitin_topspace)
  moreover
  have "\U. \\V. openin X V \ l \ V \ (\\<^sub>F x in F. f x \ V); openin Y U; g l \ U\
            \<Longrightarrow> \<forall>\<^sub>F x in F. g (f x) \<in> U"
    using assms eventually_mono
    by (fastforce simp: limitin_def dest!: openin_continuous_map_preimage)
  ultimately show ?thesis
    using f by (fastforce simp add: limitin_def)
qed

subsection\<open>Pointwise continuity in topological spaces\<close>

definition topcontinuous_at where
  "topcontinuous_at X Y f x \
     x \<in> topspace X \<and>
     (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
     (\<forall>V. openin Y V \<and> f x \<in> V
          \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y \<in> U. f y \<in> V)))"

lemma topcontinuous_at_atin:
   "topcontinuous_at X Y f x \
        x \<in> topspace X \<and>
        (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
        limitin Y f (f x) (atin X x)"
  unfolding topcontinuous_at_def
  by (fastforce simp add: limitin_atin)+

lemma continuous_map_eq_topcontinuous_at:
   "continuous_map X Y f \ (\x \ topspace X. topcontinuous_at X Y f x)"
    (is "?lhs = ?rhs")
proof
  assume ?lhs
  then show ?rhs
    by (auto simp: continuous_map_def topcontinuous_at_def)
next
  assume R: ?rhs
  then show ?lhs
    apply (auto simp: continuous_map_def topcontinuous_at_def)
    apply (subst openin_subopen, safe)
    apply (drule bspec, assumption)
    using openin_subset[of X] apply (auto simp: subset_iff dest!: spec)
    done
qed

lemma continuous_map_atin:
   "continuous_map X Y f \ (\x \ topspace X. limitin Y f (f x) (atin X x))"
  by (auto simp: limitin_def topcontinuous_at_atin continuous_map_eq_topcontinuous_at)

lemma limitin_continuous_map:
   "\continuous_map X Y f; a \ topspace X; f a = b\ \ limitin Y f b (atin X a)"
  by (auto simp: continuous_map_atin)

subsection\<open>Combining theorems for continuous functions into the reals\<close>

lemma continuous_map_canonical_const [continuous_intros]:
   "continuous_map X euclidean (\x. c)"
  by simp

lemma continuous_map_real_mult [continuous_intros]:
   "\continuous_map X euclideanreal f; continuous_map X euclideanreal g\
   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x * g x)"
  by (simp add: continuous_map_atin tendsto_mult)

lemma continuous_map_real_pow [continuous_intros]:
   "continuous_map X euclideanreal f \ continuous_map X euclideanreal (\x. f x ^ n)"
  by (induction n) (auto simp: continuous_map_real_mult)

lemma continuous_map_real_mult_left:
   "continuous_map X euclideanreal f \ continuous_map X euclideanreal (\x. c * f x)"
  by (simp add: continuous_map_atin tendsto_mult)

lemma continuous_map_real_mult_left_eq:
   "continuous_map X euclideanreal (\x. c * f x) \ c = 0 \ continuous_map X euclideanreal f"
proof (cases "c = 0")
  case False
  have "continuous_map X euclideanreal (\x. c * f x) \ continuous_map X euclideanreal f"
    apply (frule continuous_map_real_mult_left [where c="inverse c"])
    apply (simp add: field_simps False)
    done
  with False show ?thesis
    using continuous_map_real_mult_left by blast
qed simp

lemma continuous_map_real_mult_right:
   "continuous_map X euclideanreal f \ continuous_map X euclideanreal (\x. f x * c)"
  by (simp add: continuous_map_atin tendsto_mult)

lemma continuous_map_real_mult_right_eq:
   "continuous_map X euclideanreal (\x. f x * c) \ c = 0 \ continuous_map X euclideanreal f"
  by (simp add: mult.commute flip: continuous_map_real_mult_left_eq)

lemma continuous_map_minus [continuous_intros]:
  fixes f :: "'a\'b::real_normed_vector"
  shows "continuous_map X euclidean f \ continuous_map X euclidean (\x. - f x)"
  by (simp add: continuous_map_atin tendsto_minus)

lemma continuous_map_minus_eq [simp]:
  fixes f :: "'a\'b::real_normed_vector"
  shows "continuous_map X euclidean (\x. - f x) \ continuous_map X euclidean f"
  using continuous_map_minus add.inverse_inverse continuous_map_eq by fastforce

lemma continuous_map_add [continuous_intros]:
  fixes f :: "'a\'b::real_normed_vector"
  shows "\continuous_map X euclidean f; continuous_map X euclidean g\ \ continuous_map X euclidean (\x. f x + g x)"
  by (simp add: continuous_map_atin tendsto_add)

lemma continuous_map_diff [continuous_intros]:
  fixes f :: "'a\'b::real_normed_vector"
  shows "\continuous_map X euclidean f; continuous_map X euclidean g\ \ continuous_map X euclidean (\x. f x - g x)"
  by (simp add: continuous_map_atin tendsto_diff)

lemma continuous_map_norm [continuous_intros]:
  fixes f :: "'a\'b::real_normed_vector"
  shows "continuous_map X euclidean f \ continuous_map X euclidean (\x. norm(f x))"
  by (simp add: continuous_map_atin tendsto_norm)

lemma continuous_map_real_abs [continuous_intros]:
   "continuous_map X euclideanreal f \ continuous_map X euclideanreal (\x. abs(f x))"
  by (simp add: continuous_map_atin tendsto_rabs)

lemma continuous_map_real_max [continuous_intros]:
   "\continuous_map X euclideanreal f; continuous_map X euclideanreal g\
   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. max (f x) (g x))"
  by (simp add: continuous_map_atin tendsto_max)

lemma continuous_map_real_min [continuous_intros]:
   "\continuous_map X euclideanreal f; continuous_map X euclideanreal g\
   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. min (f x) (g x))"
  by (simp add: continuous_map_atin tendsto_min)

lemma continuous_map_sum [continuous_intros]:
  fixes f :: "'a\'b\'c::real_normed_vector"
  shows "\finite I; \i. i \ I \ continuous_map X euclidean (\x. f x i)\
         \<Longrightarrow> continuous_map X euclidean (\<lambda>x. sum (f x) I)"
  by (simp add: continuous_map_atin tendsto_sum)

lemma continuous_map_prod [continuous_intros]:
   "\finite I;
         \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x i)\<rbrakk>
        \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. prod (f x) I)"
  by (simp add: continuous_map_atin tendsto_prod)

lemma continuous_map_real_inverse [continuous_intros]:
   "\continuous_map X euclideanreal f; \x. x \ topspace X \ f x \ 0\
        \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. inverse(f x))"
  by (simp add: continuous_map_atin tendsto_inverse)

lemma continuous_map_real_divide [continuous_intros]:
   "\continuous_map X euclideanreal f; continuous_map X euclideanreal g; \x. x \ topspace X \ g x \ 0\
   \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x / g x)"
  by (simp add: continuous_map_atin tendsto_divide)

end

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.