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