src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
changeset 51000 c9adb50f74ad
parent 50104 de19856feb54
child 51329 4a3c453f99a1
     1.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jan 31 11:31:27 2013 +0100
     1.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Jan 31 11:31:30 2013 +0100
     1.3 @@ -288,16 +288,9 @@
     1.4    assumes lim:"f ----> (l :: ereal)"
     1.5      and ge: "ALL n>=N. f n >= C"
     1.6    shows "l>=C"
     1.7 -proof -
     1.8 -  def g == "(%i. -(f i))"
     1.9 -  { fix n
    1.10 -    assume "n>=N"
    1.11 -    then have "g n <= -C" using assms ereal_minus_le_minus g_def by auto }
    1.12 -  then have "ALL n>=N. g n <= -C" by auto
    1.13 -  moreover have limg: "g ----> (-l)" using g_def ereal_lim_uminus lim by auto
    1.14 -  ultimately have "-l <= -C" using Lim_bounded_ereal[of g "-l" _ "-C"] by auto
    1.15 -  then show ?thesis using ereal_minus_le_minus by auto
    1.16 -qed
    1.17 +  using ge
    1.18 +  by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
    1.19 +     (auto simp: eventually_sequentially)
    1.20  
    1.21  lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
    1.22  proof
    1.23 @@ -326,54 +319,69 @@
    1.24    fixes f :: "'a => ereal"
    1.25    shows "Liminf net f =
    1.26      Sup {l. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
    1.27 -  unfolding Liminf_Sup
    1.28 -proof (intro arg_cong[where f="\<lambda>P. Sup (Collect P)"] ext iffI allI impI)
    1.29 -  fix l S
    1.30 -  assume ev: "\<forall>y<l. eventually (\<lambda>x. y < f x) net" and "open S" "mono_set S" "l \<in> S"
    1.31 -  then have "S = UNIV \<or> S = {Inf S <..}"
    1.32 -    using ereal_open_mono_set[of S] by auto
    1.33 -  then show "eventually (\<lambda>x. f x \<in> S) net"
    1.34 -  proof
    1.35 -    assume S: "S = {Inf S<..}"
    1.36 -    then have "Inf S < l" using `l \<in> S` by auto
    1.37 -    then have "eventually (\<lambda>x. Inf S < f x) net" using ev by auto
    1.38 -    then show "eventually (\<lambda>x. f x \<in> S) net" by (subst S) auto
    1.39 -  qed auto
    1.40 +    (is "_ = Sup ?A")
    1.41 +proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
    1.42 +  fix P assume P: "eventually P net"
    1.43 +  fix S assume S: "mono_set S" "INFI (Collect P) f \<in> S"
    1.44 +  { fix x assume "P x"
    1.45 +    then have "INFI (Collect P) f \<le> f x"
    1.46 +      by (intro complete_lattice_class.INF_lower) simp
    1.47 +    with S have "f x \<in> S"
    1.48 +      by (simp add: mono_set) }
    1.49 +  with P show "eventually (\<lambda>x. f x \<in> S) net"
    1.50 +    by (auto elim: eventually_elim1)
    1.51  next
    1.52 -  fix l y
    1.53 -  assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "y < l"
    1.54 -  have "eventually  (\<lambda>x. f x \<in> {y <..}) net"
    1.55 -    using `y < l` by (intro S[rule_format]) auto
    1.56 -  then show "eventually (\<lambda>x. y < f x) net" by auto
    1.57 +  fix y l
    1.58 +  assume S: "\<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
    1.59 +  assume P: "\<forall>P. eventually P net \<longrightarrow> INFI (Collect P) f \<le> y"
    1.60 +  show "l \<le> y"
    1.61 +  proof (rule ereal_le_ereal)
    1.62 +    fix B assume "B < l"
    1.63 +    then have "eventually (\<lambda>x. f x \<in> {B <..}) net"
    1.64 +      by (intro S[rule_format]) auto
    1.65 +    then have "INFI {x. B < f x} f \<le> y"
    1.66 +      using P by auto
    1.67 +    moreover have "B \<le> INFI {x. B < f x} f"
    1.68 +      by (intro INF_greatest) auto
    1.69 +    ultimately show "B \<le> y"
    1.70 +      by simp
    1.71 +  qed
    1.72  qed
    1.73  
    1.74  lemma ereal_Limsup_Inf_monoset:
    1.75    fixes f :: "'a => ereal"
    1.76    shows "Limsup net f =
    1.77      Inf {l. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> S) net}"
    1.78 -  unfolding Limsup_Inf
    1.79 -proof (intro arg_cong[where f="\<lambda>P. Inf (Collect P)"] ext iffI allI impI)
    1.80 -  fix l S
    1.81 -  assume ev: "\<forall>y>l. eventually (\<lambda>x. f x < y) net" and "open S" "mono_set (uminus`S)" "l \<in> S"
    1.82 -  then have "open (uminus`S) \<and> mono_set (uminus`S)" by (simp add: ereal_open_uminus)
    1.83 -  then have "S = UNIV \<or> S = {..< Sup S}"
    1.84 -    unfolding ereal_open_mono_set ereal_Inf_uminus_image_eq ereal_image_uminus_shift by simp
    1.85 -  then show "eventually (\<lambda>x. f x \<in> S) net"
    1.86 -  proof
    1.87 -    assume S: "S = {..< Sup S}"
    1.88 -    then have "l < Sup S" using `l \<in> S` by auto
    1.89 -    then have "eventually (\<lambda>x. f x < Sup S) net" using ev by auto
    1.90 -    then show "eventually (\<lambda>x. f x \<in> S) net"  by (subst S) auto
    1.91 -  qed auto
    1.92 +    (is "_ = Inf ?A")
    1.93 +proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
    1.94 +  fix P assume P: "eventually P net"
    1.95 +  fix S assume S: "mono_set (uminus`S)" "SUPR (Collect P) f \<in> S"
    1.96 +  { fix x assume "P x"
    1.97 +    then have "f x \<le> SUPR (Collect P) f"
    1.98 +      by (intro complete_lattice_class.SUP_upper) simp
    1.99 +    with S(1)[unfolded mono_set, rule_format, of "- SUPR (Collect P) f" "- f x"] S(2)
   1.100 +    have "f x \<in> S"
   1.101 +      by (simp add: inj_image_mem_iff) }
   1.102 +  with P show "eventually (\<lambda>x. f x \<in> S) net"
   1.103 +    by (auto elim: eventually_elim1)
   1.104  next
   1.105 -  fix l y
   1.106 -  assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus`S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net" "l < y"
   1.107 -  have "eventually  (\<lambda>x. f x \<in> {..< y}) net"
   1.108 -    using `l < y` by (intro S[rule_format]) auto
   1.109 -  then show "eventually (\<lambda>x. f x < y) net" by auto
   1.110 +  fix y l
   1.111 +  assume S: "\<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually  (\<lambda>x. f x \<in> S) net"
   1.112 +  assume P: "\<forall>P. eventually P net \<longrightarrow> y \<le> SUPR (Collect P) f"
   1.113 +  show "y \<le> l"
   1.114 +  proof (rule ereal_ge_ereal, safe)
   1.115 +    fix B assume "l < B"
   1.116 +    then have "eventually (\<lambda>x. f x \<in> {..< B}) net"
   1.117 +      by (intro S[rule_format]) auto
   1.118 +    then have "y \<le> SUPR {x. f x < B} f"
   1.119 +      using P by auto
   1.120 +    moreover have "SUPR {x. f x < B} f \<le> B"
   1.121 +      by (intro SUP_least) auto
   1.122 +    ultimately show "y \<le> B"
   1.123 +      by simp
   1.124 +  qed
   1.125  qed
   1.126  
   1.127 -
   1.128  lemma open_uminus_iff: "open (uminus ` S) \<longleftrightarrow> open (S::ereal set)"
   1.129    using ereal_open_uminus[of S] ereal_open_uminus[of "uminus`S"] by auto
   1.130  
   1.131 @@ -434,21 +442,16 @@
   1.132    shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
   1.133  proof (intro lim_imp_Liminf iffI assms)
   1.134    assume rhs: "Liminf net f = \<infinity>"
   1.135 -  { fix S :: "ereal set"
   1.136 -    assume "open S & \<infinity> : S"
   1.137 -    then obtain m where "{ereal m<..} <= S" using open_PInfty2 by auto
   1.138 -    moreover
   1.139 -    have "eventually (\<lambda>x. f x \<in> {ereal m<..}) net"
   1.140 -      using rhs
   1.141 -      unfolding Liminf_Sup top_ereal_def[symmetric] Sup_eq_top_iff
   1.142 -      by (auto elim!: allE[where x="ereal m"] simp: top_ereal_def)
   1.143 -    ultimately
   1.144 -    have "eventually (%x. f x : S) net"
   1.145 -      apply (subst eventually_mono)
   1.146 -      apply auto
   1.147 -      done
   1.148 -  }
   1.149 -  then show "(f ---> \<infinity>) net" unfolding tendsto_def by auto
   1.150 +  show "(f ---> \<infinity>) net"
   1.151 +    unfolding tendsto_PInfty
   1.152 +  proof
   1.153 +    fix r :: real
   1.154 +    have "ereal r < top" unfolding top_ereal_def by simp
   1.155 +    with rhs obtain P where "eventually P net" "r < INFI (Collect P) f"
   1.156 +      unfolding Liminf_def SUP_eq_top_iff top_ereal_def[symmetric] by auto
   1.157 +    then show "eventually (\<lambda>x. ereal r < f x) net"
   1.158 +      by (auto elim!: eventually_elim1 dest: less_INF_D)
   1.159 +  qed
   1.160  qed
   1.161  
   1.162  lemma Limsup_MInfty:
   1.163 @@ -474,12 +477,12 @@
   1.164    show "(f ---> f0) net"
   1.165    proof (rule topological_tendstoI)
   1.166      fix S
   1.167 -    assume "open S""f0 \<in> S"
   1.168 +    assume "open S" "f0 \<in> S"
   1.169      then obtain a b where "a < Liminf net f" "Limsup net f < b" "{a<..<b} \<subseteq> S"
   1.170        using ereal_open_cont_interval2[of S f0] real lim by auto
   1.171      then have "eventually (\<lambda>x. f x \<in> {a<..<b}) net"
   1.172 -      unfolding Liminf_Sup Limsup_Inf less_Sup_iff Inf_less_iff
   1.173 -      by (auto intro!: eventually_conj)
   1.174 +      unfolding Liminf_def Limsup_def less_SUP_iff INF_less_iff
   1.175 +      by (auto intro!: eventually_conj elim: eventually_elim1 dest: less_INF_D SUP_lessD)
   1.176      with `{a<..<b} \<subseteq> S` show "eventually (%x. f x : S) net"
   1.177        by (rule_tac eventually_mono) auto
   1.178    qed
   1.179 @@ -518,7 +521,7 @@
   1.180    assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
   1.181      and "X ----> x" "Y ----> y"
   1.182    shows "x <= y"
   1.183 -  by (metis ereal_Liminf_eq_Limsup_iff[OF trivial_limit_sequentially] assms liminf_mono)
   1.184 +  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
   1.185  
   1.186  lemma incseq_le_ereal:
   1.187    fixes X :: "nat \<Rightarrow> ereal"
   1.188 @@ -577,114 +580,24 @@
   1.189    by (metis abs_less_iff assms leI le_max_iff_disj
   1.190      less_eq_real_def less_le_not_le less_minus_iff minus_minus)
   1.191  
   1.192 -lemma bounded_increasing_convergent2:
   1.193 -  fixes f::"nat => real"
   1.194 -  assumes "ALL n. f n <= B" "ALL n m. n>=m --> f n >= f m"
   1.195 -  shows "EX l. (f ---> l) sequentially"
   1.196 -proof -
   1.197 -  def N == "max (abs (f 0)) (abs B)"
   1.198 -  { fix n
   1.199 -    have "abs (f n) <= N"
   1.200 -      unfolding N_def
   1.201 -      apply (subst bounded_abs)
   1.202 -      using assms apply auto
   1.203 -      done }
   1.204 -  then have "bounded {f n| n::nat. True}"
   1.205 -    unfolding bounded_real by auto
   1.206 -  then show ?thesis
   1.207 -    apply (rule Topology_Euclidean_Space.bounded_increasing_convergent)
   1.208 -    using assms apply auto
   1.209 -    done
   1.210 -qed
   1.211 -
   1.212  lemma lim_ereal_increasing:
   1.213 -  assumes "\<And>n m. n >= m \<Longrightarrow> f n >= f m"
   1.214 -  obtains l where "f ----> (l::ereal)"
   1.215 -proof (cases "f = (\<lambda>x. - \<infinity>)")
   1.216 -  case True
   1.217 -  then show thesis
   1.218 -    using tendsto_const[of "- \<infinity>" sequentially] by (intro that[of "-\<infinity>"]) auto
   1.219 -next
   1.220 -  case False
   1.221 -  then obtain N where N_def: "f N > (-\<infinity>)" by (auto simp: fun_eq_iff)
   1.222 -  have "ALL n>=N. f n >= f N" using assms by auto
   1.223 -  then have minf: "ALL n>=N. f n > (-\<infinity>)" using N_def by auto
   1.224 -  def Y == "(%n. (if n>=N then f n else f N))"
   1.225 -  then have incy: "!!n m. n>=m ==> Y n >= Y m" using assms by auto
   1.226 -  from minf have minfy: "ALL n. Y n ~= (-\<infinity>)" using Y_def by auto
   1.227 -  show thesis
   1.228 -  proof (cases "EX B. ALL n. f n < ereal B")
   1.229 -    case False
   1.230 -    then show thesis
   1.231 -      apply -
   1.232 -      apply (rule that[of \<infinity>])
   1.233 -      unfolding Lim_PInfty not_ex not_all
   1.234 -      apply safe
   1.235 -      apply (erule_tac x=B in allE, safe)
   1.236 -      apply (rule_tac x=x in exI, safe)
   1.237 -      apply (rule order_trans[OF _ assms[rule_format]])
   1.238 -      apply auto
   1.239 -      done
   1.240 -  next
   1.241 -    case True
   1.242 -    then guess B ..
   1.243 -    then have "ALL n. Y n < ereal B" using Y_def by auto
   1.244 -    note B = this[rule_format]
   1.245 -    { fix n
   1.246 -      have "Y n < \<infinity>"
   1.247 -        using B[of n]
   1.248 -        apply (subst less_le_trans)
   1.249 -        apply auto
   1.250 -        done
   1.251 -      then have "Y n ~= \<infinity> & Y n ~= (-\<infinity>)" using minfy by auto
   1.252 -    }
   1.253 -    then have *: "ALL n. \<bar>Y n\<bar> \<noteq> \<infinity>" by auto
   1.254 -    { fix n
   1.255 -      have "real (Y n) < B"
   1.256 -      proof -
   1.257 -        case goal1
   1.258 -        then show ?case
   1.259 -          using B[of n] apply-apply(subst(asm) ereal_real'[THEN sym]) defer defer
   1.260 -          unfolding ereal_less using * by auto
   1.261 -      qed
   1.262 -    }
   1.263 -    then have B': "ALL n. (real (Y n) <= B)" using less_imp_le by auto
   1.264 -    have "EX l. (%n. real (Y n)) ----> l"
   1.265 -      apply (rule bounded_increasing_convergent2)
   1.266 -    proof safe
   1.267 -      show "\<And>n. real (Y n) <= B" using B' by auto
   1.268 -      fix n m :: nat
   1.269 -      assume "n<=m"
   1.270 -      then have "ereal (real (Y n)) <= ereal (real (Y m))"
   1.271 -        using incy[rule_format,of n m] apply(subst ereal_real)+
   1.272 -        using *[rule_format, of n] *[rule_format, of m] by auto
   1.273 -      then show "real (Y n) <= real (Y m)" by auto
   1.274 -    qed
   1.275 -    then guess l .. note l=this
   1.276 -    have "Y ----> ereal l"
   1.277 -      using l
   1.278 -      apply -
   1.279 -      apply (subst(asm) lim_ereal[THEN sym])
   1.280 -      unfolding ereal_real
   1.281 -      using * apply auto
   1.282 -      done
   1.283 -    then show thesis
   1.284 -      apply -
   1.285 -      apply (rule that[of "ereal l"])
   1.286 -      apply (subst tail_same_limit[of Y _ N])
   1.287 -      using Y_def apply auto
   1.288 -      done
   1.289 -  qed
   1.290 +  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
   1.291 +  obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
   1.292 +proof
   1.293 +  show "f ----> (SUP n. f n)"
   1.294 +    using assms
   1.295 +    by (intro increasing_tendsto)
   1.296 +       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
   1.297  qed
   1.298  
   1.299  lemma lim_ereal_decreasing:
   1.300 -  assumes "\<And>n m. n >= m \<Longrightarrow> f n <= f m"
   1.301 -  obtains l where "f ----> (l::ereal)"
   1.302 -proof -
   1.303 -  from lim_ereal_increasing[of "\<lambda>x. - f x"] assms
   1.304 -  obtain l where "(\<lambda>x. - f x) ----> l" by auto
   1.305 -  from ereal_lim_mult[OF this, of "- 1"] show thesis
   1.306 -    by (intro that[of "-l"]) (simp add: ereal_uminus_eq_reorder)
   1.307 +  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
   1.308 +  obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
   1.309 +proof
   1.310 +  show "f ----> (INF n. f n)"
   1.311 +    using assms
   1.312 +    by (intro decreasing_tendsto)
   1.313 +       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
   1.314  qed
   1.315  
   1.316  lemma compact_ereal:
   1.317 @@ -711,37 +624,17 @@
   1.318    by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
   1.319  
   1.320  lemma SUP_Lim_ereal:
   1.321 -  fixes X :: "nat \<Rightarrow> ereal"
   1.322 -  assumes "incseq X" "X ----> l"
   1.323 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
   1.324 +  assumes inc: "incseq X" and l: "X ----> l"
   1.325    shows "(SUP n. X n) = l"
   1.326 -proof (rule ereal_SUPI)
   1.327 -  fix n from assms show "X n \<le> l"
   1.328 -    by (intro incseq_le_ereal) (simp add: incseq_def)
   1.329 -next
   1.330 -  fix y assume "\<And>n. n \<in> UNIV \<Longrightarrow> X n \<le> y"
   1.331 -  with ereal_Sup_lim[OF _ `X ----> l`, of "{..y}"] show "l \<le> y" by auto
   1.332 -qed
   1.333 -
   1.334 -lemma LIMSEQ_ereal_SUPR:
   1.335 -  fixes X :: "nat \<Rightarrow> ereal"
   1.336 -  assumes "incseq X"
   1.337 -  shows "X ----> (SUP n. X n)"
   1.338 -proof (rule lim_ereal_increasing)
   1.339 -  fix n m :: nat
   1.340 -  assume "m \<le> n"
   1.341 -  then show "X m \<le> X n" using `incseq X` by (simp add: incseq_def)
   1.342 -next
   1.343 -  fix l
   1.344 -  assume "X ----> l"
   1.345 -  with SUP_Lim_ereal[of X, OF assms this] show ?thesis by simp
   1.346 -qed
   1.347 +  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l] by simp
   1.348  
   1.349  lemma INF_Lim_ereal: "decseq X \<Longrightarrow> X ----> l \<Longrightarrow> (INF n. X n) = (l::ereal)"
   1.350    using SUP_Lim_ereal[of "\<lambda>i. - X i" "- l"]
   1.351    by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
   1.352  
   1.353  lemma LIMSEQ_ereal_INFI: "decseq X \<Longrightarrow> X ----> (INF n. X n :: ereal)"
   1.354 -  using LIMSEQ_ereal_SUPR[of "\<lambda>i. - X i"]
   1.355 +  using LIMSEQ_SUP[of "\<lambda>i. - X i"]
   1.356    by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
   1.357  
   1.358  lemma SUP_eq_LIMSEQ:
   1.359 @@ -755,165 +648,66 @@
   1.360      from SUP_Lim_ereal[OF inc this]
   1.361      show "(SUP n. ereal (f n)) = ereal x" . }
   1.362    { assume "(SUP n. ereal (f n)) = ereal x"
   1.363 -    with LIMSEQ_ereal_SUPR[OF inc]
   1.364 +    with LIMSEQ_SUP[OF inc]
   1.365      show "f ----> x" by auto }
   1.366  qed
   1.367  
   1.368  lemma Liminf_within:
   1.369 -  fixes f :: "'a::metric_space => ereal"
   1.370 -  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
   1.371 -proof -
   1.372 -  let ?l="(SUP e:{0<..}. INF y:(S Int ball x e - {x}). f y)"
   1.373 -  { fix T
   1.374 -    assume T_def: "open T & mono_set T & ?l:T"
   1.375 -    have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
   1.376 -    proof -
   1.377 -      { assume "T=UNIV" then have ?thesis by (simp add: gt_ex) }
   1.378 -      moreover
   1.379 -      { assume "~(T=UNIV)"
   1.380 -        then obtain B where "T={B<..}" using T_def ereal_open_mono_set[of T] by auto
   1.381 -        then have "B<?l" using T_def by auto
   1.382 -        then obtain d where d_def: "0<d & B<(INF y:(S Int ball x d - {x}). f y)"
   1.383 -          unfolding less_SUP_iff by auto
   1.384 -        { fix y assume "y:S & 0 < dist y x & dist y x < d"
   1.385 -          then have "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
   1.386 -          then have "f y:T" using d_def INF_lower[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
   1.387 -        } then have ?thesis apply(rule_tac x="d" in exI) using d_def by auto
   1.388 -      }
   1.389 -      ultimately show ?thesis by auto
   1.390 -    qed
   1.391 -  }
   1.392 -  moreover
   1.393 -  { fix z
   1.394 -    assume a: "ALL T. open T --> mono_set T --> z : T -->
   1.395 -       (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
   1.396 -    { fix B
   1.397 -      assume "B<z"
   1.398 -      then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> B < f y)"
   1.399 -         using a[rule_format, of "{B<..}"] mono_greaterThan by auto
   1.400 -      { fix y
   1.401 -        assume "y:(S Int ball x d - {x})"
   1.402 -        then have "y:S & 0 < dist y x & dist y x < d"
   1.403 -          unfolding ball_def
   1.404 -          apply (simp add: dist_commute)
   1.405 -          apply (metis dist_eq_0_iff less_le zero_le_dist)
   1.406 -          done
   1.407 -        then have "B <= f y" using d_def by auto
   1.408 -      }
   1.409 -      then have "B <= INFI (S Int ball x d - {x}) f"
   1.410 -        apply (subst INF_greatest)
   1.411 -        apply auto
   1.412 -        done
   1.413 -      also have "...<=?l"
   1.414 -        apply (subst SUP_upper)
   1.415 -        using d_def apply auto
   1.416 -        done
   1.417 -      finally have "B<=?l" by auto
   1.418 -    }
   1.419 -    then have "z <= ?l" using ereal_le_ereal[of z "?l"] by auto
   1.420 -  }
   1.421 -  ultimately show ?thesis
   1.422 -    unfolding ereal_Liminf_Sup_monoset eventually_within
   1.423 -    apply (subst ereal_SupI[of _ "(SUP e:{0<..}. INFI (S Int ball x e - {x}) f)"])
   1.424 -    apply auto
   1.425 -    done
   1.426 +  fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
   1.427 +  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
   1.428 +  unfolding Liminf_def eventually_within
   1.429 +proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
   1.430 +  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
   1.431 +  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   1.432 +    by (auto simp: zero_less_dist_iff dist_commute)
   1.433 +  then show "\<exists>r>0. INFI (Collect P) f \<le> INFI (S \<inter> ball x r - {x}) f"
   1.434 +    by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
   1.435 +next
   1.436 +  fix d :: real assume "0 < d"
   1.437 +  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
   1.438 +    INFI (S \<inter> ball x d - {x}) f \<le> INFI (Collect P) f"
   1.439 +    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   1.440 +       (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
   1.441  qed
   1.442  
   1.443  lemma Limsup_within:
   1.444 -  fixes f :: "'a::metric_space => ereal"
   1.445 -  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
   1.446 -proof -
   1.447 -  let ?l = "(INF e:{0<..}. SUP y:(S Int ball x e - {x}). f y)"
   1.448 -  { fix T
   1.449 -    assume T_def: "open T & mono_set (uminus ` T) & ?l:T"
   1.450 -    have "EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T"
   1.451 -    proof -
   1.452 -      { assume "T = UNIV"
   1.453 -        then have ?thesis by (simp add: gt_ex) }
   1.454 -      moreover
   1.455 -      { assume "T \<noteq> UNIV"
   1.456 -        then have "~(uminus ` T = UNIV)"
   1.457 -          by (metis Int_UNIV_right Int_absorb1 image_mono ereal_minus_minus_image subset_UNIV)
   1.458 -        then have "uminus ` T = {Inf (uminus ` T)<..}"
   1.459 -          using T_def ereal_open_mono_set[of "uminus ` T"] ereal_open_uminus[of T] by auto
   1.460 -        then obtain B where "T={..<B}"
   1.461 -          unfolding ereal_Inf_uminus_image_eq ereal_uminus_lessThan[symmetric]
   1.462 -          unfolding inj_image_eq_iff[OF ereal_inj_on_uminus] by simp
   1.463 -        then have "?l<B" using T_def by auto
   1.464 -        then obtain d where d_def: "0<d & (SUP y:(S Int ball x d - {x}). f y)<B"
   1.465 -          unfolding INF_less_iff by auto
   1.466 -        { fix y
   1.467 -          assume "y:S & 0 < dist y x & dist y x < d"
   1.468 -          then have "y:(S Int ball x d - {x})"
   1.469 -            unfolding ball_def by (auto simp add: dist_commute)
   1.470 -          then have "f y:T"
   1.471 -            using d_def SUP_upper[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
   1.472 -        }
   1.473 -        then have ?thesis
   1.474 -          apply (rule_tac x="d" in exI)
   1.475 -          using d_def apply auto
   1.476 -          done
   1.477 -      }
   1.478 -      ultimately show ?thesis by auto
   1.479 -    qed
   1.480 -  }
   1.481 -  moreover
   1.482 -  { fix z
   1.483 -    assume a: "ALL T. open T --> mono_set (uminus ` T) --> z : T -->
   1.484 -       (EX d>0. ALL y:S. 0 < dist y x & dist y x < d --> f y : T)"
   1.485 -    { fix B
   1.486 -      assume "z<B"
   1.487 -      then obtain d where d_def: "d>0 & (ALL y:S. 0 < dist y x & dist y x < d --> f y<B)"
   1.488 -         using a[rule_format, of "{..<B}"] by auto
   1.489 -      { fix y
   1.490 -        assume "y:(S Int ball x d - {x})"
   1.491 -        then have "y:S & 0 < dist y x & dist y x < d"
   1.492 -          unfolding ball_def
   1.493 -          apply (simp add: dist_commute)
   1.494 -          apply (metis dist_eq_0_iff less_le zero_le_dist)
   1.495 -          done
   1.496 -        then have "f y <= B" using d_def by auto
   1.497 -      }
   1.498 -      then have "SUPR (S Int ball x d - {x}) f <= B"
   1.499 -        apply (subst SUP_least)
   1.500 -        apply auto
   1.501 -        done
   1.502 -      moreover
   1.503 -      have "?l<=SUPR (S Int ball x d - {x}) f"
   1.504 -        apply (subst INF_lower)
   1.505 -        using d_def apply auto
   1.506 -        done
   1.507 -      ultimately have "?l<=B" by auto
   1.508 -    } then have "?l <= z" using ereal_ge_ereal[of z "?l"] by auto
   1.509 -  }
   1.510 -  ultimately show ?thesis
   1.511 -    unfolding ereal_Limsup_Inf_monoset eventually_within
   1.512 -    apply (subst ereal_InfI)
   1.513 -    apply auto
   1.514 -    done
   1.515 +  fixes f :: "'a::metric_space => 'b::complete_lattice"
   1.516 +  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
   1.517 +  unfolding Limsup_def eventually_within
   1.518 +proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
   1.519 +  fix P d assume "0 < d" "\<forall>y. y \<in> S \<longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> P y"
   1.520 +  then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
   1.521 +    by (auto simp: zero_less_dist_iff dist_commute)
   1.522 +  then show "\<exists>r>0. SUPR (S \<inter> ball x r - {x}) f \<le> SUPR (Collect P) f"
   1.523 +    by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
   1.524 +next
   1.525 +  fix d :: real assume "0 < d"
   1.526 +  then show "\<exists>P. (\<exists>d>0. \<forall>xa. xa \<in> S \<longrightarrow> 0 < dist xa x \<and> dist xa x < d \<longrightarrow> P xa) \<and>
   1.527 +    SUPR (Collect P) f \<le> SUPR (S \<inter> ball x d - {x}) f"
   1.528 +    by (intro exI[of _ "\<lambda>y. y \<in> S \<inter> ball x d - {x}"])
   1.529 +       (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
   1.530  qed
   1.531  
   1.532 -
   1.533  lemma Liminf_within_UNIV:
   1.534 -  fixes f :: "'a::metric_space => ereal"
   1.535 +  fixes f :: "'a::metric_space => _"
   1.536    shows "Liminf (at x) f = Liminf (at x within UNIV) f"
   1.537    by simp (* TODO: delete *)
   1.538  
   1.539  
   1.540  lemma Liminf_at:
   1.541 -  fixes f :: "'a::metric_space => ereal"
   1.542 +  fixes f :: "'a::metric_space => _"
   1.543    shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
   1.544    using Liminf_within[of x UNIV f] by simp
   1.545  
   1.546  
   1.547  lemma Limsup_within_UNIV:
   1.548 -  fixes f :: "'a::metric_space => ereal"
   1.549 +  fixes f :: "'a::metric_space => _"
   1.550    shows "Limsup (at x) f = Limsup (at x within UNIV) f"
   1.551    by simp (* TODO: delete *)
   1.552  
   1.553  
   1.554  lemma Limsup_at:
   1.555 -  fixes f :: "'a::metric_space => ereal"
   1.556 +  fixes f :: "'a::metric_space => _"
   1.557    shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
   1.558    using Limsup_within[of x UNIV f] by simp
   1.559  
   1.560 @@ -1295,7 +1089,7 @@
   1.561  proof -
   1.562    have "incseq (\<lambda>i. \<Sum>j=0..<i. f j)"
   1.563      using ereal_add_mono[OF _ assms] by (auto intro!: incseq_SucI)
   1.564 -  from LIMSEQ_ereal_SUPR[OF this]
   1.565 +  from LIMSEQ_SUP[OF this]
   1.566    show ?thesis unfolding sums_def by (simp add: atLeast0LessThan)
   1.567  qed
   1.568