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
```