new material connected with HOL Light measure theory, plus more rationalisation
authorpaulson <lp15@cam.ac.uk>
Wed Sep 28 17:01:01 2016 +0100 (2016-09-28)
changeset 63952354808e9f44b
parent 63950 cdc1e59aa513
child 63953 b5d7806c9396
new material connected with HOL Light measure theory, plus more rationalisation
src/HOL/Analysis/Borel_Space.thy
src/HOL/Analysis/Bounded_Linear_Function.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Euclidean_Space.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Deriv.thy
src/HOL/Fields.thy
src/HOL/Groups_Big.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Limits.thy
src/HOL/Order_Relation.thy
src/HOL/Probability/Helly_Selection.thy
src/HOL/Probability/Weak_Convergence.thy
src/HOL/Series.thy
src/HOL/Set.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Analysis/Borel_Space.thy	Mon Sep 26 07:56:54 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Borel_Space.thy	Wed Sep 28 17:01:01 2016 +0100
     1.3 @@ -101,7 +101,7 @@
     1.4    assumes mono: "mono_on f A" and deriv: "(f has_real_derivative D) (at x)"
     1.5    assumes "x \<in> interior A"
     1.6    shows "D \<ge> 0"
     1.7 -proof (rule tendsto_le_const)
     1.8 +proof (rule tendsto_lowerbound)
     1.9    let ?A' = "(\<lambda>y. y - x) ` interior A"
    1.10    from deriv show "((\<lambda>h. (f (x + h) - f x) / h) \<longlongrightarrow> D) (at 0)"
    1.11        by (simp add: field_has_derivative_at has_field_derivative_def)
     2.1 --- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Mon Sep 26 07:56:54 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Wed Sep 28 17:01:01 2016 +0100
     2.3 @@ -328,7 +328,7 @@
     2.4          have tendsto_v: "(\<lambda>m. norm (X n x - X m x)) \<longlonglongrightarrow> norm (X n x - Blinfun v x)"
     2.5            by (auto intro!: tendsto_intros Bv)
     2.6          show "norm ((X n - Blinfun v) x) \<le> r' * norm x"
     2.7 -          by (auto intro!: tendsto_ge_const tendsto_v ev_le simp: blinfun.bilinear_simps)
     2.8 +          by (auto intro!: tendsto_upperbound tendsto_v ev_le simp: blinfun.bilinear_simps)
     2.9        qed (simp add: \<open>0 < r'\<close> less_imp_le)
    2.10        thus "norm (X n - Blinfun v) < r"
    2.11          by (metis \<open>r' < r\<close> le_less_trans)
     3.1 --- a/src/HOL/Analysis/Derivative.thy	Mon Sep 26 07:56:54 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Derivative.thy	Wed Sep 28 17:01:01 2016 +0100
     3.3 @@ -1998,7 +1998,7 @@
     3.4            by (auto simp add: algebra_simps)
     3.5        qed
     3.6        ultimately show "norm (f n x - f n y - (g x - g y)) \<le> e * norm (x - y)"
     3.7 -        by (rule tendsto_ge_const[OF trivial_limit_sequentially])
     3.8 +        by (simp add: tendsto_upperbound)
     3.9      qed
    3.10    qed
    3.11    have "\<forall>x\<in>s. ((\<lambda>n. f n x) \<longlongrightarrow> g x) sequentially \<and> (g has_derivative g' x) (at x within s)"
    3.12 @@ -2667,7 +2667,7 @@
    3.13    qed
    3.14    hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<le> (f x - f c) / (x - c)) (at c within ?A')"
    3.15      by (blast intro: filter_leD at_le)
    3.16 -  ultimately have "f' \<le> (f x - f c) / (x - c)" by (rule tendsto_ge_const)
    3.17 +  ultimately have "f' \<le> (f x - f c) / (x - c)" by (simp add: tendsto_upperbound)
    3.18    thus ?thesis using xc by (simp add: field_simps)
    3.19  next
    3.20    assume xc: "x < c"
    3.21 @@ -2691,7 +2691,7 @@
    3.22    qed
    3.23    hence "eventually (\<lambda>y. (f y - f c) / (y - c) \<ge> (f x - f c) / (x - c)) (at c within ?A')"
    3.24      by (blast intro: filter_leD at_le)
    3.25 -  ultimately have "f' \<ge> (f x - f c) / (x - c)" by (rule tendsto_le_const)
    3.26 +  ultimately have "f' \<ge> (f x - f c) / (x - c)" by (simp add: tendsto_lowerbound)
    3.27    thus ?thesis using xc by (simp add: field_simps)
    3.28  qed simp_all
    3.29  
     4.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Sep 26 07:56:54 2016 +0200
     4.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Wed Sep 28 17:01:01 2016 +0100
     4.3 @@ -1870,7 +1870,7 @@
     4.4    have F_mono: "a \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> F x \<le> F y" for x y
     4.5      using f nonneg by (intro DERIV_nonneg_imp_nondecreasing[of x y F]) (auto intro: order_trans)
     4.6    then have F_le_T: "a \<le> x \<Longrightarrow> F x \<le> T" for x
     4.7 -    by (intro tendsto_le_const[OF _ lim])
     4.8 +    by (intro tendsto_lowerbound[OF lim])
     4.9         (auto simp: trivial_limit_at_top_linorder eventually_at_top_linorder)
    4.10  
    4.11    have "(SUP i::nat. ?f i x) = ?fR x" for x
     5.1 --- a/src/HOL/Analysis/Euclidean_Space.thy	Mon Sep 26 07:56:54 2016 +0200
     5.2 +++ b/src/HOL/Analysis/Euclidean_Space.thy	Wed Sep 28 17:01:01 2016 +0100
     5.3 @@ -93,6 +93,11 @@
     5.4      by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"])
     5.5  qed auto
     5.6  
     5.7 +lemma (in euclidean_space) bchoice_Basis_iff:
     5.8 +  fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
     5.9 +  shows "(\<forall>i\<in>Basis. \<exists>x\<in>A. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. inner x i \<in> A \<and> P i (inner x i))"
    5.10 +by (simp add: choice_Basis_iff Bex_def)
    5.11 +
    5.12  lemma (in euclidean_space) euclidean_representation_setsum_fun:
    5.13      "(\<lambda>x. \<Sum>b\<in>Basis. inner (f x) b *\<^sub>R b) = f"
    5.14    by (rule ext) (simp add: euclidean_representation_setsum)
     6.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Mon Sep 26 07:56:54 2016 +0200
     6.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Wed Sep 28 17:01:01 2016 +0100
     6.3 @@ -1812,13 +1812,13 @@
     6.4    shows   "G x = Gamma x"
     6.5  proof (rule antisym)
     6.6    show "G x \<ge> Gamma x"
     6.7 -  proof (rule tendsto_ge_const)
     6.8 +  proof (rule tendsto_upperbound)
     6.9      from G_lower[of x] show "eventually (\<lambda>n. Gamma_series x n \<le> G x) sequentially"
    6.10        using eventually_ge_at_top[of "1::nat"] x by (auto elim!: eventually_mono)
    6.11    qed (simp_all add: Gamma_series_LIMSEQ)
    6.12  next
    6.13    show "G x \<le> Gamma x"
    6.14 -  proof (rule tendsto_le_const)
    6.15 +  proof (rule tendsto_lowerbound)
    6.16      have "(\<lambda>n. Gamma_series x n * (1 + x / real n)) \<longlonglongrightarrow> Gamma x * (1 + 0)"
    6.17        by (rule tendsto_intros real_tendsto_divide_at_top 
    6.18                 Gamma_series_LIMSEQ filterlim_real_sequentially)+
     7.1 --- a/src/HOL/Deriv.thy	Mon Sep 26 07:56:54 2016 +0200
     7.2 +++ b/src/HOL/Deriv.thy	Wed Sep 28 17:01:01 2016 +0100
     7.3 @@ -1563,12 +1563,12 @@
     7.4      and lim: "(f \<longlongrightarrow> flim) at_bot"
     7.5    shows "flim < f b"
     7.6  proof -
     7.7 -  have "flim \<le> f (b - 1)"
     7.8 -    apply (rule tendsto_ge_const [OF _ lim])
     7.9 -     apply (auto simp: trivial_limit_at_bot_linorder eventually_at_bot_linorder)
    7.10 +  have "\<exists>N. \<forall>n\<le>N. f n \<le> f (b - 1)"
    7.11      apply (rule_tac x="b - 2" in exI)
    7.12      apply (force intro: order.strict_implies_order DERIV_pos_imp_increasing [where f=f] assms)
    7.13      done
    7.14 +  then have "flim \<le> f (b - 1)"
    7.15 +     by (auto simp: trivial_limit_at_bot_linorder eventually_at_bot_linorder tendsto_upperbound [OF lim])
    7.16    also have "\<dots> < f b"
    7.17      by (force intro: DERIV_pos_imp_increasing [where f=f] assms)
    7.18    finally show ?thesis .
     8.1 --- a/src/HOL/Fields.thy	Mon Sep 26 07:56:54 2016 +0200
     8.2 +++ b/src/HOL/Fields.thy	Wed Sep 28 17:01:01 2016 +0100
     8.3 @@ -1192,6 +1192,20 @@
     8.4    finally show ?thesis .
     8.5  qed
     8.6  
     8.7 +text\<open>For creating values between @{term u} and @{term v}.\<close>
     8.8 +lemma scaling_mono:
     8.9 +  assumes "u \<le> v" "0 \<le> r" "r \<le> s"
    8.10 +    shows "u + r * (v - u) / s \<le> v"
    8.11 +proof -
    8.12 +  have "r/s \<le> 1" using assms
    8.13 +    using divide_le_eq_1 by fastforce
    8.14 +  then have "(r/s) * (v - u) \<le> 1 * (v - u)"
    8.15 +    apply (rule mult_right_mono)
    8.16 +    using assms by simp
    8.17 +  then show ?thesis
    8.18 +    by (simp add: field_simps)
    8.19 +qed
    8.20 +
    8.21  end
    8.22  
    8.23  text \<open>Min/max Simplification Rules\<close>
     9.1 --- a/src/HOL/Groups_Big.thy	Mon Sep 26 07:56:54 2016 +0200
     9.2 +++ b/src/HOL/Groups_Big.thy	Wed Sep 28 17:01:01 2016 +0100
     9.3 @@ -47,6 +47,9 @@
     9.4  lemma insert_remove: "finite A \<Longrightarrow> F g (insert x A) = g x \<^bold>* F g (A - {x})"
     9.5    by (cases "x \<in> A") (simp_all add: remove insert_absorb)
     9.6  
     9.7 +lemma insert_if: "finite A \<Longrightarrow> F g (insert x A) = (if x \<in> A then F g A else g x \<^bold>* F g A)"
     9.8 +  by (cases "x \<in> A") (simp_all add: insert_absorb)
     9.9 +
    9.10  lemma neutral: "\<forall>x\<in>A. g x = \<^bold>1 \<Longrightarrow> F g A = \<^bold>1"
    9.11    by (induct A rule: infinite_finite_induct) simp_all
    9.12  
    9.13 @@ -1288,4 +1291,22 @@
    9.14    qed
    9.15  qed
    9.16  
    9.17 +lemma setsum_image_le:
    9.18 +  fixes g :: "'a \<Rightarrow> 'b::ordered_ab_group_add"
    9.19 +  assumes "finite I" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g(f i)"
    9.20 +    shows "setsum g (f ` I) \<le> setsum (g \<circ> f) I"
    9.21 +  using assms
    9.22 +proof induction
    9.23 +  case empty
    9.24 +  then show ?case by auto
    9.25 +next
    9.26 +  case (insert x F) then
    9.27 +  have "setsum g (f ` insert x F) = setsum g (insert (f x) (f ` F))" by simp
    9.28 +  also have "\<dots> \<le> g (f x) + setsum g (f ` F)"
    9.29 +    by (simp add: insert setsum.insert_if)
    9.30 +  also have "\<dots>  \<le> setsum (g \<circ> f) (insert x F)"
    9.31 +    using insert by auto
    9.32 +  finally show ?case .
    9.33 +qed
    9.34 + 
    9.35  end
    10.1 --- a/src/HOL/Library/Extended_Real.thy	Mon Sep 26 07:56:54 2016 +0200
    10.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Sep 28 17:01:01 2016 +0100
    10.3 @@ -3856,7 +3856,7 @@
    10.4    assumes "eventually (\<lambda>x. f x \<ge> 0) F"
    10.5    shows   "((\<lambda>x. inverse (f x)) \<longlongrightarrow> inverse c) F"
    10.6    by (cases "F = bot")
    10.7 -     (auto intro!: tendsto_le_const[of F] assms
    10.8 +     (auto intro!: tendsto_lowerbound assms
    10.9                     continuous_on_tendsto_compose[OF continuous_on_inverse_ereal])
   10.10  
   10.11  
    11.1 --- a/src/HOL/Limits.thy	Mon Sep 26 07:56:54 2016 +0200
    11.2 +++ b/src/HOL/Limits.thy	Wed Sep 28 17:01:01 2016 +0100
    11.3 @@ -2368,7 +2368,7 @@
    11.4    fixes f :: "real \<Rightarrow> real"
    11.5    assumes ev: "b < x" "\<forall> x' \<in> { b <..< x}. 0 \<le> f x'" and "isCont f x"
    11.6    shows "0 \<le> f x"
    11.7 -proof (rule tendsto_le_const)
    11.8 +proof (rule tendsto_lowerbound)
    11.9    show "(f \<longlongrightarrow> f x) (at_left x)"
   11.10      using \<open>isCont f x\<close> by (simp add: filterlim_at_split isCont_def)
   11.11    show "eventually (\<lambda>x. 0 \<le> f x) (at_left x)"
    12.1 --- a/src/HOL/Order_Relation.thy	Mon Sep 26 07:56:54 2016 +0200
    12.2 +++ b/src/HOL/Order_Relation.thy	Wed Sep 28 17:01:01 2016 +0100
    12.3 @@ -397,6 +397,18 @@
    12.4    ultimately show ?thesis unfolding R_def by blast
    12.5  qed
    12.6  
    12.7 +text\<open>A transitive relation is well-founded if all initial segments are finite.\<close>
    12.8 +corollary wf_finite_segments:
    12.9 +  assumes "irrefl r" and "trans r" and "\<And>x. finite {y. (y, x) \<in> r}"
   12.10 +  shows "wf (r)"
   12.11 +proof (clarsimp simp: trans_wf_iff wf_iff_acyclic_if_finite converse_def assms)
   12.12 +  fix a
   12.13 +  have "trans (r \<inter> ({x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r}))"
   12.14 +    using assms unfolding trans_def Field_def by blast
   12.15 +  then show "acyclic (r \<inter> {x. (x, a) \<in> r} \<times> {x. (x, a) \<in> r})"
   12.16 +    using assms acyclic_def assms irrefl_def by fastforce
   12.17 +qed
   12.18 +
   12.19  text \<open>The next lemma is a variation of \<open>wf_eq_minimal\<close> from Wellfounded,
   12.20    allowing one to assume the set included in the field.\<close>
   12.21  
    13.1 --- a/src/HOL/Probability/Helly_Selection.thy	Mon Sep 26 07:56:54 2016 +0200
    13.2 +++ b/src/HOL/Probability/Helly_Selection.thy	Wed Sep 28 17:01:01 2016 +0100
    13.3 @@ -108,7 +108,7 @@
    13.4    moreover have "(\<lambda>n. f (d n) x) \<longlonglongrightarrow> F x" if cts: "continuous (at x) F" for x
    13.5    proof (rule limsup_le_liminf_real)
    13.6      show "limsup (\<lambda>n. f (d n) x) \<le> F x"
    13.7 -    proof (rule tendsto_le_const)
    13.8 +    proof (rule tendsto_lowerbound)
    13.9        show "(F \<longlongrightarrow> ereal (F x)) (at_right x)"
   13.10          using cts unfolding continuous_at_split by (auto simp: continuous_within)
   13.11        show "\<forall>\<^sub>F i in at_right x. limsup (\<lambda>n. f (d n) x) \<le> F i"
   13.12 @@ -128,7 +128,7 @@
   13.13        qed
   13.14      qed simp
   13.15      show "F x \<le> liminf (\<lambda>n. f (d n) x)"
   13.16 -    proof (rule tendsto_ge_const)
   13.17 +    proof (rule tendsto_upperbound)
   13.18        show "(F \<longlongrightarrow> ereal (F x)) (at_left x)"
   13.19          using cts unfolding continuous_at_split by (auto simp: continuous_within)
   13.20        show "\<forall>\<^sub>F i in at_left x. F i \<le> liminf (\<lambda>n. f (d n) x)"
   13.21 @@ -214,7 +214,7 @@
   13.22      have "(\<lambda>k. ?\<mu> k {..b}) \<longlonglongrightarrow> F b"
   13.23        using b(2) lim_F unfolding f_def cdf_def o_def by auto
   13.24      then have "1 - \<epsilon> \<le> F b"
   13.25 -    proof (rule tendsto_le_const[OF sequentially_bot], intro always_eventually allI)
   13.26 +    proof (rule tendsto_lowerbound, intro always_eventually allI)
   13.27        fix k
   13.28        have "1 - \<epsilon> < ?\<mu> k {a<..b}"
   13.29          using ab by auto
   13.30 @@ -222,20 +222,20 @@
   13.31          by (auto intro!: \<mu>.finite_measure_mono)
   13.32        finally show "1 - \<epsilon> \<le> ?\<mu> k {..b}"
   13.33          by (rule less_imp_le)
   13.34 -    qed
   13.35 +    qed (rule sequentially_bot)
   13.36      then show "\<exists>b. \<forall>x\<ge>b. 1 - \<epsilon> \<le> F x"
   13.37        using F unfolding mono_def by (metis order.trans)
   13.38  
   13.39      have "(\<lambda>k. ?\<mu> k {..a}) \<longlonglongrightarrow> F a"
   13.40        using a(2) lim_F unfolding f_def cdf_def o_def by auto
   13.41      then have Fa: "F a \<le> \<epsilon>"
   13.42 -    proof (rule tendsto_ge_const[OF sequentially_bot], intro always_eventually allI)
   13.43 +    proof (rule tendsto_upperbound, intro always_eventually allI)
   13.44        fix k
   13.45        have "?\<mu> k {..a} + ?\<mu> k {a<..b} \<le> 1"
   13.46          by (subst \<mu>.finite_measure_Union[symmetric]) auto
   13.47        then show "?\<mu> k {..a} \<le> \<epsilon>"
   13.48          using ab[of k] by simp
   13.49 -    qed
   13.50 +    qed (rule sequentially_bot)
   13.51      then show "\<exists>a. \<forall>x\<le>a. F x \<le> \<epsilon>"
   13.52        using F unfolding mono_def by (metis order.trans)
   13.53    qed
    14.1 --- a/src/HOL/Probability/Weak_Convergence.thy	Mon Sep 26 07:56:54 2016 +0200
    14.2 +++ b/src/HOL/Probability/Weak_Convergence.thy	Wed Sep 28 17:01:01 2016 +0100
    14.3 @@ -200,7 +200,7 @@
    14.4        using \<omega>(2) by (auto intro: tendsto_within_subset simp: continuous_at)
    14.5      show "limsup (\<lambda>n. \<mu>.I n \<omega>) \<le> M.I \<omega>"
    14.6        using \<omega>
    14.7 -      by (intro tendsto_le_const[OF trivial_limit_at_right_real **])
    14.8 +      by (intro tendsto_lowerbound[OF **])
    14.9           (auto intro!: exI[of _ 1] * simp: eventually_at_right[of _ 1])
   14.10    qed
   14.11  
   14.12 @@ -391,12 +391,12 @@
   14.13    } note ** = this
   14.14  
   14.15    have "limsup (\<lambda>n. cdf (M_seq n) x) \<le> cdf M x"
   14.16 -  proof (rule tendsto_le_const)
   14.17 +  proof (rule tendsto_lowerbound)
   14.18      show "\<forall>\<^sub>F i in at_right x. limsup (\<lambda>xa. ereal (cdf (M_seq xa) x)) \<le> ereal (cdf M i)"
   14.19        by (subst eventually_at_right[of _ "x + 1"]) (auto simp: * intro: exI [of _ "x+1"])
   14.20    qed (insert cdf_is_right_cont, auto simp: continuous_within)
   14.21    moreover have "cdf M x \<le> liminf (\<lambda>n. cdf (M_seq n) x)"
   14.22 -  proof (rule tendsto_ge_const)
   14.23 +  proof (rule tendsto_upperbound)
   14.24      show "\<forall>\<^sub>F i in at_left x. ereal (cdf M i) \<le> liminf (\<lambda>xa. ereal (cdf (M_seq xa) x))"
   14.25        by (subst eventually_at_left[of "x - 1"]) (auto simp: ** intro: exI [of _ "x-1"])
   14.26    qed (insert left_cont, auto simp: continuous_within)
    15.1 --- a/src/HOL/Series.thy	Mon Sep 26 07:56:54 2016 +0200
    15.2 +++ b/src/HOL/Series.thy	Wed Sep 28 17:01:01 2016 +0100
    15.3 @@ -26,12 +26,16 @@
    15.4      (binder "\<Sum>" 10)
    15.5    where "suminf f = (THE s. f sums s)"
    15.6  
    15.7 +text\<open>Variants of the definition\<close>
    15.8  lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
    15.9    apply (simp add: sums_def)
   15.10    apply (subst LIMSEQ_Suc_iff [symmetric])
   15.11    apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
   15.12    done
   15.13  
   15.14 +lemma sums_def_le: "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> s"
   15.15 +  by (simp add: sums_def' atMost_atLeast0)
   15.16 +
   15.17  
   15.18  subsection \<open>Infinite summability on topological monoids\<close>
   15.19  
    16.1 --- a/src/HOL/Set.thy	Mon Sep 26 07:56:54 2016 +0200
    16.2 +++ b/src/HOL/Set.thy	Wed Sep 28 17:01:01 2016 +0100
    16.3 @@ -1858,6 +1858,9 @@
    16.4  definition disjnt :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
    16.5    where "disjnt A B \<longleftrightarrow> A \<inter> B = {}"
    16.6  
    16.7 +lemma disjnt_self_iff_empty [simp]: "disjnt S S \<longleftrightarrow> S = {}"
    16.8 +  by (auto simp: disjnt_def)
    16.9 +
   16.10  lemma disjnt_iff: "disjnt A B \<longleftrightarrow> (\<forall>x. \<not> (x \<in> A \<and> x \<in> B))"
   16.11    by (force simp: disjnt_def)
   16.12  
    17.1 --- a/src/HOL/Topological_Spaces.thy	Mon Sep 26 07:56:54 2016 +0200
    17.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Sep 28 17:01:01 2016 +0100
    17.3 @@ -884,19 +884,19 @@
    17.4      by (simp add: eventually_False)
    17.5  qed
    17.6  
    17.7 -lemma tendsto_le_const:
    17.8 +lemma tendsto_lowerbound:
    17.9    fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
   17.10 -  assumes F: "\<not> trivial_limit F"
   17.11 -    and x: "(f \<longlongrightarrow> x) F"
   17.12 -    and ev: "eventually (\<lambda>i. a \<le> f i) F"
   17.13 +  assumes x: "(f \<longlongrightarrow> x) F"
   17.14 +      and ev: "eventually (\<lambda>i. a \<le> f i) F"
   17.15 +      and F: "\<not> trivial_limit F"
   17.16    shows "a \<le> x"
   17.17    using F x tendsto_const ev by (rule tendsto_le)
   17.18  
   17.19 -lemma tendsto_ge_const:
   17.20 +lemma tendsto_upperbound:
   17.21    fixes f :: "'a \<Rightarrow> 'b::linorder_topology"
   17.22 -  assumes F: "\<not> trivial_limit F"
   17.23 -    and x: "(f \<longlongrightarrow> x) F"
   17.24 -    and ev: "eventually (\<lambda>i. a \<ge> f i) F"
   17.25 +  assumes x: "(f \<longlongrightarrow> x) F"
   17.26 +      and ev: "eventually (\<lambda>i. a \<ge> f i) F"
   17.27 +      and F: "\<not> trivial_limit F"
   17.28    shows "a \<ge> x"
   17.29    by (rule tendsto_le [OF F tendsto_const x ev])
   17.30  
   17.31 @@ -1256,7 +1256,7 @@
   17.32  
   17.33  lemma LIMSEQ_le_const: "X \<longlonglongrightarrow> x \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. a \<le> X n \<Longrightarrow> a \<le> x"
   17.34    for a x :: "'a::linorder_topology"
   17.35 -  using tendsto_le_const[of sequentially X x a] by (simp add: eventually_sequentially)
   17.36 +  by (simp add: eventually_at_top_linorder tendsto_lowerbound)
   17.37  
   17.38  lemma LIMSEQ_le: "X \<longlonglongrightarrow> x \<Longrightarrow> Y \<longlonglongrightarrow> y \<Longrightarrow> \<exists>N. \<forall>n\<ge>N. X n \<le> Y n \<Longrightarrow> x \<le> y"
   17.39    for x y :: "'a::linorder_topology"