Quelle Abstract_Limits.thy Sprache: 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_within :: "['a topology, 'a, 'a set] \ 'a filter"
  where "atin_within X a S = inf (nhdsin X a) (principal (topspace X \ S - {a}))"

abbreviation atin :: "'a topology \ 'a \ 'a filter"
  where "atin X a \ atin_within X a UNIV"

lemma atin_def: "atin X a = inf (nhdsin X a) (principal (topspace X - {a}))"
  by (simp add: atin_within_def)

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_within:
  "eventually P (atin_within X a S) \ a \ topspace X \ (\T. openin X T \ a \ T \ (\x\T. x \ S \ x \ a \ P x))"
proof (cases "a \ topspace X")
  case True
  hence "eventually P (atin_within X a S) \
         (\<exists>T. openin X T \<and> a \<in> T \<and>
          (\<forall>x\<in>T. x \<in> topspace X \<and> x \<in> S \<and> x \<noteq> a \<longrightarrow> P x))"
    by (simp add: atin_within_def eventually_inf_principal eventually_nhdsin)
  also have "\ \ (\T. openin X T \ a \ T \ (\x\T. x \ S \ x \ a \ P x))"
    using openin_subset by (intro ex_cong) auto
  finally show ?thesis by (simp add: True)
qed (simp add: atin_within_def)

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))"
  by (auto simp add: eventually_atin_within)

lemma nontrivial_limit_atin:
   "atin X a \ bot \ a \ X derived_set_of topspace X"
proof
  assume L: "atin X a \ bot"
  then have "a \ topspace X"
    by (meson atin_degenerate)
  moreover have "\ openin X {a}"
    using L by (auto simp: eventually_atin trivial_limit_eq)
  ultimately
  show "a \ X derived_set_of topspace X"
    by (auto simp: derived_set_of_topspace)
next
  assume a: "a \ X derived_set_of topspace X"
  show "atin X a \ bot"
  proof
    assume "atin X a = bot"
    then have "eventually (\_. False) (atin X a)"
      by simp
    then show False
      by (metis a eventually_atin in_derived_set_of insertE insert_Diff)
  qed
qed

lemma eventually_atin_subtopology:
  assumes "a \ topspace X"
  shows "eventually P (atin (subtopology X S) a) \
    (a \<in> S \<longrightarrow> (\<exists>U. openin (subtopology X S) U \<and> a \<in> U \<and> (\<forall>x\<in>U - {a}. P x)))"
  using assms by (simp add: eventually_atin)

lemma eventually_within_imp:
   "eventually P (atin_within X a S) \ eventually (\x. x \ S \ P x) (atin X a)"
  by (auto simp add: eventually_atin_within eventually_atin)

lemma atin_subtopology_within:
  assumes "a \ S"
  shows "atin (subtopology X S) a = atin_within X a S"
proof -
  have "eventually P (atin (subtopology X S) a) \ eventually P (atin_within X a S)" for P
    unfolding eventually_atin eventually_atin_within openin_subtopology
    using assms by auto
  then show ?thesis
    by (meson le_filter_def order.eq_iff)
qed

lemma atin_subtopology_within_if:
  shows "atin (subtopology X S) a = (if a \ S then atin_within X a S else bot)"
  by (simp add: atin_subtopology_within)

lemma trivial_limit_atpointof_within:
   "trivial_limit(atin_within X a S) \
        (a \<notin> X derived_set_of S)"
  by (auto simp: trivial_limit_def eventually_atin_within in_derived_set_of)

lemma derived_set_of_trivial_limit:
   "a \ X derived_set_of S \ \ trivial_limit(atin_within X a S)"
  by (simp add: trivial_limit_atpointof_within)

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 limit_within_subset:
   "\limitin X f l (atin_within Y a S); T \ S\ \ limitin X f l (atin_within Y a T)"
  by (smt (verit) eventually_atin_within limitin_def subset_eq)

lemma limitinD: "\limitin X f l F; openin X U; l \ U\ \ eventually (\x. f x \ U) F"
  by (simp add: limitin_def)

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)
    moreover have "\U. \openin X U; l \ U\ \ \\<^sub>F x in F. f x \ S \ U"
      using limitinD [OF L] True openin_subtopology_Int2 by force
    ultimately show ?rhs
      using True by (auto simp: limitin_def eventually_conj_iff)
  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 add_le_imp_le_diff le_add_diff_inverse2)
    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 f image_eqI in_mono limitin_def)
  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>
     f \<in> topspace X \<rightarrow> 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>
        f \<in> topspace X \<rightarrow> 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
    unfolding continuous_map_def topcontinuous_at_def Pi_iff
    by (smt (verit, ccfv_threshold)  mem_Collect_eq openin_subopen openin_subset subset_eq)
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)

lemma limit_continuous_map_within:
   "\continuous_map (subtopology X S) Y f; a \ S; a \ topspace X\
    \<Longrightarrow> limitin Y f (f a) (atin_within X a S)"
  by (metis Int_iff atin_subtopology_within continuous_map_atin topspace_subtopology)

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
  { assume "continuous_map X euclideanreal (\x. c * f x)"
    then have "continuous_map X euclideanreal (\x. inverse c * (c * f x))"
      by (simp add: continuous_map_real_mult)
    then have "continuous_map X euclideanreal f"
      by (simp add: field_simps False) }
  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

quality96%

¤ Dauer der Verarbeitung: 0.18 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.