src/HOL/Analysis/Abstract_Limits.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (2 months ago) changeset 69981 3dced198b9ec parent 69875 03bc14eab432 child 70019 095dce9892e8 permissions -rw-r--r--
more strict AFP properties;
```     1 theory Abstract_Limits
```
```     2   imports
```
```     3     Abstract_Topology
```
```     4 begin
```
```     5
```
```     6 subsection\<open>nhdsin and atin\<close>
```
```     7
```
```     8 definition nhdsin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
```
```     9   where "nhdsin X a =
```
```    10            (if a \<in> topspace X then (INF S:{S. openin X S \<and> a \<in> S}. principal S) else bot)"
```
```    11
```
```    12 definition atin :: "'a topology \<Rightarrow> 'a \<Rightarrow> 'a filter"
```
```    13   where "atin X a \<equiv> inf (nhdsin X a) (principal (topspace X - {a}))"
```
```    14
```
```    15
```
```    16 lemma nhdsin_degenerate [simp]: "a \<notin> topspace X \<Longrightarrow> nhdsin X a = bot"
```
```    17   and atin_degenerate [simp]: "a \<notin> topspace X \<Longrightarrow> atin X a = bot"
```
```    18   by (simp_all add: nhdsin_def atin_def)
```
```    19
```
```    20 lemma eventually_nhdsin:
```
```    21   "eventually P (nhdsin X a) \<longleftrightarrow> a \<notin> topspace X \<or> (\<exists>S. openin X S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
```
```    22 proof (cases "a \<in> topspace X")
```
```    23   case True
```
```    24   hence "nhdsin X a = (INF S:{S. openin X S \<and> a \<in> S}. principal S)"
```
```    25     by (simp add: nhdsin_def)
```
```    26   also have "eventually P \<dots> \<longleftrightarrow> (\<exists>S. openin X S \<and> a \<in> S \<and> (\<forall>x\<in>S. P x))"
```
```    27     using True by (subst eventually_INF_base) (auto simp: eventually_principal)
```
```    28   finally show ?thesis using True by simp
```
```    29 qed auto
```
```    30
```
```    31 lemma eventually_atin:
```
```    32   "eventually P (atin X a) \<longleftrightarrow> a \<notin> topspace X \<or>
```
```    33              (\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
```
```    34 proof (cases "a \<in> topspace X")
```
```    35   case True
```
```    36   hence "eventually P (atin X a) \<longleftrightarrow> (\<exists>S. openin X S \<and>
```
```    37            a \<in> S \<and> (\<forall>x\<in>S. x \<in> topspace X \<and> x \<noteq> a \<longrightarrow> P x))"
```
```    38     by (simp add: atin_def eventually_inf_principal eventually_nhdsin)
```
```    39   also have "\<dots> \<longleftrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> (\<forall>x \<in> U - {a}. P x))"
```
```    40     using openin_subset by (intro ex_cong) auto
```
```    41   finally show ?thesis by (simp add: True)
```
```    42 qed auto
```
```    43
```
```    44
```
```    45 subsection\<open>Limits in a topological space\<close>
```
```    46
```
```    47 definition limitin :: "'a topology \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'b filter \<Rightarrow> bool" where
```
```    48   "limitin X f l F \<equiv> l \<in> topspace X \<and> (\<forall>U. openin X U \<and> l \<in> U \<longrightarrow> eventually (\<lambda>x. f x \<in> U) F)"
```
```    49
```
```    50 lemma limitin_euclideanreal_iff [simp]: "limitin euclideanreal f l F \<longleftrightarrow> (f \<longlongrightarrow> l) F"
```
```    51   by (auto simp: limitin_def tendsto_def)
```
```    52
```
```    53 lemma limitin_topspace: "limitin X f l F \<Longrightarrow> l \<in> topspace X"
```
```    54   by (simp add: limitin_def)
```
```    55
```
```    56 lemma limitin_const: "limitin X (\<lambda>a. l) l F \<longleftrightarrow> l \<in> topspace X"
```
```    57   by (simp add: limitin_def)
```
```    58
```
```    59 lemma limitin_real_const: "limitin euclideanreal (\<lambda>a. l) l F"
```
```    60   by (simp add: limitin_def)
```
```    61
```
```    62 lemma limitin_eventually:
```
```    63    "\<lbrakk>l \<in> topspace X; eventually (\<lambda>x. f x = l) F\<rbrakk> \<Longrightarrow> limitin X f l F"
```
```    64   by (auto simp: limitin_def eventually_mono)
```
```    65
```
```    66 lemma limitin_subsequence:
```
```    67    "\<lbrakk>strict_mono r; limitin X f l sequentially\<rbrakk> \<Longrightarrow> limitin X (f \<circ> r) l sequentially"
```
```    68   unfolding limitin_def using eventually_subseq by fastforce
```
```    69
```
```    70 lemma limitin_subtopology:
```
```    71   "limitin (subtopology X S) f l F
```
```    72    \<longleftrightarrow> l \<in> S \<and> eventually (\<lambda>a. f a \<in> S) F \<and> limitin X f l F"  (is "?lhs = ?rhs")
```
```    73 proof (cases "l \<in> S \<inter> topspace X")
```
```    74   case True
```
```    75   show ?thesis
```
```    76   proof
```
```    77     assume L: ?lhs
```
```    78     with True
```
```    79     have "\<forall>\<^sub>F b in F. f b \<in> topspace X \<inter> S"
```
```    80       by (metis (no_types) limitin_def openin_topspace topspace_subtopology)
```
```    81     with L show ?rhs
```
```    82       apply (clarsimp simp add: limitin_def eventually_mono topspace_subtopology openin_subtopology_alt)
```
```    83       apply (drule_tac x="S \<inter> U" in spec, force simp: elim: eventually_mono)
```
```    84       done
```
```    85   next
```
```    86     assume ?rhs
```
```    87     then show ?lhs
```
```    88       using eventually_elim2
```
```    89       by (fastforce simp add: limitin_def topspace_subtopology openin_subtopology_alt)
```
```    90   qed
```
```    91 qed (auto simp: limitin_def topspace_subtopology)
```
```    92
```
```    93
```
```    94 lemma limitin_sequentially:
```
```    95    "limitin X S l sequentially \<longleftrightarrow>
```
```    96      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))"
```
```    97   by (simp add: limitin_def eventually_sequentially)
```
```    98
```
```    99 lemma limitin_sequentially_offset:
```
```   100    "limitin X f l sequentially \<Longrightarrow> limitin X (\<lambda>i. f (i + k)) l sequentially"
```
```   101   unfolding limitin_sequentially
```
```   102   by (metis add.commute le_add2 order_trans)
```
```   103
```
```   104 lemma limitin_sequentially_offset_rev:
```
```   105   assumes "limitin X (\<lambda>i. f (i + k)) l sequentially"
```
```   106   shows "limitin X f l sequentially"
```
```   107 proof -
```
```   108   have "\<exists>N. \<forall>n\<ge>N. f n \<in> U" if U: "openin X U" "l \<in> U" for U
```
```   109   proof -
```
```   110     obtain N where "\<And>n. n\<ge>N \<Longrightarrow> f (n + k) \<in> U"
```
```   111       using assms U unfolding limitin_sequentially by blast
```
```   112     then have "\<forall>n\<ge>N+k. f n \<in> U"
```
```   113       by (metis add_leD2 le_add_diff_inverse ordered_cancel_comm_monoid_diff_class.le_diff_conv2 add.commute)
```
```   114     then show ?thesis ..
```
```   115   qed
```
```   116   with assms show ?thesis
```
```   117     unfolding limitin_sequentially
```
```   118     by simp
```
```   119 qed
```
```   120
```
```   121 lemma limitin_atin:
```
```   122    "limitin Y f y (atin X x) \<longleftrightarrow>
```
```   123         y \<in> topspace Y \<and>
```
```   124         (x \<in> topspace X
```
```   125         \<longrightarrow> (\<forall>V. openin Y V \<and> y \<in> V
```
```   126                  \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> f ` (U - {x}) \<subseteq> V)))"
```
```   127   by (auto simp: limitin_def eventually_atin image_subset_iff)
```
```   128
```
```   129 lemma limitin_atin_self:
```
```   130    "limitin Y f (f a) (atin X a) \<longleftrightarrow>
```
```   131         f a \<in> topspace Y \<and>
```
```   132         (a \<in> topspace X
```
```   133          \<longrightarrow> (\<forall>V. openin Y V \<and> f a \<in> V
```
```   134                   \<longrightarrow> (\<exists>U. openin X U \<and> a \<in> U \<and> f ` U \<subseteq> V)))"
```
```   135   unfolding limitin_atin by fastforce
```
```   136
```
```   137 lemma limitin_trivial:
```
```   138    "\<lbrakk>trivial_limit F; y \<in> topspace X\<rbrakk> \<Longrightarrow> limitin X f y F"
```
```   139   by (simp add: limitin_def)
```
```   140
```
```   141 lemma limitin_transform_eventually:
```
```   142    "\<lbrakk>eventually (\<lambda>x. f x = g x) F; limitin X f l F\<rbrakk> \<Longrightarrow> limitin X g l F"
```
```   143   unfolding limitin_def using eventually_elim2 by fastforce
```
```   144
```
```   145 lemma continuous_map_limit:
```
```   146   assumes "continuous_map X Y g" and f: "limitin X f l F"
```
```   147   shows "limitin Y (g \<circ> f) (g l) F"
```
```   148 proof -
```
```   149   have "g l \<in> topspace Y"
```
```   150     by (meson assms continuous_map_def limitin_topspace)
```
```   151   moreover
```
```   152   have "\<And>U. \<lbrakk>\<forall>V. openin X V \<and> l \<in> V \<longrightarrow> (\<forall>\<^sub>F x in F. f x \<in> V); openin Y U; g l \<in> U\<rbrakk>
```
```   153             \<Longrightarrow> \<forall>\<^sub>F x in F. g (f x) \<in> U"
```
```   154     using assms eventually_mono
```
```   155     by (fastforce simp: limitin_def dest!: openin_continuous_map_preimage)
```
```   156   ultimately show ?thesis
```
```   157     using f by (fastforce simp add: limitin_def)
```
```   158 qed
```
```   159
```
```   160
```
```   161 subsection\<open>Pointwise continuity in topological spaces\<close>
```
```   162
```
```   163 definition topcontinuous_at where
```
```   164   "topcontinuous_at X Y f x \<longleftrightarrow>
```
```   165      x \<in> topspace X \<and>
```
```   166      (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
```
```   167      (\<forall>V. openin Y V \<and> f x \<in> V
```
```   168           \<longrightarrow> (\<exists>U. openin X U \<and> x \<in> U \<and> (\<forall>y \<in> U. f y \<in> V)))"
```
```   169
```
```   170 lemma topcontinuous_at_atin:
```
```   171    "topcontinuous_at X Y f x \<longleftrightarrow>
```
```   172         x \<in> topspace X \<and>
```
```   173         (\<forall>x \<in> topspace X. f x \<in> topspace Y) \<and>
```
```   174         limitin Y f (f x) (atin X x)"
```
```   175   unfolding topcontinuous_at_def
```
```   176   by (fastforce simp add: limitin_atin)+
```
```   177
```
```   178 lemma continuous_map_eq_topcontinuous_at:
```
```   179    "continuous_map X Y f \<longleftrightarrow> (\<forall>x \<in> topspace X. topcontinuous_at X Y f x)"
```
```   180     (is "?lhs = ?rhs")
```
```   181 proof
```
```   182   assume ?lhs
```
```   183   then show ?rhs
```
```   184     by (auto simp: continuous_map_def topcontinuous_at_def)
```
```   185 next
```
```   186   assume R: ?rhs
```
```   187   then show ?lhs
```
```   188     apply (auto simp: continuous_map_def topcontinuous_at_def)
```
```   189     apply (subst openin_subopen, safe)
```
```   190     apply (drule bspec, assumption)
```
```   191     using openin_subset[of X] apply (auto simp: subset_iff dest!: spec)
```
```   192     done
```
```   193 qed
```
```   194
```
```   195 lemma continuous_map_atin:
```
```   196    "continuous_map X Y f \<longleftrightarrow> (\<forall>x \<in> topspace X. limitin Y f (f x) (atin X x))"
```
```   197   by (auto simp: limitin_def topcontinuous_at_atin continuous_map_eq_topcontinuous_at)
```
```   198
```
```   199 lemma limitin_continuous_map:
```
```   200    "\<lbrakk>continuous_map X Y f; a \<in> topspace X; f a = b\<rbrakk> \<Longrightarrow> limitin Y f b (atin X a)"
```
```   201   by (auto simp: continuous_map_atin)
```
```   202
```
```   203
```
```   204 subsection\<open>Combining theorems for continuous functions into the reals\<close>
```
```   205
```
```   206 lemma continuous_map_real_const [simp,continuous_intros]:
```
```   207    "continuous_map X euclideanreal (\<lambda>x. c)"
```
```   208   by simp
```
```   209
```
```   210 lemma continuous_map_real_mult [continuous_intros]:
```
```   211    "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
```
```   212    \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x * g x)"
```
```   213   by (simp add: continuous_map_atin tendsto_mult)
```
```   214
```
```   215 lemma continuous_map_real_pow [continuous_intros]:
```
```   216    "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x ^ n)"
```
```   217   by (induction n) (auto simp: continuous_map_real_mult)
```
```   218
```
```   219 lemma continuous_map_real_mult_left:
```
```   220    "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. c * f x)"
```
```   221   by (simp add: continuous_map_atin tendsto_mult)
```
```   222
```
```   223 lemma continuous_map_real_mult_left_eq:
```
```   224    "continuous_map X euclideanreal (\<lambda>x. c * f x) \<longleftrightarrow> c = 0 \<or> continuous_map X euclideanreal f"
```
```   225 proof (cases "c = 0")
```
```   226   case False
```
```   227   have "continuous_map X euclideanreal (\<lambda>x. c * f x) \<Longrightarrow> continuous_map X euclideanreal f"
```
```   228     apply (frule continuous_map_real_mult_left [where c="inverse c"])
```
```   229     apply (simp add: field_simps False)
```
```   230     done
```
```   231   with False show ?thesis
```
```   232     using continuous_map_real_mult_left by blast
```
```   233 qed simp
```
```   234
```
```   235 lemma continuous_map_real_mult_right:
```
```   236    "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x * c)"
```
```   237   by (simp add: continuous_map_atin tendsto_mult)
```
```   238
```
```   239 lemma continuous_map_real_mult_right_eq:
```
```   240    "continuous_map X euclideanreal (\<lambda>x. f x * c) \<longleftrightarrow> c = 0 \<or> continuous_map X euclideanreal f"
```
```   241   by (simp add: mult.commute flip: continuous_map_real_mult_left_eq)
```
```   242
```
```   243 lemma continuous_map_real_minus [continuous_intros]:
```
```   244    "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. - f x)"
```
```   245   by (simp add: continuous_map_atin tendsto_minus)
```
```   246
```
```   247 lemma continuous_map_real_minus_eq:
```
```   248    "continuous_map X euclideanreal (\<lambda>x. - f x) \<longleftrightarrow> continuous_map X euclideanreal f"
```
```   249   using continuous_map_real_mult_left_eq [where c = "-1"] by auto
```
```   250
```
```   251 lemma continuous_map_real_add [continuous_intros]:
```
```   252    "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
```
```   253    \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x + g x)"
```
```   254   by (simp add: continuous_map_atin tendsto_add)
```
```   255
```
```   256 lemma continuous_map_real_diff [continuous_intros]:
```
```   257    "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
```
```   258    \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x - g x)"
```
```   259   by (simp add: continuous_map_atin tendsto_diff)
```
```   260
```
```   261 lemma continuous_map_real_abs [continuous_intros]:
```
```   262    "continuous_map X euclideanreal f \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. abs(f x))"
```
```   263   by (simp add: continuous_map_atin tendsto_rabs)
```
```   264
```
```   265 lemma continuous_map_real_max [continuous_intros]:
```
```   266    "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
```
```   267    \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. max (f x) (g x))"
```
```   268   by (simp add: continuous_map_atin tendsto_max)
```
```   269
```
```   270 lemma continuous_map_real_min [continuous_intros]:
```
```   271    "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g\<rbrakk>
```
```   272    \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. min (f x) (g x))"
```
```   273   by (simp add: continuous_map_atin tendsto_min)
```
```   274
```
```   275 lemma continuous_map_sum [continuous_intros]:
```
```   276    "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x i)\<rbrakk>
```
```   277         \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. sum (f x) I)"
```
```   278   by (simp add: continuous_map_atin tendsto_sum)
```
```   279
```
```   280 lemma continuous_map_prod [continuous_intros]:
```
```   281    "\<lbrakk>finite I;
```
```   282          \<And>i. i \<in> I \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x i)\<rbrakk>
```
```   283         \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. prod (f x) I)"
```
```   284   by (simp add: continuous_map_atin tendsto_prod)
```
```   285
```
```   286 lemma continuous_map_real_inverse [continuous_intros]:
```
```   287    "\<lbrakk>continuous_map X euclideanreal f; \<And>x. x \<in> topspace X \<Longrightarrow> f x \<noteq> 0\<rbrakk>
```
```   288         \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. inverse(f x))"
```
```   289   by (simp add: continuous_map_atin tendsto_inverse)
```
```   290
```
```   291 lemma continuous_map_real_divide [continuous_intros]:
```
```   292    "\<lbrakk>continuous_map X euclideanreal f; continuous_map X euclideanreal g; \<And>x. x \<in> topspace X \<Longrightarrow> g x \<noteq> 0\<rbrakk>
```
```   293    \<Longrightarrow> continuous_map X euclideanreal (\<lambda>x. f x / g x)"
```
```   294   by (simp add: continuous_map_atin tendsto_divide)
```
```   295
```
```   296 end
```