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