generalized lemmas in Extended_Real_Limits
authorhoelzl
Tue Mar 05 15:43:22 2013 +0100 (2013-03-05)
changeset 51351dd1dd470690b
parent 51350 490f34774a9a
child 51352 fdecc2cd5649
child 51355 ef494f2288cf
generalized lemmas in Extended_Real_Limits
src/HOL/Library/Extended_Real.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Projective_Limit.thy
     1.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Mar 05 15:43:21 2013 +0100
     1.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Mar 05 15:43:22 2013 +0100
     1.3 @@ -131,10 +131,11 @@
     1.4  
     1.5  subsubsection "Addition"
     1.6  
     1.7 -instantiation ereal :: comm_monoid_add
     1.8 +instantiation ereal :: "{one, comm_monoid_add}"
     1.9  begin
    1.10  
    1.11  definition "0 = ereal 0"
    1.12 +definition "1 = ereal 1"
    1.13  
    1.14  function plus_ereal where
    1.15  "ereal r + ereal p = ereal (r + p)" |
    1.16 @@ -173,6 +174,8 @@
    1.17  qed
    1.18  end
    1.19  
    1.20 +instance ereal :: numeral ..
    1.21 +
    1.22  lemma real_of_ereal_0[simp]: "real (0::ereal) = 0"
    1.23    unfolding real_of_ereal_def zero_ereal_def by simp
    1.24  
    1.25 @@ -474,9 +477,7 @@
    1.26  instantiation ereal :: "{comm_monoid_mult, sgn}"
    1.27  begin
    1.28  
    1.29 -definition "1 = ereal 1"
    1.30 -
    1.31 -function sgn_ereal where
    1.32 +function sgn_ereal :: "ereal \<Rightarrow> ereal" where
    1.33    "sgn (ereal r) = ereal (sgn r)"
    1.34  | "sgn (\<infinity>::ereal) = 1"
    1.35  | "sgn (-\<infinity>::ereal) = -1"
    1.36 @@ -661,8 +662,6 @@
    1.37    using assms
    1.38    by (cases rule: ereal3_cases[of a b c]) (simp_all add: field_simps)
    1.39  
    1.40 -instance ereal :: numeral ..
    1.41 -
    1.42  lemma numeral_eq_ereal [simp]: "numeral w = ereal (numeral w)"
    1.43    apply (induct w rule: num_induct)
    1.44    apply (simp only: numeral_One one_ereal_def)
    1.45 @@ -1811,9 +1810,16 @@
    1.46    "f ----> l \<Longrightarrow> ALL n>=N. f n <= ereal B \<Longrightarrow> l ~= \<infinity>"
    1.47    using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
    1.48  
    1.49 -lemma Lim_bounded_ereal: "f ----> (l :: ereal) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
    1.50 +lemma Lim_bounded_ereal: "f ----> (l :: 'a::linorder_topology) \<Longrightarrow> ALL n>=M. f n <= C \<Longrightarrow> l<=C"
    1.51    by (intro LIMSEQ_le_const2) auto
    1.52  
    1.53 +lemma Lim_bounded2_ereal:
    1.54 +  assumes lim:"f ----> (l :: 'a::linorder_topology)" and ge: "ALL n>=N. f n >= C"
    1.55 +  shows "l>=C"
    1.56 +  using ge
    1.57 +  by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
    1.58 +     (auto simp: eventually_sequentially)
    1.59 +
    1.60  lemma real_of_ereal_mult[simp]:
    1.61    fixes a b :: ereal shows "real (a * b) = real a * real b"
    1.62    by (cases rule: ereal2_cases[of a b]) auto
     2.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 05 15:43:21 2013 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 05 15:43:22 2013 +0100
     2.3 @@ -11,6 +11,114 @@
     2.4    imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real"
     2.5  begin
     2.6  
     2.7 +lemma convergent_limsup_cl:
     2.8 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
     2.9 +  shows "convergent X \<Longrightarrow> limsup X = lim X"
    2.10 +  by (auto simp: convergent_def limI lim_imp_Limsup)
    2.11 +
    2.12 +lemma lim_increasing_cl:
    2.13 +  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
    2.14 +  obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
    2.15 +proof
    2.16 +  show "f ----> (SUP n. f n)"
    2.17 +    using assms
    2.18 +    by (intro increasing_tendsto)
    2.19 +       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
    2.20 +qed
    2.21 +
    2.22 +lemma lim_decreasing_cl:
    2.23 +  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
    2.24 +  obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
    2.25 +proof
    2.26 +  show "f ----> (INF n. f n)"
    2.27 +    using assms
    2.28 +    by (intro decreasing_tendsto)
    2.29 +       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
    2.30 +qed
    2.31 +
    2.32 +lemma compact_complete_linorder:
    2.33 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
    2.34 +  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
    2.35 +proof -
    2.36 +  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
    2.37 +    using seq_monosub[of X] unfolding comp_def by auto
    2.38 +  then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
    2.39 +    by (auto simp add: monoseq_def)
    2.40 +  then obtain l where "(X\<circ>r) ----> l"
    2.41 +     using lim_increasing_cl[of "X \<circ> r"] lim_decreasing_cl[of "X \<circ> r"] by auto
    2.42 +  then show ?thesis using `subseq r` by auto
    2.43 +qed
    2.44 +
    2.45 +lemma compact_UNIV: "compact (UNIV :: 'a::{complete_linorder, linorder_topology, second_countable_topology} set)"
    2.46 +  using compact_complete_linorder
    2.47 +  by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def)
    2.48 +
    2.49 +lemma compact_eq_closed:
    2.50 +  fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set"
    2.51 +  shows "compact S \<longleftrightarrow> closed S"
    2.52 +  using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed by auto
    2.53 +
    2.54 +lemma closed_contains_Sup_cl:
    2.55 +  fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set"
    2.56 +  assumes "closed S" "S \<noteq> {}" shows "Sup S \<in> S"
    2.57 +proof -
    2.58 +  from compact_eq_closed[of S] compact_attains_sup[of S] assms
    2.59 +  obtain s where "s \<in> S" "\<forall>t\<in>S. t \<le> s" by auto
    2.60 +  moreover then have "Sup S = s"
    2.61 +    by (auto intro!: Sup_eqI)
    2.62 +  ultimately show ?thesis
    2.63 +    by simp
    2.64 +qed
    2.65 +
    2.66 +lemma closed_contains_Inf_cl:
    2.67 +  fixes S :: "'a::{complete_linorder, linorder_topology, second_countable_topology} set"
    2.68 +  assumes "closed S" "S \<noteq> {}" shows "Inf S \<in> S"
    2.69 +proof -
    2.70 +  from compact_eq_closed[of S] compact_attains_inf[of S] assms
    2.71 +  obtain s where "s \<in> S" "\<forall>t\<in>S. s \<le> t" by auto
    2.72 +  moreover then have "Inf S = s"
    2.73 +    by (auto intro!: Inf_eqI)
    2.74 +  ultimately show ?thesis
    2.75 +    by simp
    2.76 +qed
    2.77 +
    2.78 +lemma ereal_dense3: 
    2.79 +  fixes x y :: ereal shows "x < y \<Longrightarrow> \<exists>r::rat. x < real_of_rat r \<and> real_of_rat r < y"
    2.80 +proof (cases x y rule: ereal2_cases, simp_all)
    2.81 +  fix r q :: real assume "r < q"
    2.82 +  from Rats_dense_in_real[OF this]
    2.83 +  show "\<exists>x. r < real_of_rat x \<and> real_of_rat x < q"
    2.84 +    by (fastforce simp: Rats_def)
    2.85 +next
    2.86 +  fix r :: real show "\<exists>x. r < real_of_rat x" "\<exists>x. real_of_rat x < r"
    2.87 +    using gt_ex[of r] lt_ex[of r] Rats_dense_in_real
    2.88 +    by (auto simp: Rats_def)
    2.89 +qed
    2.90 +
    2.91 +instance ereal :: second_countable_topology
    2.92 +proof (default, intro exI conjI)
    2.93 +  let ?B = "(\<Union>r\<in>\<rat>. {{..< r}, {r <..}} :: ereal set set)"
    2.94 +  show "countable ?B" by (auto intro: countable_rat)
    2.95 +  show "open = generate_topology ?B"
    2.96 +  proof (intro ext iffI)
    2.97 +    fix S :: "ereal set" assume "open S"
    2.98 +    then show "generate_topology ?B S"
    2.99 +      unfolding open_generated_order
   2.100 +    proof induct
   2.101 +      case (Basis b)
   2.102 +      then obtain e where "b = {..< e} \<or> b = {e <..}" by auto
   2.103 +      moreover have "{..<e} = \<Union>{{..<x}|x. x \<in> \<rat> \<and> x < e}" "{e<..} = \<Union>{{x<..}|x. x \<in> \<rat> \<and> e < x}"
   2.104 +        by (auto dest: ereal_dense3
   2.105 +                 simp del: ex_simps
   2.106 +                 simp add: ex_simps[symmetric] conj_commute Rats_def image_iff)
   2.107 +      ultimately show ?case
   2.108 +        by (auto intro: generate_topology.intros)
   2.109 +    qed (auto intro: generate_topology.intros)
   2.110 +  next
   2.111 +    fix S assume "generate_topology ?B S" then show "open S" by induct auto
   2.112 +  qed
   2.113 +qed
   2.114 +
   2.115  lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal"
   2.116    unfolding continuous_on_topological open_ereal_def by auto
   2.117  
   2.118 @@ -41,57 +149,6 @@
   2.119    shows "closed (uminus ` S)"
   2.120    using assms unfolding closed_def ereal_uminus_complement[symmetric] by (rule ereal_open_uminus)
   2.121  
   2.122 -lemma ereal_closed_contains_Inf:
   2.123 -  fixes S :: "ereal set"
   2.124 -  assumes "closed S" "S ~= {}"
   2.125 -  shows "Inf S : S"
   2.126 -proof (rule ccontr)
   2.127 -  assume "Inf S \<notin> S"
   2.128 -  then have a: "open (-S)" "Inf S:(- S)" using assms by auto
   2.129 -  show False
   2.130 -  proof (cases "Inf S")
   2.131 -    case MInf
   2.132 -    then have "(-\<infinity>) : - S" using a by auto
   2.133 -    then obtain y where "{..<ereal y} <= (-S)" using a open_MInfty2[of "- S"] by auto
   2.134 -    then have "ereal y <= Inf S" by (metis Compl_anti_mono Compl_lessThan atLeast_iff
   2.135 -      complete_lattice_class.Inf_greatest double_complement set_rev_mp)
   2.136 -    then show False using MInf by auto
   2.137 -  next
   2.138 -    case PInf
   2.139 -    then have "S={\<infinity>}" by (metis Inf_eq_PInfty assms(2))
   2.140 -    then show False using `Inf S ~: S` by (simp add: top_ereal_def)
   2.141 -  next
   2.142 -    case (real r)
   2.143 -    then have fin: "\<bar>Inf S\<bar> \<noteq> \<infinity>" by simp
   2.144 -    from ereal_open_cont_interval[OF a this] guess e . note e = this
   2.145 -    { fix x
   2.146 -      assume "x:S" then have "x>=Inf S" by (rule complete_lattice_class.Inf_lower)
   2.147 -      then have *: "x>Inf S-e" using e by (metis fin ereal_between(1) order_less_le_trans)
   2.148 -      { assume "x<Inf S+e"
   2.149 -        then have "x:{Inf S-e <..< Inf S+e}" using * by auto
   2.150 -        then have False using e `x:S` by auto
   2.151 -      } then have "x>=Inf S+e" by (metis linorder_le_less_linear)
   2.152 -    }
   2.153 -    then have "Inf S + e <= Inf S" by (metis le_Inf_iff)
   2.154 -    then show False using real e by (cases e) auto
   2.155 -  qed
   2.156 -qed
   2.157 -
   2.158 -lemma ereal_closed_contains_Sup:
   2.159 -  fixes S :: "ereal set"
   2.160 -  assumes "closed S" "S ~= {}"
   2.161 -  shows "Sup S : S"
   2.162 -proof -
   2.163 -  have "closed (uminus ` S)"
   2.164 -    by (metis assms(1) ereal_closed_uminus)
   2.165 -  then have "Inf (uminus ` S) : uminus ` S"
   2.166 -    using assms ereal_closed_contains_Inf[of "uminus ` S"] by auto
   2.167 -  then have "- Sup S : uminus ` S"
   2.168 -    using ereal_Sup_uminus_image_eq[of "uminus ` S"] by (auto simp: image_image)
   2.169 -  then show ?thesis
   2.170 -    by (metis imageI ereal_uminus_uminus ereal_minus_minus_image)
   2.171 -qed
   2.172 -
   2.173  lemma ereal_open_closed_aux:
   2.174    fixes S :: "ereal set"
   2.175    assumes "open S" "closed S"
   2.176 @@ -99,7 +156,7 @@
   2.177    shows "S = {}"
   2.178  proof (rule ccontr)
   2.179    assume "S ~= {}"
   2.180 -  then have *: "(Inf S):S" by (metis assms(2) ereal_closed_contains_Inf)
   2.181 +  then have *: "(Inf S):S" by (metis assms(2) closed_contains_Inf_cl)
   2.182    { assume "Inf S=(-\<infinity>)"
   2.183      then have False using * assms(3) by auto }
   2.184    moreover
   2.185 @@ -237,14 +294,6 @@
   2.186      ereal_lim_mult[of "(\<lambda>i. - X i)" "-L" net "ereal (-1)"]
   2.187    by (auto simp add: algebra_simps)
   2.188  
   2.189 -lemma Lim_bounded2_ereal:
   2.190 -  assumes lim:"f ----> (l :: ereal)"
   2.191 -    and ge: "ALL n>=N. f n >= C"
   2.192 -  shows "l>=C"
   2.193 -  using ge
   2.194 -  by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
   2.195 -     (auto simp: eventually_sequentially)
   2.196 -
   2.197  lemma ereal_open_atLeast: fixes x :: ereal shows "open {x..} \<longleftrightarrow> x = -\<infinity>"
   2.198  proof
   2.199    assume "x = -\<infinity>" then have "{x..} = UNIV" by auto
   2.200 @@ -272,74 +321,50 @@
   2.201      ereal_lim_mult[of "\<lambda>x. - (f x)" "-f0" net "- 1"]
   2.202    by (auto simp: ereal_uminus_reorder)
   2.203  
   2.204 -lemma convergent_ereal_limsup:
   2.205 -  fixes X :: "nat \<Rightarrow> ereal"
   2.206 -  shows "convergent X \<Longrightarrow> limsup X = lim X"
   2.207 -  by (auto simp: convergent_def limI lim_imp_Limsup)
   2.208 -
   2.209  lemma Liminf_PInfty:
   2.210    fixes f :: "'a \<Rightarrow> ereal"
   2.211    assumes "\<not> trivial_limit net"
   2.212    shows "(f ---> \<infinity>) net \<longleftrightarrow> Liminf net f = \<infinity>"
   2.213 -proof (intro lim_imp_Liminf iffI assms)
   2.214 -  assume rhs: "Liminf net f = \<infinity>"
   2.215 -  show "(f ---> \<infinity>) net"
   2.216 -    unfolding tendsto_PInfty
   2.217 -  proof
   2.218 -    fix r :: real
   2.219 -    have "ereal r < top" unfolding top_ereal_def by simp
   2.220 -    with rhs obtain P where "eventually P net" "r < INFI (Collect P) f"
   2.221 -      unfolding Liminf_def SUP_eq_top_iff top_ereal_def[symmetric] by auto
   2.222 -    then show "eventually (\<lambda>x. ereal r < f x) net"
   2.223 -      by (auto elim!: eventually_elim1 dest: less_INF_D)
   2.224 -  qed
   2.225 -qed
   2.226 +  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] using Liminf_le_Limsup[OF assms, of f] by auto
   2.227  
   2.228  lemma Limsup_MInfty:
   2.229    fixes f :: "'a \<Rightarrow> ereal"
   2.230    assumes "\<not> trivial_limit net"
   2.231    shows "(f ---> -\<infinity>) net \<longleftrightarrow> Limsup net f = -\<infinity>"
   2.232 -  using assms ereal_Lim_uminus[of f "-\<infinity>"] Liminf_PInfty[of _ "\<lambda>x. - (f x)"]
   2.233 -        ereal_Liminf_uminus[of _ f] by (auto simp: ereal_uminus_eq_reorder)
   2.234 +  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms] using Liminf_le_Limsup[OF assms, of f] by auto
   2.235  
   2.236  lemma convergent_ereal:
   2.237 -  fixes X :: "nat \<Rightarrow> ereal"
   2.238 +  fixes X :: "nat \<Rightarrow> 'a :: {complete_linorder, linorder_topology}"
   2.239    shows "convergent X \<longleftrightarrow> limsup X = liminf X"
   2.240    using tendsto_iff_Liminf_eq_Limsup[of sequentially]
   2.241    by (auto simp: convergent_def)
   2.242  
   2.243 -lemma limsup_INFI_SUPR:
   2.244 -  fixes f :: "nat \<Rightarrow> ereal"
   2.245 -  shows "limsup f = (INF n. SUP m:{n..}. f m)"
   2.246 -  using ereal_Limsup_uminus[of sequentially "\<lambda>x. - f x"]
   2.247 -  by (simp add: liminf_SUPR_INFI ereal_INFI_uminus ereal_SUPR_uminus)
   2.248 -
   2.249  lemma liminf_PInfty:
   2.250 -  fixes X :: "nat => ereal"
   2.251 -  shows "X ----> \<infinity> <-> liminf X = \<infinity>"
   2.252 +  fixes X :: "nat \<Rightarrow> ereal"
   2.253 +  shows "X ----> \<infinity> \<longleftrightarrow> liminf X = \<infinity>"
   2.254    by (metis Liminf_PInfty trivial_limit_sequentially)
   2.255  
   2.256  lemma limsup_MInfty:
   2.257 -  fixes X :: "nat => ereal"
   2.258 -  shows "X ----> (-\<infinity>) <-> limsup X = (-\<infinity>)"
   2.259 +  fixes X :: "nat \<Rightarrow> ereal"
   2.260 +  shows "X ----> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
   2.261    by (metis Limsup_MInfty trivial_limit_sequentially)
   2.262  
   2.263  lemma ereal_lim_mono:
   2.264 -  fixes X Y :: "nat => ereal"
   2.265 +  fixes X Y :: "nat => 'a::linorder_topology"
   2.266    assumes "\<And>n. N \<le> n \<Longrightarrow> X n <= Y n"
   2.267      and "X ----> x" "Y ----> y"
   2.268    shows "x <= y"
   2.269    using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
   2.270  
   2.271  lemma incseq_le_ereal:
   2.272 -  fixes X :: "nat \<Rightarrow> ereal"
   2.273 +  fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
   2.274    assumes inc: "incseq X" and lim: "X ----> L"
   2.275    shows "X N \<le> L"
   2.276    using inc by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
   2.277  
   2.278  lemma decseq_ge_ereal:
   2.279    assumes dec: "decseq X"
   2.280 -    and lim: "X ----> (L::ereal)"
   2.281 +    and lim: "X ----> (L::'a::linorder_topology)"
   2.282    shows "X N >= L"
   2.283    using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
   2.284  
   2.285 @@ -349,62 +374,25 @@
   2.286    by (metis abs_less_iff assms leI le_max_iff_disj
   2.287      less_eq_real_def less_le_not_le less_minus_iff minus_minus)
   2.288  
   2.289 -lemma lim_ereal_increasing:
   2.290 -  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<ge> f m"
   2.291 -  obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
   2.292 -proof
   2.293 -  show "f ----> (SUP n. f n)"
   2.294 -    using assms
   2.295 -    by (intro increasing_tendsto)
   2.296 -       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
   2.297 -qed
   2.298 -
   2.299 -lemma lim_ereal_decreasing:
   2.300 -  assumes "\<And>n m. n \<ge> m \<Longrightarrow> f n \<le> f m"
   2.301 -  obtains l where "f ----> (l::'a::{complete_linorder, linorder_topology})"
   2.302 -proof
   2.303 -  show "f ----> (INF n. f n)"
   2.304 -    using assms
   2.305 -    by (intro decreasing_tendsto)
   2.306 -       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
   2.307 -qed
   2.308 -
   2.309 -lemma compact_ereal:
   2.310 -  fixes X :: "nat \<Rightarrow> ereal"
   2.311 -  shows "\<exists>l r. subseq r \<and> (X \<circ> r) ----> l"
   2.312 -proof -
   2.313 -  obtain r where "subseq r" and mono: "monoseq (X \<circ> r)"
   2.314 -    using seq_monosub[of X] unfolding comp_def by auto
   2.315 -  then have "(\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) m \<le> (X \<circ> r) n) \<or> (\<forall>n m. m \<le> n \<longrightarrow> (X \<circ> r) n \<le> (X \<circ> r) m)"
   2.316 -    by (auto simp add: monoseq_def)
   2.317 -  then obtain l where "(X\<circ>r) ----> l"
   2.318 -     using lim_ereal_increasing[of "X \<circ> r"] lim_ereal_decreasing[of "X \<circ> r"] by auto
   2.319 -  then show ?thesis using `subseq r` by auto
   2.320 -qed
   2.321 -
   2.322  lemma ereal_Sup_lim:
   2.323 -  assumes "\<And>n. b n \<in> s" "b ----> (a::ereal)"
   2.324 +  assumes "\<And>n. b n \<in> s" "b ----> (a::'a::{complete_linorder, linorder_topology})"
   2.325    shows "a \<le> Sup s"
   2.326    by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
   2.327  
   2.328  lemma ereal_Inf_lim:
   2.329 -  assumes "\<And>n. b n \<in> s" "b ----> (a::ereal)"
   2.330 +  assumes "\<And>n. b n \<in> s" "b ----> (a::'a::{complete_linorder, linorder_topology})"
   2.331    shows "Inf s \<le> a"
   2.332    by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
   2.333  
   2.334  lemma SUP_Lim_ereal:
   2.335    fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
   2.336 -  assumes inc: "incseq X" and l: "X ----> l"
   2.337 -  shows "(SUP n. X n) = l"
   2.338 +  assumes inc: "incseq X" and l: "X ----> l" shows "(SUP n. X n) = l"
   2.339    using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l] by simp
   2.340  
   2.341 -lemma INF_Lim_ereal: "decseq X \<Longrightarrow> X ----> l \<Longrightarrow> (INF n. X n) = (l::ereal)"
   2.342 -  using SUP_Lim_ereal[of "\<lambda>i. - X i" "- l"]
   2.343 -  by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
   2.344 -
   2.345 -lemma LIMSEQ_ereal_INFI: "decseq X \<Longrightarrow> X ----> (INF n. X n :: ereal)"
   2.346 -  using LIMSEQ_SUP[of "\<lambda>i. - X i"]
   2.347 -  by (simp add: ereal_SUPR_uminus ereal_lim_uminus)
   2.348 +lemma INF_Lim_ereal:
   2.349 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder, linorder_topology}"
   2.350 +  assumes dec: "decseq X" and l: "X ----> l" shows "(INF n. X n) = l"
   2.351 +  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l] by simp
   2.352  
   2.353  lemma SUP_eq_LIMSEQ:
   2.354    assumes "mono f"
   2.355 @@ -421,48 +409,6 @@
   2.356      show "f ----> x" by auto }
   2.357  qed
   2.358  
   2.359 -lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"
   2.360 -  unfolding islimpt_def by blast
   2.361 -
   2.362 -
   2.363 -lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
   2.364 -  unfolding closure_def using islimpt_punctured by blast
   2.365 -
   2.366 -
   2.367 -lemma not_trivial_limit_within: "~trivial_limit (at x within S) = (x:closure(S-{x}))"
   2.368 -  using islimpt_in_closure by (metis trivial_limit_within)
   2.369 -
   2.370 -
   2.371 -lemma not_trivial_limit_within_ball:
   2.372 -  "(~trivial_limit (at x within S)) = (ALL e>0. S Int ball x e - {x} ~= {})"
   2.373 -  (is "?lhs = ?rhs")
   2.374 -proof -
   2.375 -  { assume "?lhs"
   2.376 -    { fix e :: real
   2.377 -      assume "e>0"
   2.378 -      then obtain y where "y:(S-{x}) & dist y x < e"
   2.379 -        using `?lhs` not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
   2.380 -        by auto
   2.381 -      then have "y : (S Int ball x e - {x})"
   2.382 -        unfolding ball_def by (simp add: dist_commute)
   2.383 -      then have "S Int ball x e - {x} ~= {}" by blast
   2.384 -    } then have "?rhs" by auto
   2.385 -  }
   2.386 -  moreover
   2.387 -  { assume "?rhs"
   2.388 -    { fix e :: real
   2.389 -      assume "e>0"
   2.390 -      then obtain y where "y : (S Int ball x e - {x})" using `?rhs` by blast
   2.391 -      then have "y:(S-{x}) & dist y x < e"
   2.392 -        unfolding ball_def by (simp add: dist_commute)
   2.393 -      then have "EX y:(S-{x}). dist y x < e" by auto
   2.394 -    }
   2.395 -    then have "?lhs"
   2.396 -      using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto
   2.397 -  }
   2.398 -  ultimately show ?thesis by auto
   2.399 -qed
   2.400 -
   2.401  lemma liminf_ereal_cminus:
   2.402    fixes f :: "nat \<Rightarrow> ereal"
   2.403    assumes "c \<noteq> -\<infinity>"
   2.404 @@ -484,43 +430,6 @@
   2.405  
   2.406  subsubsection {* Continuity *}
   2.407  
   2.408 -lemma continuous_imp_tendsto:
   2.409 -  assumes "continuous (at x0) f"
   2.410 -    and "x ----> x0"
   2.411 -  shows "(f o x) ----> (f x0)"
   2.412 -proof -
   2.413 -  { fix S
   2.414 -    assume "open S & (f x0):S"
   2.415 -    then obtain T where T_def: "open T & x0 : T & (ALL x:T. f x : S)"
   2.416 -       using assms continuous_at_open by metis
   2.417 -    then have "(EX N. ALL n>=N. x n : T)"
   2.418 -      using assms tendsto_explicit T_def by auto
   2.419 -    then have "(EX N. ALL n>=N. f(x n) : S)" using T_def by auto
   2.420 -  }
   2.421 -  then show ?thesis using tendsto_explicit[of "f o x" "f x0"] by auto
   2.422 -qed
   2.423 -
   2.424 -
   2.425 -lemma continuous_at_sequentially2:
   2.426 -  fixes f :: "'a::metric_space => 'b:: topological_space"
   2.427 -  shows "continuous (at x0) f <-> (ALL x. (x ----> x0) --> (f o x) ----> (f x0))"
   2.428 -proof -
   2.429 -  { assume "~(continuous (at x0) f)"
   2.430 -    then obtain T where
   2.431 -      T_def: "open T & f x0 : T & (ALL S. (open S & x0 : S) --> (EX x':S. f x' ~: T))"
   2.432 -      using continuous_at_open[of x0 f] by metis
   2.433 -    def X == "{x'. f x' ~: T}"
   2.434 -    then have "x0 islimpt X"
   2.435 -      unfolding islimpt_def using T_def by auto
   2.436 -    then obtain x where x_def: "(ALL n. x n : X) & x ----> x0"
   2.437 -      using islimpt_sequential[of x0 X] by auto
   2.438 -    then have "~(f o x) ----> (f x0)"
   2.439 -      unfolding tendsto_explicit using X_def T_def by auto
   2.440 -    then have "EX x. x ----> x0 & (~(f o x) ----> (f x0))" using x_def by auto
   2.441 -  }
   2.442 -  then show ?thesis using continuous_imp_tendsto by auto
   2.443 -qed
   2.444 -
   2.445  lemma continuous_at_of_ereal:
   2.446    fixes x0 :: ereal
   2.447    assumes "\<bar>x0\<bar> \<noteq> \<infinity>"
   2.448 @@ -606,35 +515,6 @@
   2.449    unfolding continuous_at_open using assms t1_space by auto
   2.450  
   2.451  
   2.452 -lemma closure_contains_Inf:
   2.453 -  fixes S :: "real set"
   2.454 -  assumes "S ~= {}" "EX B. ALL x:S. B<=x"
   2.455 -  shows "Inf S : closure S"
   2.456 -proof -
   2.457 -  have *: "ALL x:S. Inf S <= x"
   2.458 -    using Inf_lower_EX[of _ S] assms by metis
   2.459 -  { fix e
   2.460 -    assume "e>(0 :: real)"
   2.461 -    then obtain x where x_def: "x:S & x < Inf S + e" using Inf_close `S ~= {}` by auto
   2.462 -    moreover then have "x > Inf S - e" using * by auto
   2.463 -    ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
   2.464 -    then have "EX x:S. abs (x - Inf S) < e" using x_def by auto
   2.465 -  }
   2.466 -  then show ?thesis
   2.467 -    apply (subst closure_approachable)
   2.468 -    unfolding dist_norm apply auto
   2.469 -    done
   2.470 -qed
   2.471 -
   2.472 -
   2.473 -lemma closed_contains_Inf:
   2.474 -  fixes S :: "real set"
   2.475 -  assumes "S ~= {}" "EX B. ALL x:S. B<=x"
   2.476 -    and "closed S"
   2.477 -  shows "Inf S : S"
   2.478 -  by (metis closure_contains_Inf closure_closed assms)
   2.479 -
   2.480 -
   2.481  lemma mono_closed_real:
   2.482    fixes S :: "real set"
   2.483    assumes mono: "ALL y z. y:S & y<=z --> z:S"
     3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:21 2013 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Mar 05 15:43:22 2013 +0100
     3.3 @@ -956,6 +956,9 @@
     3.4  lemma islimpt_UNIV_iff: "x islimpt UNIV \<longleftrightarrow> \<not> open {x}"
     3.5    unfolding islimpt_def by (safe, fast, case_tac "T = {x}", fast, fast)
     3.6  
     3.7 +lemma islimpt_punctured: "x islimpt S = x islimpt (S-{x})"
     3.8 +  unfolding islimpt_def by blast
     3.9 +
    3.10  text {* A perfect space has no isolated points. *}
    3.11  
    3.12  lemma islimpt_UNIV [simp, intro]: "(x::'a::perfect_space) islimpt UNIV"
    3.13 @@ -1239,6 +1242,10 @@
    3.14  qed
    3.15  
    3.16  
    3.17 +lemma islimpt_in_closure: "(x islimpt S) = (x:closure(S-{x}))"
    3.18 +  unfolding closure_def using islimpt_punctured by blast
    3.19 +
    3.20 +
    3.21  subsection {* Frontier (aka boundary) *}
    3.22  
    3.23  definition "frontier S = closure S - interior S"
    3.24 @@ -1328,6 +1335,9 @@
    3.25    apply (drule_tac x=UNIV in spec, simp)
    3.26    done
    3.27  
    3.28 +lemma not_trivial_limit_within: "~trivial_limit (at x within S) = (x:closure(S-{x}))"
    3.29 +  using islimpt_in_closure by (metis trivial_limit_within)
    3.30 +
    3.31  text {* Some property holds "sufficiently close" to the limit point. *}
    3.32  
    3.33  lemma eventually_at: (* FIXME: this replaces Limits.eventually_at *)
    3.34 @@ -1817,6 +1827,62 @@
    3.35    shows "closed S ==> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
    3.36    by (metis closure_closed closure_approachable)
    3.37  
    3.38 +lemma closure_contains_Inf:
    3.39 +  fixes S :: "real set"
    3.40 +  assumes "S \<noteq> {}" "\<forall>x\<in>S. B \<le> x"
    3.41 +  shows "Inf S \<in> closure S"
    3.42 +  unfolding closure_approachable
    3.43 +proof safe
    3.44 +  have *: "\<forall>x\<in>S. Inf S \<le> x"
    3.45 +    using Inf_lower_EX[of _ S] assms by metis
    3.46 +
    3.47 +  fix e :: real assume "0 < e"
    3.48 +  then obtain x where x: "x \<in> S" "x < Inf S + e"
    3.49 +    using Inf_close `S \<noteq> {}` by auto
    3.50 +  moreover then have "x > Inf S - e" using * by auto
    3.51 +  ultimately have "abs (x - Inf S) < e" by (simp add: abs_diff_less_iff)
    3.52 +  then show "\<exists>x\<in>S. dist x (Inf S) < e"
    3.53 +    using x by (auto simp: dist_norm)
    3.54 +qed
    3.55 +
    3.56 +lemma closed_contains_Inf:
    3.57 +  fixes S :: "real set"
    3.58 +  assumes "S \<noteq> {}" "\<forall>x\<in>S. B \<le> x"
    3.59 +    and "closed S"
    3.60 +  shows "Inf S \<in> S"
    3.61 +  by (metis closure_contains_Inf closure_closed assms)
    3.62 +
    3.63 +
    3.64 +lemma not_trivial_limit_within_ball:
    3.65 +  "(\<not> trivial_limit (at x within S)) = (\<forall>e>0. S \<inter> ball x e - {x} \<noteq> {})"
    3.66 +  (is "?lhs = ?rhs")
    3.67 +proof -
    3.68 +  { assume "?lhs"
    3.69 +    { fix e :: real
    3.70 +      assume "e>0"
    3.71 +      then obtain y where "y:(S-{x}) & dist y x < e"
    3.72 +        using `?lhs` not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"]
    3.73 +        by auto
    3.74 +      then have "y : (S Int ball x e - {x})"
    3.75 +        unfolding ball_def by (simp add: dist_commute)
    3.76 +      then have "S Int ball x e - {x} ~= {}" by blast
    3.77 +    } then have "?rhs" by auto
    3.78 +  }
    3.79 +  moreover
    3.80 +  { assume "?rhs"
    3.81 +    { fix e :: real
    3.82 +      assume "e>0"
    3.83 +      then obtain y where "y : (S Int ball x e - {x})" using `?rhs` by blast
    3.84 +      then have "y:(S-{x}) & dist y x < e"
    3.85 +        unfolding ball_def by (simp add: dist_commute)
    3.86 +      then have "EX y:(S-{x}). dist y x < e" by auto
    3.87 +    }
    3.88 +    then have "?lhs"
    3.89 +      using not_trivial_limit_within[of x S] closure_approachable[of x "S - {x}"] by auto
    3.90 +  }
    3.91 +  ultimately show ?thesis by auto
    3.92 +qed
    3.93 +
    3.94  subsection {* Infimum Distance *}
    3.95  
    3.96  definition "infdist x A = (if A = {} then 0 else Inf {dist x a|a. a \<in> A})"
    3.97 @@ -3834,6 +3900,7 @@
    3.98    using assms unfolding continuous_at continuous_within
    3.99    by (rule Lim_at_within)
   3.100  
   3.101 +
   3.102  text{* Derive the epsilon-delta forms, which we often use as "definitions" *}
   3.103  
   3.104  lemma continuous_within_eps_delta:
   3.105 @@ -4386,6 +4453,20 @@
   3.106  unfolding continuous_within_topological [of x UNIV f, unfolded within_UNIV]
   3.107  unfolding imp_conjL by (intro all_cong imp_cong ex_cong conj_cong refl) auto
   3.108  
   3.109 +lemma continuous_imp_tendsto:
   3.110 +  assumes "continuous (at x0) f" and "x ----> x0"
   3.111 +  shows "(f \<circ> x) ----> (f x0)"
   3.112 +proof (rule topological_tendstoI)
   3.113 +  fix S
   3.114 +  assume "open S" "f x0 \<in> S"
   3.115 +  then obtain T where T_def: "open T" "x0 \<in> T" "\<forall>x\<in>T. f x \<in> S"
   3.116 +     using assms continuous_at_open by metis
   3.117 +  then have "eventually (\<lambda>n. x n \<in> T) sequentially"
   3.118 +    using assms T_def by (auto simp: tendsto_def)
   3.119 +  then show "eventually (\<lambda>n. (f \<circ> x) n \<in> S) sequentially"
   3.120 +    using T_def by (auto elim!: eventually_elim1)
   3.121 +qed
   3.122 +
   3.123  lemma continuous_on_open:
   3.124    shows "continuous_on s f \<longleftrightarrow>
   3.125          (\<forall>t. openin (subtopology euclidean (f ` s)) t
     4.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Mar 05 15:43:21 2013 +0100
     4.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Mar 05 15:43:22 2013 +0100
     4.3 @@ -1133,7 +1133,7 @@
     4.4    shows "(\<lambda>x. lim (\<lambda>i. f i x)) \<in> borel_measurable M"
     4.5  proof -
     4.6    have "\<And>x. lim (\<lambda>i. f i x) = (if convergent (\<lambda>i. f i x) then limsup (\<lambda>i. f i x) else (THE i. False))"
     4.7 -    using convergent_ereal_limsup by (simp add: lim_def convergent_def)
     4.8 +    by (simp add: lim_def convergent_def convergent_limsup_cl)
     4.9    then show ?thesis
    4.10      by simp
    4.11  qed
     5.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 05 15:43:21 2013 +0100
     5.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Tue Mar 05 15:43:22 2013 +0100
     5.3 @@ -303,7 +303,7 @@
     5.4        with `(\<Inter>i. A i) = {}` show False by auto
     5.5      qed
     5.6      ultimately show "(\<lambda>i. \<mu>G (A i)) ----> 0"
     5.7 -      using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (A i)"] by simp
     5.8 +      using LIMSEQ_INF[of "\<lambda>i. \<mu>G (A i)"] by simp
     5.9    qed fact+
    5.10    then guess \<mu> .. note \<mu> = this
    5.11    show ?thesis
     6.1 --- a/src/HOL/Probability/Measure_Space.thy	Tue Mar 05 15:43:21 2013 +0100
     6.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Mar 05 15:43:22 2013 +0100
     6.3 @@ -385,7 +385,7 @@
     6.4      finally have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f (A n)" . }
     6.5    ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)"
     6.6      by simp
     6.7 -  with LIMSEQ_ereal_INFI[OF decseq_fA]
     6.8 +  with LIMSEQ_INF[OF decseq_fA]
     6.9    show "(\<lambda>i. f (A i)) ----> f (\<Inter>i. A i)" by simp
    6.10  qed
    6.11  
    6.12 @@ -565,7 +565,7 @@
    6.13  lemma Lim_emeasure_decseq:
    6.14    assumes A: "range A \<subseteq> sets M" "decseq A" and fin: "\<And>i. emeasure M (A i) \<noteq> \<infinity>"
    6.15    shows "(\<lambda>i. emeasure M (A i)) ----> emeasure M (\<Inter>i. A i)"
    6.16 -  using LIMSEQ_ereal_INFI[OF decseq_emeasure, OF A]
    6.17 +  using LIMSEQ_INF[OF decseq_emeasure, OF A]
    6.18    using INF_emeasure_decseq[OF A fin] by simp
    6.19  
    6.20  lemma emeasure_subadditive:
     7.1 --- a/src/HOL/Probability/Projective_Limit.thy	Tue Mar 05 15:43:21 2013 +0100
     7.2 +++ b/src/HOL/Probability/Projective_Limit.thy	Tue Mar 05 15:43:22 2013 +0100
     7.3 @@ -515,7 +515,7 @@
     7.4        thus False using Z by simp
     7.5      qed
     7.6      ultimately show "(\<lambda>i. \<mu>G (Z i)) ----> 0"
     7.7 -      using LIMSEQ_ereal_INFI[of "\<lambda>i. \<mu>G (Z i)"] by simp
     7.8 +      using LIMSEQ_INF[of "\<lambda>i. \<mu>G (Z i)"] by simp
     7.9    qed
    7.10    then guess \<mu> .. note \<mu> = this
    7.11    def f \<equiv> "finmap_of J B"