merged
authorpaulson
Fri Jun 29 11:39:40 2018 +0100 (11 months ago)
changeset 685337da59435126a
parent 68531 7c6f812afdc4
parent 68532 f8b98d31ad45
child 68534 914e1bc7369a
merged
CONTRIBUTORS
     1.1 --- a/CONTRIBUTORS	Fri Jun 29 10:55:05 2018 +0100
     1.2 +++ b/CONTRIBUTORS	Fri Jun 29 11:39:40 2018 +0100
     1.3 @@ -12,6 +12,9 @@
     1.4  * June 2018: Martin Baillon and Paulo Emílio de Vilhena
     1.5    A variety of contributions to HOL-Algebra.
     1.6  
     1.7 +* June 2018: Wenda Li
     1.8 +  New/strengthened results involving analysis, topology, etc.
     1.9 +
    1.10  * May 2018: Manuel Eberl
    1.11    Landau symbols and asymptotic equivalence (moved from the AFP).
    1.12  
     2.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Jun 29 10:55:05 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Fri Jun 29 11:39:40 2018 +0100
     2.3 @@ -774,7 +774,27 @@
     2.4    ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
     2.5      using \<open>finite S\<close> by auto
     2.6  qed
     2.7 -
     2.8 +  
     2.9 +lemma valid_path_uminus_comp[simp]:
    2.10 +  fixes g::"real \<Rightarrow> 'a ::real_normed_field"
    2.11 +  shows "valid_path (uminus \<circ> g) \<longleftrightarrow> valid_path g"
    2.12 +proof 
    2.13 +  show "valid_path g \<Longrightarrow> valid_path (uminus \<circ> g)" for g::"real \<Rightarrow> 'a"
    2.14 +    by (auto intro!: valid_path_compose derivative_intros simp add: deriv_linear[of "-1",simplified])  
    2.15 +  then show "valid_path g" when "valid_path (uminus \<circ> g)"
    2.16 +    by (metis fun.map_comp group_add_class.minus_comp_minus id_comp that)
    2.17 +qed
    2.18 +
    2.19 +lemma valid_path_offset[simp]:
    2.20 +  shows "valid_path (\<lambda>t. g t - z) \<longleftrightarrow> valid_path g"  
    2.21 +proof 
    2.22 +  show *: "valid_path (g::real\<Rightarrow>'a) \<Longrightarrow> valid_path (\<lambda>t. g t - z)" for g z
    2.23 +    unfolding valid_path_def
    2.24 +    by (fastforce intro:derivative_intros C1_differentiable_imp_piecewise piecewise_C1_differentiable_diff)
    2.25 +  show "valid_path (\<lambda>t. g t - z) \<Longrightarrow> valid_path g"
    2.26 +    using *[of "\<lambda>t. g t - z" "-z",simplified] .
    2.27 +qed
    2.28 +  
    2.29  
    2.30  subsection\<open>Contour Integrals along a path\<close>
    2.31  
    2.32 @@ -3554,6 +3574,19 @@
    2.33     "(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> p t = q t) \<Longrightarrow> winding_number p z = winding_number q z"
    2.34    by (simp add: winding_number_def winding_number_prop_def pathstart_def pathfinish_def)
    2.35  
    2.36 +lemma winding_number_constI:
    2.37 +  assumes "c\<noteq>z" "\<And>t. \<lbrakk>0\<le>t; t\<le>1\<rbrakk> \<Longrightarrow> g t = c" 
    2.38 +  shows "winding_number g z = 0"
    2.39 +proof -
    2.40 +  have "winding_number g z = winding_number (linepath c c) z"
    2.41 +    apply (rule winding_number_cong)
    2.42 +    using assms unfolding linepath_def by auto
    2.43 +  moreover have "winding_number (linepath c c) z =0"
    2.44 +    apply (rule winding_number_trivial)
    2.45 +    using assms by auto
    2.46 +  ultimately show ?thesis by auto
    2.47 +qed
    2.48 +
    2.49  lemma winding_number_offset: "winding_number p z = winding_number (\<lambda>w. p w - z) 0"
    2.50    unfolding winding_number_def
    2.51  proof (intro ext arg_cong [where f = Eps] arg_cong [where f = All] imp_cong refl, safe)
    2.52 @@ -4812,8 +4845,7 @@
    2.53            winding_number (subpath u w g) z"
    2.54  apply (rule trans [OF winding_number_join [THEN sym]
    2.55                        winding_number_homotopic_paths [OF homotopic_join_subpaths]])
    2.56 -apply (auto dest: path_image_subpath_subset)
    2.57 -done
    2.58 +  using path_image_subpath_subset by auto
    2.59  
    2.60  
    2.61  subsection\<open>Partial circle path\<close>
    2.62 @@ -4829,6 +4861,11 @@
    2.63       "pathfinish(part_circlepath z r s t) = z + r*exp(\<i>*t)"
    2.64  by (metis part_circlepath_def pathfinish_def pathfinish_linepath)
    2.65  
    2.66 +lemma reversepath_part_circlepath[simp]:
    2.67 +    "reversepath (part_circlepath z r s t) = part_circlepath z r t s"
    2.68 +  unfolding part_circlepath_def reversepath_def linepath_def 
    2.69 +  by (auto simp:algebra_simps)
    2.70 +    
    2.71  proposition has_vector_derivative_part_circlepath [derivative_intros]:
    2.72      "((part_circlepath z r s t) has_vector_derivative
    2.73        (\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)))
     3.1 --- a/src/HOL/Analysis/Change_Of_Vars.thy	Fri Jun 29 10:55:05 2018 +0100
     3.2 +++ b/src/HOL/Analysis/Change_Of_Vars.thy	Fri Jun 29 11:39:40 2018 +0100
     3.3 @@ -2937,7 +2937,7 @@
     3.4    moreover have "integral (g ` S) (h n) \<le> integral S (\<lambda>x. ?D x * f (g x))" for n
     3.5      using hint by (blast intro: le order_trans)
     3.6    ultimately show ?thesis
     3.7 -    by (auto intro: Lim_bounded_ereal)
     3.8 +    by (auto intro: Lim_bounded)
     3.9  qed
    3.10  
    3.11  
     4.1 --- a/src/HOL/Analysis/Interval_Integral.thy	Fri Jun 29 10:55:05 2018 +0100
     4.2 +++ b/src/HOL/Analysis/Interval_Integral.thy	Fri Jun 29 11:39:40 2018 +0100
     4.3 @@ -875,7 +875,7 @@
     4.4        using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
     4.5        by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
     4.6      hence A3: "\<And>i. g (l i) \<ge> A"
     4.7 -      by (intro decseq_le, auto simp: decseq_def)
     4.8 +      by (intro decseq_ge, auto simp: decseq_def)
     4.9      have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
    4.10        using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
    4.11        by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
    4.12 @@ -972,7 +972,7 @@
    4.13        using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
    4.14        by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
    4.15      hence A3: "\<And>i. g (l i) \<ge> A"
    4.16 -      by (intro decseq_le, auto simp: decseq_def)
    4.17 +      by (intro decseq_ge, auto simp: decseq_def)
    4.18      have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
    4.19        using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
    4.20        by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
     5.1 --- a/src/HOL/Analysis/Measure_Space.thy	Fri Jun 29 10:55:05 2018 +0100
     5.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Fri Jun 29 11:39:40 2018 +0100
     5.3 @@ -389,7 +389,7 @@
     5.4      show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
     5.5        using A by auto
     5.6    qed
     5.7 -  from INF_Lim_ereal[OF decseq_f this]
     5.8 +  from INF_Lim[OF decseq_f this]
     5.9    have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
    5.10    moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
    5.11      by auto
    5.12 @@ -2020,7 +2020,7 @@
    5.13      finally show ?thesis by simp
    5.14    qed
    5.15    ultimately have "emeasure M (\<Union>N. B N) \<le> ennreal (\<Sum>n. measure M (A n))"
    5.16 -    by (simp add: Lim_bounded_ereal)
    5.17 +    by (simp add: Lim_bounded)
    5.18    then show "emeasure M (\<Union>n. A n) \<le> (\<Sum>n. measure M (A n))"
    5.19      unfolding B_def by (metis UN_UN_flatten UN_lessThan_UNIV)
    5.20    then show "emeasure M (\<Union>n. A n) < \<infinity>"
     6.1 --- a/src/HOL/Analysis/Path_Connected.thy	Fri Jun 29 10:55:05 2018 +0100
     6.2 +++ b/src/HOL/Analysis/Path_Connected.thy	Fri Jun 29 11:39:40 2018 +0100
     6.3 @@ -929,10 +929,10 @@
     6.4      done
     6.5  
     6.6  lemma path_image_subpath_subset:
     6.7 -    "\<lbrakk>path g; u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
     6.8 +    "\<lbrakk>u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
     6.9    apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost path_image_subpath)
    6.10    apply (auto simp: path_image_def)
    6.11 -  done
    6.12 +  done  
    6.13  
    6.14  lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
    6.15    by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)
    6.16 @@ -1751,14 +1751,14 @@
    6.17      by (simp add: path_connected_def)
    6.18  qed
    6.19  
    6.20 -lemma path_component: "path_component s x y \<longleftrightarrow> (\<exists>t. path_connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t)"
    6.21 +lemma path_component: "path_component S x y \<longleftrightarrow> (\<exists>t. path_connected t \<and> t \<subseteq> S \<and> x \<in> t \<and> y \<in> t)"
    6.22    apply (intro iffI)
    6.23    apply (metis path_connected_path_image path_defs(5) pathfinish_in_path_image pathstart_in_path_image)
    6.24    using path_component_of_subset path_connected_component by blast
    6.25  
    6.26  lemma path_component_path_component [simp]:
    6.27 -   "path_component_set (path_component_set s x) x = path_component_set s x"
    6.28 -proof (cases "x \<in> s")
    6.29 +   "path_component_set (path_component_set S x) x = path_component_set S x"
    6.30 +proof (cases "x \<in> S")
    6.31    case True show ?thesis
    6.32      apply (rule subset_antisym)
    6.33      apply (simp add: path_component_subset)
    6.34 @@ -1769,11 +1769,11 @@
    6.35  qed
    6.36  
    6.37  lemma path_component_subset_connected_component:
    6.38 -   "(path_component_set s x) \<subseteq> (connected_component_set s x)"
    6.39 -proof (cases "x \<in> s")
    6.40 +   "(path_component_set S x) \<subseteq> (connected_component_set S x)"
    6.41 +proof (cases "x \<in> S")
    6.42    case True show ?thesis
    6.43      apply (rule connected_component_maximal)
    6.44 -    apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected path_connected_path_component)
    6.45 +    apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected)
    6.46      done
    6.47  next
    6.48    case False then show ?thesis
    6.49 @@ -1784,11 +1784,11 @@
    6.50  
    6.51  lemma path_connected_linear_image:
    6.52    fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
    6.53 -  assumes "path_connected s" "bounded_linear f"
    6.54 -    shows "path_connected(f ` s)"
    6.55 +  assumes "path_connected S" "bounded_linear f"
    6.56 +    shows "path_connected(f ` S)"
    6.57  by (auto simp: linear_continuous_on assms path_connected_continuous_image)
    6.58  
    6.59 -lemma is_interval_path_connected: "is_interval s \<Longrightarrow> path_connected s"
    6.60 +lemma is_interval_path_connected: "is_interval S \<Longrightarrow> path_connected S"
    6.61    by (simp add: convex_imp_path_connected is_interval_convex)
    6.62  
    6.63  lemma linear_homeomorphism_image:
     7.1 --- a/src/HOL/Analysis/Summation_Tests.thy	Fri Jun 29 10:55:05 2018 +0100
     7.2 +++ b/src/HOL/Analysis/Summation_Tests.thy	Fri Jun 29 11:39:40 2018 +0100
     7.3 @@ -752,7 +752,7 @@
     7.4    assumes lim: "(\<lambda>n. ereal (norm (f n) / norm (f (Suc n)))) \<longlonglongrightarrow> c"
     7.5    shows   "conv_radius f = c"
     7.6  proof (rule conv_radius_eqI')
     7.7 -  show "c \<ge> 0" by (intro Lim_bounded2_ereal[OF lim]) simp_all
     7.8 +  show "c \<ge> 0" by (intro Lim_bounded2[OF lim]) simp_all
     7.9  next
    7.10    fix r assume r: "0 < r" "ereal r < c"
    7.11    let ?l = "liminf (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))"
     8.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Jun 29 10:55:05 2018 +0100
     8.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Fri Jun 29 11:39:40 2018 +0100
     8.3 @@ -2068,32 +2068,45 @@
     8.4  lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
     8.5    by (auto simp: islimpt_def)
     8.6  
     8.7 +lemma finite_ball_include:
     8.8 +  fixes a :: "'a::metric_space"
     8.9 +  assumes "finite S" 
    8.10 +  shows "\<exists>e>0. S \<subseteq> ball a e"
    8.11 +  using assms
    8.12 +proof induction
    8.13 +  case (insert x S)
    8.14 +  then obtain e0 where "e0>0" and e0:"S \<subseteq> ball a e0" by auto
    8.15 +  define e where "e = max e0 (2 * dist a x)"
    8.16 +  have "e>0" unfolding e_def using \<open>e0>0\<close> by auto
    8.17 +  moreover have "insert x S \<subseteq> ball a e"
    8.18 +    using e0 \<open>e>0\<close> unfolding e_def by auto
    8.19 +  ultimately show ?case by auto
    8.20 +qed (auto intro: zero_less_one)
    8.21 +
    8.22  lemma finite_set_avoid:
    8.23    fixes a :: "'a::metric_space"
    8.24 -  assumes fS: "finite S"
    8.25 +  assumes "finite S"
    8.26    shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
    8.27 -proof (induct rule: finite_induct[OF fS])
    8.28 -  case 1
    8.29 -  then show ?case by (auto intro: zero_less_one)
    8.30 -next
    8.31 -  case (2 x F)
    8.32 -  from 2 obtain d where d: "d > 0" "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> d \<le> dist a x"
    8.33 +  using assms
    8.34 +proof induction
    8.35 +  case (insert x S)
    8.36 +  then obtain d where "d > 0" and d: "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
    8.37      by blast
    8.38    show ?case
    8.39    proof (cases "x = a")
    8.40      case True
    8.41 -    with d show ?thesis by auto
    8.42 +    with \<open>d > 0 \<close>d show ?thesis by auto
    8.43    next
    8.44      case False
    8.45      let ?d = "min d (dist a x)"
    8.46 -    from False d(1) have dp: "?d > 0"
    8.47 +    from False \<open>d > 0\<close> have dp: "?d > 0"
    8.48        by auto
    8.49 -    from d have d': "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
    8.50 +    from d have d': "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
    8.51        by auto
    8.52      with dp False show ?thesis
    8.53 -      by (auto intro!: exI[where x="?d"])
    8.54 +      by (metis insert_iff le_less min_less_iff_conj not_less)
    8.55    qed
    8.56 -qed
    8.57 +qed (auto intro: zero_less_one)
    8.58  
    8.59  lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
    8.60    by (simp add: islimpt_iff_eventually eventually_conj_iff)
     9.1 --- a/src/HOL/Computational_Algebra/Polynomial.thy	Fri Jun 29 10:55:05 2018 +0100
     9.2 +++ b/src/HOL/Computational_Algebra/Polynomial.thy	Fri Jun 29 11:39:40 2018 +0100
     9.3 @@ -1832,10 +1832,13 @@
     9.4      by simp
     9.5  qed
     9.6  
     9.7 -(* Next two lemmas contributed by Wenda Li *)
     9.8 +(* Next three lemmas contributed by Wenda Li *)
     9.9  lemma order_1_eq_0 [simp]:"order x 1 = 0"
    9.10    by (metis order_root poly_1 zero_neq_one)
    9.11  
    9.12 +lemma order_uminus[simp]: "order x (-p) = order x p"
    9.13 +  by (metis neg_equal_0_iff_equal order_smult smult_1_left smult_minus_left) 
    9.14 +
    9.15  lemma order_power_n_n: "order a ([:-a,1:]^n)=n"
    9.16  proof (induct n) (*might be proved more concisely using nat_less_induct*)
    9.17    case 0
    9.18 @@ -2575,17 +2578,28 @@
    9.19  lemma poly_DERIV [simp]: "DERIV (\<lambda>x. poly p x) x :> poly (pderiv p) x"
    9.20    by (induct p) (auto intro!: derivative_eq_intros simp add: pderiv_pCons)
    9.21  
    9.22 +lemma poly_isCont[simp]: 
    9.23 +  fixes x::"'a::real_normed_field"
    9.24 +  shows "isCont (\<lambda>x. poly p x) x"
    9.25 +by (rule poly_DERIV [THEN DERIV_isCont])
    9.26 +
    9.27 +lemma tendsto_poly [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. poly p (f x)) \<longlongrightarrow> poly p a) F"
    9.28 +  for f :: "_ \<Rightarrow> 'a::real_normed_field"  
    9.29 +  by (rule isCont_tendsto_compose [OF poly_isCont])
    9.30 +
    9.31 +lemma continuous_within_poly: "continuous (at z within s) (poly p)"
    9.32 +  for z :: "'a::{real_normed_field}"
    9.33 +  by (simp add: continuous_within tendsto_poly)  
    9.34 +    
    9.35 +lemma continuous_poly [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. poly p (f x))"
    9.36 +  for f :: "_ \<Rightarrow> 'a::real_normed_field"
    9.37 +  unfolding continuous_def by (rule tendsto_poly)
    9.38 +      
    9.39  lemma continuous_on_poly [continuous_intros]:
    9.40    fixes p :: "'a :: {real_normed_field} poly"
    9.41    assumes "continuous_on A f"
    9.42    shows "continuous_on A (\<lambda>x. poly p (f x))"
    9.43 -proof -
    9.44 -  have "continuous_on A (\<lambda>x. (\<Sum>i\<le>degree p. (f x) ^ i * coeff p i))"
    9.45 -    by (intro continuous_intros assms)
    9.46 -  also have "\<dots> = (\<lambda>x. poly p (f x))"
    9.47 -    by (rule ext) (simp add: poly_altdef mult_ac)
    9.48 -  finally show ?thesis .
    9.49 -qed
    9.50 +  by (metis DERIV_continuous_on assms continuous_on_compose2 poly_DERIV subset_UNIV)
    9.51  
    9.52  text \<open>Consequences of the derivative theorem above.\<close>
    9.53  
    9.54 @@ -2593,10 +2607,6 @@
    9.55    for x :: real
    9.56    by (simp add: real_differentiable_def) (blast intro: poly_DERIV)
    9.57  
    9.58 -lemma poly_isCont[simp]: "isCont (\<lambda>x. poly p x) x"
    9.59 -  for x :: real
    9.60 -  by (rule poly_DERIV [THEN DERIV_isCont])
    9.61 -
    9.62  lemma poly_IVT_pos: "a < b \<Longrightarrow> poly p a < 0 \<Longrightarrow> 0 < poly p b \<Longrightarrow> \<exists>x. a < x \<and> x < b \<and> poly p x = 0"
    9.63    for a b :: real
    9.64    using IVT_objl [of "poly p" a 0 b] by (auto simp add: order_le_less)
    10.1 --- a/src/HOL/Library/Extended_Real.thy	Fri Jun 29 10:55:05 2018 +0100
    10.2 +++ b/src/HOL/Library/Extended_Real.thy	Fri Jun 29 11:39:40 2018 +0100
    10.3 @@ -2921,17 +2921,6 @@
    10.4  lemma Lim_bounded_PInfty2: "f \<longlonglongrightarrow> l \<Longrightarrow> \<forall>n\<ge>N. f n \<le> ereal B \<Longrightarrow> l \<noteq> \<infinity>"
    10.5    using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
    10.6  
    10.7 -lemma Lim_bounded_ereal: "f \<longlonglongrightarrow> (l :: 'a::linorder_topology) \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
    10.8 -  by (intro LIMSEQ_le_const2) auto
    10.9 -
   10.10 -lemma Lim_bounded2_ereal:
   10.11 -  assumes lim:"f \<longlonglongrightarrow> (l :: 'a::linorder_topology)"
   10.12 -    and ge: "\<forall>n\<ge>N. f n \<ge> C"
   10.13 -  shows "l \<ge> C"
   10.14 -  using ge
   10.15 -  by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
   10.16 -     (auto simp: eventually_sequentially)
   10.17 -
   10.18  lemma real_of_ereal_mult[simp]:
   10.19    fixes a b :: ereal
   10.20    shows "real_of_ereal (a * b) = real_of_ereal a * real_of_ereal b"
   10.21 @@ -3341,7 +3330,7 @@
   10.22    assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
   10.23      and pos: "\<And>n. 0 \<le> f n"
   10.24    shows "suminf f \<le> x"
   10.25 -proof (rule Lim_bounded_ereal)
   10.26 +proof (rule Lim_bounded)
   10.27    have "summable f" using pos[THEN summable_ereal_pos] .
   10.28    then show "(\<lambda>N. \<Sum>n<N. f n) \<longlonglongrightarrow> suminf f"
   10.29      by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
   10.30 @@ -3879,66 +3868,6 @@
   10.31    shows "X \<longlonglongrightarrow> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
   10.32    by (metis Limsup_MInfty trivial_limit_sequentially)
   10.33  
   10.34 -lemma ereal_lim_mono:
   10.35 -  fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
   10.36 -  assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
   10.37 -    and "X \<longlonglongrightarrow> x"
   10.38 -    and "Y \<longlonglongrightarrow> y"
   10.39 -  shows "x \<le> y"
   10.40 -  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
   10.41 -
   10.42 -lemma incseq_le_ereal:
   10.43 -  fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
   10.44 -  assumes inc: "incseq X"
   10.45 -    and lim: "X \<longlonglongrightarrow> L"
   10.46 -  shows "X N \<le> L"
   10.47 -  using inc
   10.48 -  by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
   10.49 -
   10.50 -lemma decseq_ge_ereal:
   10.51 -  assumes dec: "decseq X"
   10.52 -    and lim: "X \<longlonglongrightarrow> (L::'a::linorder_topology)"
   10.53 -  shows "X N \<ge> L"
   10.54 -  using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
   10.55 -
   10.56 -lemma bounded_abs:
   10.57 -  fixes a :: real
   10.58 -  assumes "a \<le> x"
   10.59 -    and "x \<le> b"
   10.60 -  shows "\<bar>x\<bar> \<le> max \<bar>a\<bar> \<bar>b\<bar>"
   10.61 -  by (metis abs_less_iff assms leI le_max_iff_disj
   10.62 -    less_eq_real_def less_le_not_le less_minus_iff minus_minus)
   10.63 -
   10.64 -lemma ereal_Sup_lim:
   10.65 -  fixes a :: "'a::{complete_linorder,linorder_topology}"
   10.66 -  assumes "\<And>n. b n \<in> s"
   10.67 -    and "b \<longlonglongrightarrow> a"
   10.68 -  shows "a \<le> Sup s"
   10.69 -  by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
   10.70 -
   10.71 -lemma ereal_Inf_lim:
   10.72 -  fixes a :: "'a::{complete_linorder,linorder_topology}"
   10.73 -  assumes "\<And>n. b n \<in> s"
   10.74 -    and "b \<longlonglongrightarrow> a"
   10.75 -  shows "Inf s \<le> a"
   10.76 -  by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
   10.77 -
   10.78 -lemma SUP_Lim_ereal:
   10.79 -  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   10.80 -  assumes inc: "incseq X"
   10.81 -    and l: "X \<longlonglongrightarrow> l"
   10.82 -  shows "(SUP n. X n) = l"
   10.83 -  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
   10.84 -  by simp
   10.85 -
   10.86 -lemma INF_Lim_ereal:
   10.87 -  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   10.88 -  assumes dec: "decseq X"
   10.89 -    and l: "X \<longlonglongrightarrow> l"
   10.90 -  shows "(INF n. X n) = l"
   10.91 -  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
   10.92 -  by simp
   10.93 -
   10.94  lemma SUP_eq_LIMSEQ:
   10.95    assumes "mono f"
   10.96    shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f \<longlonglongrightarrow> x"
   10.97 @@ -3949,7 +3878,7 @@
   10.98      assume "f \<longlonglongrightarrow> x"
   10.99      then have "(\<lambda>i. ereal (f i)) \<longlonglongrightarrow> ereal x"
  10.100        by auto
  10.101 -    from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
  10.102 +    from SUP_Lim[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
  10.103    next
  10.104      assume "(SUP n. ereal (f n)) = ereal x"
  10.105      with LIMSEQ_SUP[OF inc] show "f \<longlonglongrightarrow> x" by auto
    11.1 --- a/src/HOL/Limits.thy	Fri Jun 29 10:55:05 2018 +0100
    11.2 +++ b/src/HOL/Limits.thy	Fri Jun 29 11:39:40 2018 +0100
    11.3 @@ -1347,12 +1347,17 @@
    11.4    unfolding filterlim_at_bot eventually_at_top_dense
    11.5    by (metis leI less_minus_iff order_less_asym)
    11.6  
    11.7 -lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
    11.8 -  by (rule filtermap_fun_inverse[symmetric, of uminus])
    11.9 -     (auto intro: filterlim_uminus_at_bot_at_top filterlim_uminus_at_top_at_bot)
   11.10 -
   11.11 -lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)"
   11.12 -  unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident)
   11.13 +lemma at_bot_mirror : 
   11.14 +  shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top" 
   11.15 +  apply (rule filtermap_fun_inverse[of uminus, symmetric])
   11.16 +  subgoal unfolding filterlim_at_top eventually_at_bot_linorder using le_minus_iff by auto
   11.17 +  subgoal unfolding filterlim_at_bot eventually_at_top_linorder using minus_le_iff by auto
   11.18 +  by auto
   11.19 +
   11.20 +lemma at_top_mirror : 
   11.21 +  shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot"  
   11.22 +  apply (subst at_bot_mirror)
   11.23 +  by (auto simp add: filtermap_filtermap)
   11.24  
   11.25  lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \<longleftrightarrow> (LIM x at_bot. f (-x::real) :> F)"
   11.26    unfolding filterlim_def at_top_mirror filtermap_filtermap ..
   11.27 @@ -2294,7 +2299,7 @@
   11.28    obtain L where "X \<longlonglongrightarrow> L"
   11.29      by (auto simp: convergent_def monoseq_def decseq_def)
   11.30    with \<open>decseq X\<close> show "\<exists>L. X \<longlonglongrightarrow> L \<and> (\<forall>i. L \<le> X i)"
   11.31 -    by (auto intro!: exI[of _ L] decseq_le)
   11.32 +    by (auto intro!: exI[of _ L] decseq_ge)
   11.33  qed
   11.34  
   11.35  
    12.1 --- a/src/HOL/Probability/Distribution_Functions.thy	Fri Jun 29 10:55:05 2018 +0100
    12.2 +++ b/src/HOL/Probability/Distribution_Functions.thy	Fri Jun 29 11:39:40 2018 +0100
    12.3 @@ -107,7 +107,7 @@
    12.4      using \<open>decseq f\<close> unfolding cdf_def
    12.5      by (intro finite_Lim_measure_decseq) (auto simp: decseq_def)
    12.6    also have "(\<Inter>i. {.. f i}) = {.. a}"
    12.7 -    using decseq_le[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
    12.8 +    using decseq_ge[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
    12.9    finally show "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> cdf M a"
   12.10      by (simp add: cdf_def)
   12.11  qed simp
    13.1 --- a/src/HOL/Real_Vector_Spaces.thy	Fri Jun 29 10:55:05 2018 +0100
    13.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Fri Jun 29 11:39:40 2018 +0100
    13.3 @@ -1092,7 +1092,7 @@
    13.4    then show ?thesis
    13.5      by simp
    13.6  qed
    13.7 -
    13.8 +  
    13.9  subclass uniform_space
   13.10  proof
   13.11    fix E x
    14.1 --- a/src/HOL/Topological_Spaces.thy	Fri Jun 29 10:55:05 2018 +0100
    14.2 +++ b/src/HOL/Topological_Spaces.thy	Fri Jun 29 11:39:40 2018 +0100
    14.3 @@ -1109,7 +1109,7 @@
    14.4    unfolding Lim_def ..
    14.5  
    14.6  
    14.7 -subsubsection \<open>Monotone sequences and subsequences\<close>
    14.8 +subsection \<open>Monotone sequences and subsequences\<close>
    14.9  
   14.10  text \<open>
   14.11    Definition of monotonicity.
   14.12 @@ -1132,7 +1132,7 @@
   14.13  lemma decseq_def: "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
   14.14    unfolding antimono_def ..
   14.15  
   14.16 -text \<open>Definition of subsequence.\<close>
   14.17 +subsubsection \<open>Definition of subsequence.\<close>
   14.18  
   14.19  (* For compatibility with the old "subseq" *)
   14.20  lemma strict_mono_leD: "strict_mono r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
   14.21 @@ -1205,7 +1205,7 @@
   14.22  qed
   14.23  
   14.24  
   14.25 -text \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
   14.26 +subsubsection \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
   14.27  
   14.28  lemma strict_mono_Suc_iff: "strict_mono f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
   14.29  proof (intro iffI strict_monoI)
   14.30 @@ -1351,7 +1351,7 @@
   14.31    by (rule LIMSEQ_offset [where k="Suc 0"]) simp
   14.32  
   14.33  lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l = f \<longlonglongrightarrow> l"
   14.34 -  by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
   14.35 +  by (rule filterlim_sequentially_Suc)
   14.36  
   14.37  lemma LIMSEQ_lessThan_iff_atMost:
   14.38    shows "(\<lambda>n. f {..<n}) \<longlonglongrightarrow> x \<longleftrightarrow> (\<lambda>n. f {..n}) \<longlonglongrightarrow> x"
   14.39 @@ -1375,6 +1375,56 @@
   14.40    for a x :: "'a::linorder_topology"
   14.41    by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto
   14.42  
   14.43 +lemma Lim_bounded: "f \<longlonglongrightarrow> l \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
   14.44 +  for l :: "'a::linorder_topology"
   14.45 +  by (intro LIMSEQ_le_const2) auto
   14.46 +
   14.47 +lemma Lim_bounded2:
   14.48 +  fixes f :: "nat \<Rightarrow> 'a::linorder_topology"
   14.49 +  assumes lim:"f \<longlonglongrightarrow> l" and ge: "\<forall>n\<ge>N. f n \<ge> C"
   14.50 +  shows "l \<ge> C"
   14.51 +  using ge
   14.52 +  by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
   14.53 +     (auto simp: eventually_sequentially)
   14.54 +
   14.55 +lemma lim_mono:
   14.56 +  fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
   14.57 +  assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
   14.58 +    and "X \<longlonglongrightarrow> x"
   14.59 +    and "Y \<longlonglongrightarrow> y"
   14.60 +  shows "x \<le> y"
   14.61 +  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
   14.62 +
   14.63 +lemma Sup_lim:
   14.64 +  fixes a :: "'a::{complete_linorder,linorder_topology}"
   14.65 +  assumes "\<And>n. b n \<in> s"
   14.66 +    and "b \<longlonglongrightarrow> a"
   14.67 +  shows "a \<le> Sup s"
   14.68 +  by (metis Lim_bounded assms complete_lattice_class.Sup_upper)
   14.69 +
   14.70 +lemma Inf_lim:
   14.71 +  fixes a :: "'a::{complete_linorder,linorder_topology}"
   14.72 +  assumes "\<And>n. b n \<in> s"
   14.73 +    and "b \<longlonglongrightarrow> a"
   14.74 +  shows "Inf s \<le> a"
   14.75 +  by (metis Lim_bounded2 assms complete_lattice_class.Inf_lower)
   14.76 +
   14.77 +lemma SUP_Lim:
   14.78 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   14.79 +  assumes inc: "incseq X"
   14.80 +    and l: "X \<longlonglongrightarrow> l"
   14.81 +  shows "(SUP n. X n) = l"
   14.82 +  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
   14.83 +  by simp
   14.84 +
   14.85 +lemma INF_Lim:
   14.86 +  fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   14.87 +  assumes dec: "decseq X"
   14.88 +    and l: "X \<longlonglongrightarrow> l"
   14.89 +  shows "(INF n. X n) = l"
   14.90 +  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
   14.91 +  by simp
   14.92 +
   14.93  lemma convergentD: "convergent X \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow> L"
   14.94    by (simp add: convergent_def)
   14.95  
   14.96 @@ -1417,7 +1467,7 @@
   14.97    for L :: "'a::linorder_topology"
   14.98    by (metis incseq_def LIMSEQ_le_const)
   14.99  
  14.100 -lemma decseq_le: "decseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> L \<le> X n"
  14.101 +lemma decseq_ge: "decseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> L \<le> X n"
  14.102    for L :: "'a::linorder_topology"
  14.103    by (metis decseq_def LIMSEQ_le_const2)
  14.104