--- a/CONTRIBUTORS Fri Jun 29 10:55:05 2018 +0100
+++ b/CONTRIBUTORS Fri Jun 29 11:39:40 2018 +0100
@@ -12,6 +12,9 @@
* June 2018: Martin Baillon and Paulo EmÃlio de Vilhena
A variety of contributions to HOL-Algebra.
+* June 2018: Wenda Li
+ New/strengthened results involving analysis, topology, etc.
+
* May 2018: Manuel Eberl
Landau symbols and asymptotic equivalence (moved from the AFP).
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Fri Jun 29 11:39:40 2018 +0100
@@ -774,7 +774,27 @@
ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
using \<open>finite S\<close> by auto
qed
-
+
+lemma valid_path_uminus_comp[simp]:
+ fixes g::"real \<Rightarrow> 'a ::real_normed_field"
+ shows "valid_path (uminus \<circ> g) \<longleftrightarrow> valid_path g"
+proof
+ show "valid_path g \<Longrightarrow> valid_path (uminus \<circ> g)" for g::"real \<Rightarrow> 'a"
+ by (auto intro!: valid_path_compose derivative_intros simp add: deriv_linear[of "-1",simplified])
+ then show "valid_path g" when "valid_path (uminus \<circ> g)"
+ by (metis fun.map_comp group_add_class.minus_comp_minus id_comp that)
+qed
+
+lemma valid_path_offset[simp]:
+ shows "valid_path (\<lambda>t. g t - z) \<longleftrightarrow> valid_path g"
+proof
+ show *: "valid_path (g::real\<Rightarrow>'a) \<Longrightarrow> valid_path (\<lambda>t. g t - z)" for g z
+ unfolding valid_path_def
+ by (fastforce intro:derivative_intros C1_differentiable_imp_piecewise piecewise_C1_differentiable_diff)
+ show "valid_path (\<lambda>t. g t - z) \<Longrightarrow> valid_path g"
+ using *[of "\<lambda>t. g t - z" "-z",simplified] .
+qed
+
subsection\<open>Contour Integrals along a path\<close>
@@ -3554,6 +3574,19 @@
"(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> p t = q t) \<Longrightarrow> winding_number p z = winding_number q z"
by (simp add: winding_number_def winding_number_prop_def pathstart_def pathfinish_def)
+lemma winding_number_constI:
+ assumes "c\<noteq>z" "\<And>t. \<lbrakk>0\<le>t; t\<le>1\<rbrakk> \<Longrightarrow> g t = c"
+ shows "winding_number g z = 0"
+proof -
+ have "winding_number g z = winding_number (linepath c c) z"
+ apply (rule winding_number_cong)
+ using assms unfolding linepath_def by auto
+ moreover have "winding_number (linepath c c) z =0"
+ apply (rule winding_number_trivial)
+ using assms by auto
+ ultimately show ?thesis by auto
+qed
+
lemma winding_number_offset: "winding_number p z = winding_number (\<lambda>w. p w - z) 0"
unfolding winding_number_def
proof (intro ext arg_cong [where f = Eps] arg_cong [where f = All] imp_cong refl, safe)
@@ -4812,8 +4845,7 @@
winding_number (subpath u w g) z"
apply (rule trans [OF winding_number_join [THEN sym]
winding_number_homotopic_paths [OF homotopic_join_subpaths]])
-apply (auto dest: path_image_subpath_subset)
-done
+ using path_image_subpath_subset by auto
subsection\<open>Partial circle path\<close>
@@ -4829,6 +4861,11 @@
"pathfinish(part_circlepath z r s t) = z + r*exp(\<i>*t)"
by (metis part_circlepath_def pathfinish_def pathfinish_linepath)
+lemma reversepath_part_circlepath[simp]:
+ "reversepath (part_circlepath z r s t) = part_circlepath z r t s"
+ unfolding part_circlepath_def reversepath_def linepath_def
+ by (auto simp:algebra_simps)
+
proposition has_vector_derivative_part_circlepath [derivative_intros]:
"((part_circlepath z r s t) has_vector_derivative
(\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)))
--- a/src/HOL/Analysis/Change_Of_Vars.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Fri Jun 29 11:39:40 2018 +0100
@@ -2937,7 +2937,7 @@
moreover have "integral (g ` S) (h n) \<le> integral S (\<lambda>x. ?D x * f (g x))" for n
using hint by (blast intro: le order_trans)
ultimately show ?thesis
- by (auto intro: Lim_bounded_ereal)
+ by (auto intro: Lim_bounded)
qed
--- a/src/HOL/Analysis/Interval_Integral.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Analysis/Interval_Integral.thy Fri Jun 29 11:39:40 2018 +0100
@@ -875,7 +875,7 @@
using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
hence A3: "\<And>i. g (l i) \<ge> A"
- by (intro decseq_le, auto simp: decseq_def)
+ by (intro decseq_ge, auto simp: decseq_def)
have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
@@ -972,7 +972,7 @@
using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
hence A3: "\<And>i. g (l i) \<ge> A"
- by (intro decseq_le, auto simp: decseq_def)
+ by (intro decseq_ge, auto simp: decseq_def)
have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
--- a/src/HOL/Analysis/Measure_Space.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Fri Jun 29 11:39:40 2018 +0100
@@ -389,7 +389,7 @@
show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
using A by auto
qed
- from INF_Lim_ereal[OF decseq_f this]
+ from INF_Lim[OF decseq_f this]
have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
by auto
@@ -2020,7 +2020,7 @@
finally show ?thesis by simp
qed
ultimately have "emeasure M (\<Union>N. B N) \<le> ennreal (\<Sum>n. measure M (A n))"
- by (simp add: Lim_bounded_ereal)
+ by (simp add: Lim_bounded)
then show "emeasure M (\<Union>n. A n) \<le> (\<Sum>n. measure M (A n))"
unfolding B_def by (metis UN_UN_flatten UN_lessThan_UNIV)
then show "emeasure M (\<Union>n. A n) < \<infinity>"
--- a/src/HOL/Analysis/Path_Connected.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Analysis/Path_Connected.thy Fri Jun 29 11:39:40 2018 +0100
@@ -929,10 +929,10 @@
done
lemma path_image_subpath_subset:
- "\<lbrakk>path g; u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
+ "\<lbrakk>u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost path_image_subpath)
apply (auto simp: path_image_def)
- done
+ done
lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)
@@ -1751,14 +1751,14 @@
by (simp add: path_connected_def)
qed
-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)"
+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)"
apply (intro iffI)
apply (metis path_connected_path_image path_defs(5) pathfinish_in_path_image pathstart_in_path_image)
using path_component_of_subset path_connected_component by blast
lemma path_component_path_component [simp]:
- "path_component_set (path_component_set s x) x = path_component_set s x"
-proof (cases "x \<in> s")
+ "path_component_set (path_component_set S x) x = path_component_set S x"
+proof (cases "x \<in> S")
case True show ?thesis
apply (rule subset_antisym)
apply (simp add: path_component_subset)
@@ -1769,11 +1769,11 @@
qed
lemma path_component_subset_connected_component:
- "(path_component_set s x) \<subseteq> (connected_component_set s x)"
-proof (cases "x \<in> s")
+ "(path_component_set S x) \<subseteq> (connected_component_set S x)"
+proof (cases "x \<in> S")
case True show ?thesis
apply (rule connected_component_maximal)
- apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected path_connected_path_component)
+ apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected)
done
next
case False then show ?thesis
@@ -1784,11 +1784,11 @@
lemma path_connected_linear_image:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- assumes "path_connected s" "bounded_linear f"
- shows "path_connected(f ` s)"
+ assumes "path_connected S" "bounded_linear f"
+ shows "path_connected(f ` S)"
by (auto simp: linear_continuous_on assms path_connected_continuous_image)
-lemma is_interval_path_connected: "is_interval s \<Longrightarrow> path_connected s"
+lemma is_interval_path_connected: "is_interval S \<Longrightarrow> path_connected S"
by (simp add: convex_imp_path_connected is_interval_convex)
lemma linear_homeomorphism_image:
--- a/src/HOL/Analysis/Summation_Tests.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Analysis/Summation_Tests.thy Fri Jun 29 11:39:40 2018 +0100
@@ -752,7 +752,7 @@
assumes lim: "(\<lambda>n. ereal (norm (f n) / norm (f (Suc n)))) \<longlonglongrightarrow> c"
shows "conv_radius f = c"
proof (rule conv_radius_eqI')
- show "c \<ge> 0" by (intro Lim_bounded2_ereal[OF lim]) simp_all
+ show "c \<ge> 0" by (intro Lim_bounded2[OF lim]) simp_all
next
fix r assume r: "0 < r" "ereal r < c"
let ?l = "liminf (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Jun 29 11:39:40 2018 +0100
@@ -2068,32 +2068,45 @@
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
by (auto simp: islimpt_def)
+lemma finite_ball_include:
+ fixes a :: "'a::metric_space"
+ assumes "finite S"
+ shows "\<exists>e>0. S \<subseteq> ball a e"
+ using assms
+proof induction
+ case (insert x S)
+ then obtain e0 where "e0>0" and e0:"S \<subseteq> ball a e0" by auto
+ define e where "e = max e0 (2 * dist a x)"
+ have "e>0" unfolding e_def using \<open>e0>0\<close> by auto
+ moreover have "insert x S \<subseteq> ball a e"
+ using e0 \<open>e>0\<close> unfolding e_def by auto
+ ultimately show ?case by auto
+qed (auto intro: zero_less_one)
+
lemma finite_set_avoid:
fixes a :: "'a::metric_space"
- assumes fS: "finite S"
+ assumes "finite S"
shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
-proof (induct rule: finite_induct[OF fS])
- case 1
- then show ?case by (auto intro: zero_less_one)
-next
- case (2 x F)
- from 2 obtain d where d: "d > 0" "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> d \<le> dist a x"
+ using assms
+proof induction
+ case (insert x S)
+ then obtain d where "d > 0" and d: "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
by blast
show ?case
proof (cases "x = a")
case True
- with d show ?thesis by auto
+ with \<open>d > 0 \<close>d show ?thesis by auto
next
case False
let ?d = "min d (dist a x)"
- from False d(1) have dp: "?d > 0"
+ from False \<open>d > 0\<close> have dp: "?d > 0"
by auto
- from d have d': "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
+ from d have d': "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
by auto
with dp False show ?thesis
- by (auto intro!: exI[where x="?d"])
+ by (metis insert_iff le_less min_less_iff_conj not_less)
qed
-qed
+qed (auto intro: zero_less_one)
lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
by (simp add: islimpt_iff_eventually eventually_conj_iff)
--- a/src/HOL/Computational_Algebra/Polynomial.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Fri Jun 29 11:39:40 2018 +0100
@@ -1832,10 +1832,13 @@
by simp
qed
-(* Next two lemmas contributed by Wenda Li *)
+(* Next three lemmas contributed by Wenda Li *)
lemma order_1_eq_0 [simp]:"order x 1 = 0"
by (metis order_root poly_1 zero_neq_one)
+lemma order_uminus[simp]: "order x (-p) = order x p"
+ by (metis neg_equal_0_iff_equal order_smult smult_1_left smult_minus_left)
+
lemma order_power_n_n: "order a ([:-a,1:]^n)=n"
proof (induct n) (*might be proved more concisely using nat_less_induct*)
case 0
@@ -2575,17 +2578,28 @@
lemma poly_DERIV [simp]: "DERIV (\<lambda>x. poly p x) x :> poly (pderiv p) x"
by (induct p) (auto intro!: derivative_eq_intros simp add: pderiv_pCons)
+lemma poly_isCont[simp]:
+ fixes x::"'a::real_normed_field"
+ shows "isCont (\<lambda>x. poly p x) x"
+by (rule poly_DERIV [THEN DERIV_isCont])
+
+lemma tendsto_poly [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. poly p (f x)) \<longlongrightarrow> poly p a) F"
+ for f :: "_ \<Rightarrow> 'a::real_normed_field"
+ by (rule isCont_tendsto_compose [OF poly_isCont])
+
+lemma continuous_within_poly: "continuous (at z within s) (poly p)"
+ for z :: "'a::{real_normed_field}"
+ by (simp add: continuous_within tendsto_poly)
+
+lemma continuous_poly [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. poly p (f x))"
+ for f :: "_ \<Rightarrow> 'a::real_normed_field"
+ unfolding continuous_def by (rule tendsto_poly)
+
lemma continuous_on_poly [continuous_intros]:
fixes p :: "'a :: {real_normed_field} poly"
assumes "continuous_on A f"
shows "continuous_on A (\<lambda>x. poly p (f x))"
-proof -
- have "continuous_on A (\<lambda>x. (\<Sum>i\<le>degree p. (f x) ^ i * coeff p i))"
- by (intro continuous_intros assms)
- also have "\<dots> = (\<lambda>x. poly p (f x))"
- by (rule ext) (simp add: poly_altdef mult_ac)
- finally show ?thesis .
-qed
+ by (metis DERIV_continuous_on assms continuous_on_compose2 poly_DERIV subset_UNIV)
text \<open>Consequences of the derivative theorem above.\<close>
@@ -2593,10 +2607,6 @@
for x :: real
by (simp add: real_differentiable_def) (blast intro: poly_DERIV)
-lemma poly_isCont[simp]: "isCont (\<lambda>x. poly p x) x"
- for x :: real
- by (rule poly_DERIV [THEN DERIV_isCont])
-
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"
for a b :: real
using IVT_objl [of "poly p" a 0 b] by (auto simp add: order_le_less)
--- a/src/HOL/Library/Extended_Real.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy Fri Jun 29 11:39:40 2018 +0100
@@ -2921,17 +2921,6 @@
lemma Lim_bounded_PInfty2: "f \<longlonglongrightarrow> l \<Longrightarrow> \<forall>n\<ge>N. f n \<le> ereal B \<Longrightarrow> l \<noteq> \<infinity>"
using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
-lemma Lim_bounded_ereal: "f \<longlonglongrightarrow> (l :: 'a::linorder_topology) \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
- by (intro LIMSEQ_le_const2) auto
-
-lemma Lim_bounded2_ereal:
- assumes lim:"f \<longlonglongrightarrow> (l :: 'a::linorder_topology)"
- and ge: "\<forall>n\<ge>N. f n \<ge> C"
- shows "l \<ge> C"
- using ge
- by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
- (auto simp: eventually_sequentially)
-
lemma real_of_ereal_mult[simp]:
fixes a b :: ereal
shows "real_of_ereal (a * b) = real_of_ereal a * real_of_ereal b"
@@ -3341,7 +3330,7 @@
assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
and pos: "\<And>n. 0 \<le> f n"
shows "suminf f \<le> x"
-proof (rule Lim_bounded_ereal)
+proof (rule Lim_bounded)
have "summable f" using pos[THEN summable_ereal_pos] .
then show "(\<lambda>N. \<Sum>n<N. f n) \<longlonglongrightarrow> suminf f"
by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
@@ -3879,66 +3868,6 @@
shows "X \<longlonglongrightarrow> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
by (metis Limsup_MInfty trivial_limit_sequentially)
-lemma ereal_lim_mono:
- fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
- and "X \<longlonglongrightarrow> x"
- and "Y \<longlonglongrightarrow> y"
- shows "x \<le> y"
- using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
-
-lemma incseq_le_ereal:
- fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
- assumes inc: "incseq X"
- and lim: "X \<longlonglongrightarrow> L"
- shows "X N \<le> L"
- using inc
- by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
-
-lemma decseq_ge_ereal:
- assumes dec: "decseq X"
- and lim: "X \<longlonglongrightarrow> (L::'a::linorder_topology)"
- shows "X N \<ge> L"
- using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
-
-lemma bounded_abs:
- fixes a :: real
- assumes "a \<le> x"
- and "x \<le> b"
- shows "\<bar>x\<bar> \<le> max \<bar>a\<bar> \<bar>b\<bar>"
- by (metis abs_less_iff assms leI le_max_iff_disj
- less_eq_real_def less_le_not_le less_minus_iff minus_minus)
-
-lemma ereal_Sup_lim:
- fixes a :: "'a::{complete_linorder,linorder_topology}"
- assumes "\<And>n. b n \<in> s"
- and "b \<longlonglongrightarrow> a"
- shows "a \<le> Sup s"
- by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
-
-lemma ereal_Inf_lim:
- fixes a :: "'a::{complete_linorder,linorder_topology}"
- assumes "\<And>n. b n \<in> s"
- and "b \<longlonglongrightarrow> a"
- shows "Inf s \<le> a"
- by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
-
-lemma SUP_Lim_ereal:
- fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
- assumes inc: "incseq X"
- and l: "X \<longlonglongrightarrow> l"
- shows "(SUP n. X n) = l"
- using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
- by simp
-
-lemma INF_Lim_ereal:
- fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
- assumes dec: "decseq X"
- and l: "X \<longlonglongrightarrow> l"
- shows "(INF n. X n) = l"
- using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
- by simp
-
lemma SUP_eq_LIMSEQ:
assumes "mono f"
shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f \<longlonglongrightarrow> x"
@@ -3949,7 +3878,7 @@
assume "f \<longlonglongrightarrow> x"
then have "(\<lambda>i. ereal (f i)) \<longlonglongrightarrow> ereal x"
by auto
- from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
+ from SUP_Lim[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
next
assume "(SUP n. ereal (f n)) = ereal x"
with LIMSEQ_SUP[OF inc] show "f \<longlonglongrightarrow> x" by auto
--- a/src/HOL/Limits.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Limits.thy Fri Jun 29 11:39:40 2018 +0100
@@ -1347,12 +1347,17 @@
unfolding filterlim_at_bot eventually_at_top_dense
by (metis leI less_minus_iff order_less_asym)
-lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
- by (rule filtermap_fun_inverse[symmetric, of uminus])
- (auto intro: filterlim_uminus_at_bot_at_top filterlim_uminus_at_top_at_bot)
-
-lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)"
- unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident)
+lemma at_bot_mirror :
+ shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top"
+ apply (rule filtermap_fun_inverse[of uminus, symmetric])
+ subgoal unfolding filterlim_at_top eventually_at_bot_linorder using le_minus_iff by auto
+ subgoal unfolding filterlim_at_bot eventually_at_top_linorder using minus_le_iff by auto
+ by auto
+
+lemma at_top_mirror :
+ shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot"
+ apply (subst at_bot_mirror)
+ by (auto simp add: filtermap_filtermap)
lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \<longleftrightarrow> (LIM x at_bot. f (-x::real) :> F)"
unfolding filterlim_def at_top_mirror filtermap_filtermap ..
@@ -2294,7 +2299,7 @@
obtain L where "X \<longlonglongrightarrow> L"
by (auto simp: convergent_def monoseq_def decseq_def)
with \<open>decseq X\<close> show "\<exists>L. X \<longlonglongrightarrow> L \<and> (\<forall>i. L \<le> X i)"
- by (auto intro!: exI[of _ L] decseq_le)
+ by (auto intro!: exI[of _ L] decseq_ge)
qed
--- a/src/HOL/Probability/Distribution_Functions.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Probability/Distribution_Functions.thy Fri Jun 29 11:39:40 2018 +0100
@@ -107,7 +107,7 @@
using \<open>decseq f\<close> unfolding cdf_def
by (intro finite_Lim_measure_decseq) (auto simp: decseq_def)
also have "(\<Inter>i. {.. f i}) = {.. a}"
- using decseq_le[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
+ using decseq_ge[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
finally show "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> cdf M a"
by (simp add: cdf_def)
qed simp
--- a/src/HOL/Real_Vector_Spaces.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Fri Jun 29 11:39:40 2018 +0100
@@ -1092,7 +1092,7 @@
then show ?thesis
by simp
qed
-
+
subclass uniform_space
proof
fix E x
--- a/src/HOL/Topological_Spaces.thy Fri Jun 29 10:55:05 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy Fri Jun 29 11:39:40 2018 +0100
@@ -1109,7 +1109,7 @@
unfolding Lim_def ..
-subsubsection \<open>Monotone sequences and subsequences\<close>
+subsection \<open>Monotone sequences and subsequences\<close>
text \<open>
Definition of monotonicity.
@@ -1132,7 +1132,7 @@
lemma decseq_def: "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
unfolding antimono_def ..
-text \<open>Definition of subsequence.\<close>
+subsubsection \<open>Definition of subsequence.\<close>
(* For compatibility with the old "subseq" *)
lemma strict_mono_leD: "strict_mono r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
@@ -1205,7 +1205,7 @@
qed
-text \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
+subsubsection \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
lemma strict_mono_Suc_iff: "strict_mono f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
proof (intro iffI strict_monoI)
@@ -1351,7 +1351,7 @@
by (rule LIMSEQ_offset [where k="Suc 0"]) simp
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l = f \<longlonglongrightarrow> l"
- by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
+ by (rule filterlim_sequentially_Suc)
lemma LIMSEQ_lessThan_iff_atMost:
shows "(\<lambda>n. f {..<n}) \<longlonglongrightarrow> x \<longleftrightarrow> (\<lambda>n. f {..n}) \<longlonglongrightarrow> x"
@@ -1375,6 +1375,56 @@
for a x :: "'a::linorder_topology"
by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto
+lemma Lim_bounded: "f \<longlonglongrightarrow> l \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
+ for l :: "'a::linorder_topology"
+ by (intro LIMSEQ_le_const2) auto
+
+lemma Lim_bounded2:
+ fixes f :: "nat \<Rightarrow> 'a::linorder_topology"
+ assumes lim:"f \<longlonglongrightarrow> l" and ge: "\<forall>n\<ge>N. f n \<ge> C"
+ shows "l \<ge> C"
+ using ge
+ by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
+ (auto simp: eventually_sequentially)
+
+lemma lim_mono:
+ fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
+ assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
+ and "X \<longlonglongrightarrow> x"
+ and "Y \<longlonglongrightarrow> y"
+ shows "x \<le> y"
+ using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
+
+lemma Sup_lim:
+ fixes a :: "'a::{complete_linorder,linorder_topology}"
+ assumes "\<And>n. b n \<in> s"
+ and "b \<longlonglongrightarrow> a"
+ shows "a \<le> Sup s"
+ by (metis Lim_bounded assms complete_lattice_class.Sup_upper)
+
+lemma Inf_lim:
+ fixes a :: "'a::{complete_linorder,linorder_topology}"
+ assumes "\<And>n. b n \<in> s"
+ and "b \<longlonglongrightarrow> a"
+ shows "Inf s \<le> a"
+ by (metis Lim_bounded2 assms complete_lattice_class.Inf_lower)
+
+lemma SUP_Lim:
+ fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+ assumes inc: "incseq X"
+ and l: "X \<longlonglongrightarrow> l"
+ shows "(SUP n. X n) = l"
+ using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
+ by simp
+
+lemma INF_Lim:
+ fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+ assumes dec: "decseq X"
+ and l: "X \<longlonglongrightarrow> l"
+ shows "(INF n. X n) = l"
+ using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
+ by simp
+
lemma convergentD: "convergent X \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow> L"
by (simp add: convergent_def)
@@ -1417,7 +1467,7 @@
for L :: "'a::linorder_topology"
by (metis incseq_def LIMSEQ_le_const)
-lemma decseq_le: "decseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> L \<le> X n"
+lemma decseq_ge: "decseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> L \<le> X n"
for L :: "'a::linorder_topology"
by (metis decseq_def LIMSEQ_le_const2)