src/HOL/NSA/HLim.thy
author huffman
Fri May 29 09:22:56 2009 -0700 (2009-05-29)
changeset 31338 d41a8ba25b67
parent 28562 4e74209f113e
child 37765 26bdfb7b680b
permissions -rw-r--r--
generalize constants from Lim.thy to class metric_space
huffman@27468
     1
(*  Title       : HLim.thy
huffman@27468
     2
    ID          : $Id$
huffman@27468
     3
    Author      : Jacques D. Fleuriot
huffman@27468
     4
    Copyright   : 1998  University of Cambridge
huffman@27468
     5
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
huffman@27468
     6
*)
huffman@27468
     7
huffman@27468
     8
header{* Limits and Continuity (Nonstandard) *}
huffman@27468
     9
huffman@27468
    10
theory HLim
huffman@27468
    11
imports Star Lim
huffman@27468
    12
begin
huffman@27468
    13
huffman@27468
    14
text{*Nonstandard Definitions*}
huffman@27468
    15
huffman@27468
    16
definition
huffman@27468
    17
  NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
huffman@27468
    18
            ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
haftmann@28562
    19
  [code del]: "f -- a --NS> L =
huffman@27468
    20
    (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
huffman@27468
    21
huffman@27468
    22
definition
huffman@27468
    23
  isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
huffman@27468
    24
    --{*NS definition dispenses with limit notions*}
haftmann@28562
    25
  [code del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
huffman@27468
    26
         ( *f* f) y @= star_of (f a))"
huffman@27468
    27
huffman@27468
    28
definition
huffman@27468
    29
  isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
haftmann@28562
    30
  [code del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
huffman@27468
    31
huffman@27468
    32
huffman@27468
    33
subsection {* Limits of Functions *}
huffman@27468
    34
huffman@27468
    35
lemma NSLIM_I:
huffman@27468
    36
  "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
huffman@27468
    37
   \<Longrightarrow> f -- a --NS> L"
huffman@27468
    38
by (simp add: NSLIM_def)
huffman@27468
    39
huffman@27468
    40
lemma NSLIM_D:
huffman@27468
    41
  "\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
huffman@27468
    42
   \<Longrightarrow> starfun f x \<approx> star_of L"
huffman@27468
    43
by (simp add: NSLIM_def)
huffman@27468
    44
huffman@27468
    45
text{*Proving properties of limits using nonstandard definition.
huffman@27468
    46
      The properties hold for standard limits as well!*}
huffman@27468
    47
huffman@27468
    48
lemma NSLIM_mult:
huffman@27468
    49
  fixes l m :: "'a::real_normed_algebra"
huffman@27468
    50
  shows "[| f -- x --NS> l; g -- x --NS> m |]
huffman@27468
    51
      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
huffman@27468
    52
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
huffman@27468
    53
huffman@27468
    54
lemma starfun_scaleR [simp]:
huffman@27468
    55
  "starfun (\<lambda>x. f x *\<^sub>R g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
huffman@27468
    56
by transfer (rule refl)
huffman@27468
    57
huffman@27468
    58
lemma NSLIM_scaleR:
huffman@27468
    59
  "[| f -- x --NS> l; g -- x --NS> m |]
huffman@27468
    60
      ==> (%x. f(x) *\<^sub>R g(x)) -- x --NS> (l *\<^sub>R m)"
huffman@27468
    61
by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
huffman@27468
    62
huffman@27468
    63
lemma NSLIM_add:
huffman@27468
    64
     "[| f -- x --NS> l; g -- x --NS> m |]
huffman@27468
    65
      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
huffman@27468
    66
by (auto simp add: NSLIM_def intro!: approx_add)
huffman@27468
    67
huffman@27468
    68
lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
huffman@27468
    69
by (simp add: NSLIM_def)
huffman@27468
    70
huffman@27468
    71
lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
huffman@27468
    72
by (simp add: NSLIM_def)
huffman@27468
    73
huffman@27468
    74
lemma NSLIM_diff:
huffman@27468
    75
  "\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
huffman@27468
    76
by (simp only: diff_def NSLIM_add NSLIM_minus)
huffman@27468
    77
huffman@27468
    78
lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"
huffman@27468
    79
by (simp only: NSLIM_add NSLIM_minus)
huffman@27468
    80
huffman@27468
    81
lemma NSLIM_inverse:
huffman@27468
    82
  fixes L :: "'a::real_normed_div_algebra"
huffman@27468
    83
  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
huffman@27468
    84
      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
huffman@27468
    85
apply (simp add: NSLIM_def, clarify)
huffman@27468
    86
apply (drule spec)
huffman@27468
    87
apply (auto simp add: star_of_approx_inverse)
huffman@27468
    88
done
huffman@27468
    89
huffman@27468
    90
lemma NSLIM_zero:
huffman@27468
    91
  assumes f: "f -- a --NS> l" shows "(%x. f(x) - l) -- a --NS> 0"
huffman@27468
    92
proof -
huffman@27468
    93
  have "(\<lambda>x. f x - l) -- a --NS> l - l"
huffman@27468
    94
    by (rule NSLIM_diff [OF f NSLIM_const])
huffman@27468
    95
  thus ?thesis by simp
huffman@27468
    96
qed
huffman@27468
    97
huffman@27468
    98
lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
huffman@27468
    99
apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
huffman@27468
   100
apply (auto simp add: diff_minus add_assoc)
huffman@27468
   101
done
huffman@27468
   102
huffman@27468
   103
lemma NSLIM_const_not_eq:
huffman@27468
   104
  fixes a :: "'a::real_normed_algebra_1"
huffman@27468
   105
  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --NS> L"
huffman@27468
   106
apply (simp add: NSLIM_def)
huffman@27468
   107
apply (rule_tac x="star_of a + of_hypreal epsilon" in exI)
huffman@27468
   108
apply (simp add: hypreal_epsilon_not_zero approx_def)
huffman@27468
   109
done
huffman@27468
   110
huffman@27468
   111
lemma NSLIM_not_zero:
huffman@27468
   112
  fixes a :: "'a::real_normed_algebra_1"
huffman@27468
   113
  shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>x. k) -- a --NS> 0"
huffman@27468
   114
by (rule NSLIM_const_not_eq)
huffman@27468
   115
huffman@27468
   116
lemma NSLIM_const_eq:
huffman@27468
   117
  fixes a :: "'a::real_normed_algebra_1"
huffman@27468
   118
  shows "(\<lambda>x. k) -- a --NS> L \<Longrightarrow> k = L"
huffman@27468
   119
apply (rule ccontr)
huffman@27468
   120
apply (blast dest: NSLIM_const_not_eq)
huffman@27468
   121
done
huffman@27468
   122
huffman@27468
   123
lemma NSLIM_unique:
huffman@27468
   124
  fixes a :: "'a::real_normed_algebra_1"
huffman@27468
   125
  shows "\<lbrakk>f -- a --NS> L; f -- a --NS> M\<rbrakk> \<Longrightarrow> L = M"
huffman@27468
   126
apply (drule (1) NSLIM_diff)
huffman@27468
   127
apply (auto dest!: NSLIM_const_eq)
huffman@27468
   128
done
huffman@27468
   129
huffman@27468
   130
lemma NSLIM_mult_zero:
huffman@27468
   131
  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
huffman@27468
   132
  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
huffman@27468
   133
by (drule NSLIM_mult, auto)
huffman@27468
   134
huffman@27468
   135
lemma NSLIM_self: "(%x. x) -- a --NS> a"
huffman@27468
   136
by (simp add: NSLIM_def)
huffman@27468
   137
huffman@27468
   138
subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
huffman@27468
   139
huffman@27468
   140
lemma LIM_NSLIM:
huffman@27468
   141
  assumes f: "f -- a --> L" shows "f -- a --NS> L"
huffman@27468
   142
proof (rule NSLIM_I)
huffman@27468
   143
  fix x
huffman@27468
   144
  assume neq: "x \<noteq> star_of a"
huffman@27468
   145
  assume approx: "x \<approx> star_of a"
huffman@27468
   146
  have "starfun f x - star_of L \<in> Infinitesimal"
huffman@27468
   147
  proof (rule InfinitesimalI2)
huffman@27468
   148
    fix r::real assume r: "0 < r"
huffman@27468
   149
    from LIM_D [OF f r]
huffman@27468
   150
    obtain s where s: "0 < s" and
huffman@27468
   151
      less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x - L) < r"
huffman@27468
   152
      by fast
huffman@27468
   153
    from less_r have less_r':
huffman@27468
   154
       "\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x - star_of a) < star_of s\<rbrakk>
huffman@27468
   155
        \<Longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
huffman@27468
   156
      by transfer
huffman@27468
   157
    from approx have "x - star_of a \<in> Infinitesimal"
huffman@27468
   158
      by (unfold approx_def)
huffman@27468
   159
    hence "hnorm (x - star_of a) < star_of s"
huffman@27468
   160
      using s by (rule InfinitesimalD2)
huffman@27468
   161
    with neq show "hnorm (starfun f x - star_of L) < star_of r"
huffman@27468
   162
      by (rule less_r')
huffman@27468
   163
  qed
huffman@27468
   164
  thus "starfun f x \<approx> star_of L"
huffman@27468
   165
    by (unfold approx_def)
huffman@27468
   166
qed
huffman@27468
   167
huffman@27468
   168
lemma NSLIM_LIM:
huffman@27468
   169
  assumes f: "f -- a --NS> L" shows "f -- a --> L"
huffman@27468
   170
proof (rule LIM_I)
huffman@27468
   171
  fix r::real assume r: "0 < r"
huffman@27468
   172
  have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
huffman@27468
   173
        \<longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
huffman@27468
   174
  proof (rule exI, safe)
huffman@27468
   175
    show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
huffman@27468
   176
  next
huffman@27468
   177
    fix x assume neq: "x \<noteq> star_of a"
huffman@27468
   178
    assume "hnorm (x - star_of a) < epsilon"
huffman@27468
   179
    with Infinitesimal_epsilon
huffman@27468
   180
    have "x - star_of a \<in> Infinitesimal"
huffman@27468
   181
      by (rule hnorm_less_Infinitesimal)
huffman@27468
   182
    hence "x \<approx> star_of a"
huffman@27468
   183
      by (unfold approx_def)
huffman@27468
   184
    with f neq have "starfun f x \<approx> star_of L"
huffman@27468
   185
      by (rule NSLIM_D)
huffman@27468
   186
    hence "starfun f x - star_of L \<in> Infinitesimal"
huffman@27468
   187
      by (unfold approx_def)
huffman@27468
   188
    thus "hnorm (starfun f x - star_of L) < star_of r"
huffman@27468
   189
      using r by (rule InfinitesimalD2)
huffman@27468
   190
  qed
huffman@27468
   191
  thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r"
huffman@27468
   192
    by transfer
huffman@27468
   193
qed
huffman@27468
   194
huffman@27468
   195
theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
huffman@27468
   196
by (blast intro: LIM_NSLIM NSLIM_LIM)
huffman@27468
   197
huffman@27468
   198
huffman@27468
   199
subsection {* Continuity *}
huffman@27468
   200
huffman@27468
   201
lemma isNSContD:
huffman@27468
   202
  "\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
huffman@27468
   203
by (simp add: isNSCont_def)
huffman@27468
   204
huffman@27468
   205
lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
huffman@27468
   206
by (simp add: isNSCont_def NSLIM_def)
huffman@27468
   207
huffman@27468
   208
lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
huffman@27468
   209
apply (simp add: isNSCont_def NSLIM_def, auto)
huffman@27468
   210
apply (case_tac "y = star_of a", auto)
huffman@27468
   211
done
huffman@27468
   212
huffman@27468
   213
text{*NS continuity can be defined using NS Limit in
huffman@27468
   214
    similar fashion to standard def of continuity*}
huffman@27468
   215
lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
huffman@27468
   216
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
huffman@27468
   217
huffman@27468
   218
text{*Hence, NS continuity can be given
huffman@27468
   219
  in terms of standard limit*}
huffman@27468
   220
lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
huffman@27468
   221
by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
huffman@27468
   222
huffman@27468
   223
text{*Moreover, it's trivial now that NS continuity
huffman@27468
   224
  is equivalent to standard continuity*}
huffman@27468
   225
lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
huffman@27468
   226
apply (simp add: isCont_def)
huffman@27468
   227
apply (rule isNSCont_LIM_iff)
huffman@27468
   228
done
huffman@27468
   229
huffman@27468
   230
text{*Standard continuity ==> NS continuity*}
huffman@27468
   231
lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
huffman@27468
   232
by (erule isNSCont_isCont_iff [THEN iffD2])
huffman@27468
   233
huffman@27468
   234
text{*NS continuity ==> Standard continuity*}
huffman@27468
   235
lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
huffman@27468
   236
by (erule isNSCont_isCont_iff [THEN iffD1])
huffman@27468
   237
huffman@27468
   238
text{*Alternative definition of continuity*}
huffman@27468
   239
huffman@27468
   240
(* Prove equivalence between NS limits - *)
huffman@27468
   241
(* seems easier than using standard def  *)
huffman@27468
   242
lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
huffman@27468
   243
apply (simp add: NSLIM_def, auto)
huffman@27468
   244
apply (drule_tac x = "star_of a + x" in spec)
huffman@27468
   245
apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
huffman@27468
   246
apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
huffman@27468
   247
apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
huffman@27468
   248
 prefer 2 apply (simp add: add_commute diff_def [symmetric])
huffman@27468
   249
apply (rule_tac x = x in star_cases)
huffman@27468
   250
apply (rule_tac [2] x = x in star_cases)
huffman@27468
   251
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
huffman@27468
   252
done
huffman@27468
   253
huffman@27468
   254
lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
huffman@27468
   255
by (rule NSLIM_h_iff)
huffman@27468
   256
huffman@27468
   257
lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
huffman@27468
   258
by (simp add: isNSCont_def)
huffman@27468
   259
huffman@27468
   260
lemma isNSCont_inverse:
huffman@27468
   261
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
huffman@27468
   262
  shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
huffman@27468
   263
by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
huffman@27468
   264
huffman@27468
   265
lemma isNSCont_const [simp]: "isNSCont (%x. k) a"
huffman@27468
   266
by (simp add: isNSCont_def)
huffman@27468
   267
huffman@27468
   268
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)"
huffman@27468
   269
apply (simp add: isNSCont_def)
huffman@27468
   270
apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs)
huffman@27468
   271
done
huffman@27468
   272
huffman@27468
   273
huffman@27468
   274
subsection {* Uniform Continuity *}
huffman@27468
   275
huffman@27468
   276
lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
huffman@27468
   277
by (simp add: isNSUCont_def)
huffman@27468
   278
huffman@27468
   279
lemma isUCont_isNSUCont:
huffman@27468
   280
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
huffman@27468
   281
  assumes f: "isUCont f" shows "isNSUCont f"
huffman@27468
   282
proof (unfold isNSUCont_def, safe)
huffman@27468
   283
  fix x y :: "'a star"
huffman@27468
   284
  assume approx: "x \<approx> y"
huffman@27468
   285
  have "starfun f x - starfun f y \<in> Infinitesimal"
huffman@27468
   286
  proof (rule InfinitesimalI2)
huffman@27468
   287
    fix r::real assume r: "0 < r"
huffman@27468
   288
    with f obtain s where s: "0 < s" and
huffman@27468
   289
      less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r"
huffman@31338
   290
      by (auto simp add: isUCont_def dist_norm)
huffman@27468
   291
    from less_r have less_r':
huffman@27468
   292
       "\<And>x y. hnorm (x - y) < star_of s
huffman@27468
   293
        \<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
huffman@27468
   294
      by transfer
huffman@27468
   295
    from approx have "x - y \<in> Infinitesimal"
huffman@27468
   296
      by (unfold approx_def)
huffman@27468
   297
    hence "hnorm (x - y) < star_of s"
huffman@27468
   298
      using s by (rule InfinitesimalD2)
huffman@27468
   299
    thus "hnorm (starfun f x - starfun f y) < star_of r"
huffman@27468
   300
      by (rule less_r')
huffman@27468
   301
  qed
huffman@27468
   302
  thus "starfun f x \<approx> starfun f y"
huffman@27468
   303
    by (unfold approx_def)
huffman@27468
   304
qed
huffman@27468
   305
huffman@27468
   306
lemma isNSUCont_isUCont:
huffman@27468
   307
  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
huffman@27468
   308
  assumes f: "isNSUCont f" shows "isUCont f"
huffman@31338
   309
proof (unfold isUCont_def dist_norm, safe)
huffman@27468
   310
  fix r::real assume r: "0 < r"
huffman@27468
   311
  have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s
huffman@27468
   312
        \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
huffman@27468
   313
  proof (rule exI, safe)
huffman@27468
   314
    show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
huffman@27468
   315
  next
huffman@27468
   316
    fix x y :: "'a star"
huffman@27468
   317
    assume "hnorm (x - y) < epsilon"
huffman@27468
   318
    with Infinitesimal_epsilon
huffman@27468
   319
    have "x - y \<in> Infinitesimal"
huffman@27468
   320
      by (rule hnorm_less_Infinitesimal)
huffman@27468
   321
    hence "x \<approx> y"
huffman@27468
   322
      by (unfold approx_def)
huffman@27468
   323
    with f have "starfun f x \<approx> starfun f y"
huffman@27468
   324
      by (simp add: isNSUCont_def)
huffman@27468
   325
    hence "starfun f x - starfun f y \<in> Infinitesimal"
huffman@27468
   326
      by (unfold approx_def)
huffman@27468
   327
    thus "hnorm (starfun f x - starfun f y) < star_of r"
huffman@27468
   328
      using r by (rule InfinitesimalD2)
huffman@27468
   329
  qed
huffman@27468
   330
  thus "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
huffman@27468
   331
    by transfer
huffman@27468
   332
qed
huffman@27468
   333
huffman@27468
   334
end