--- a/src/HOL/Analysis/Bochner_Integration.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Bochner_Integration.thy Wed Jul 17 14:02:50 2019 +0100
@@ -610,7 +610,7 @@
proof (safe intro!: has_bochner_integral.intros elim!: has_bochner_integral.cases)
interpret T: bounded_linear T by fact
have [measurable]: "T \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on1 T.continuous_on continuous_on_id)
+ by (intro borel_measurable_continuous_onI T.continuous_on continuous_on_id)
assume [measurable]: "f \<in> borel_measurable M"
then show "(\<lambda>x. T (f x)) \<in> borel_measurable M"
by auto
@@ -2821,7 +2821,7 @@
have "eventually (\<lambda>n. x \<le> X n) sequentially"
unfolding filterlim_at_top_ge[where c=x] by auto
then show "(\<lambda>n. indicator {..X n} x *\<^sub>R f x) \<longlonglongrightarrow> f x"
- by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
+ by (intro tendsto_eventually) (auto split: split_indicator elim!: eventually_mono)
qed
fix n show "AE x in M. norm (indicator {..X n} x *\<^sub>R f x) \<le> norm (f x)"
by (auto split: split_indicator)
--- a/src/HOL/Analysis/Borel_Space.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy Wed Jul 17 14:02:50 2019 +0100
@@ -599,7 +599,7 @@
by (force simp add: sets_restrict_space space_restrict_space)
qed
-lemma borel_measurable_continuous_on1: "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
+lemma borel_measurable_continuous_onI: "continuous_on UNIV f \<Longrightarrow> f \<in> borel_measurable borel"
by (drule borel_measurable_continuous_on_restrict) simp
lemma borel_measurable_continuous_on_if:
@@ -623,7 +623,7 @@
lemma borel_measurable_continuous_on:
assumes f: "continuous_on UNIV f" and g: "g \<in> borel_measurable M"
shows "(\<lambda>x. f (g x)) \<in> borel_measurable M"
- using measurable_comp[OF g borel_measurable_continuous_on1[OF f]] by (simp add: comp_def)
+ using measurable_comp[OF g borel_measurable_continuous_onI[OF f]] by (simp add: comp_def)
lemma borel_measurable_continuous_on_indicator:
fixes f g :: "'a::topological_space \<Rightarrow> 'b::real_normed_vector"
@@ -1332,7 +1332,7 @@
subsection "Borel measurable operators"
lemma borel_measurable_norm[measurable]: "norm \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on1 continuous_intros)
+ by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_sgn [measurable]: "(sgn::'a::real_normed_vector \<Rightarrow> 'a) \<in> borel_measurable borel"
by (rule borel_measurable_continuous_countable_exceptions[where X="{0}"])
@@ -1460,7 +1460,7 @@
lemma borel_measurable_exp[measurable]:
"(exp::'a::{real_normed_field,banach}\<Rightarrow>'a) \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_exp)
+ by (intro borel_measurable_continuous_onI continuous_at_imp_continuous_on ballI isCont_exp)
lemma measurable_real_floor[measurable]:
"(floor :: real \<Rightarrow> int) \<in> measurable borel (count_space UNIV)"
@@ -1479,10 +1479,10 @@
by simp
lemma borel_measurable_root [measurable]: "root n \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on1 continuous_intros)
+ by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_sqrt [measurable]: "sqrt \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on1 continuous_intros)
+ by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_power [measurable (raw)]:
fixes f :: "_ \<Rightarrow> 'b::{power,real_normed_algebra}"
@@ -1491,22 +1491,22 @@
by (intro borel_measurable_continuous_on [OF _ f] continuous_intros)
lemma borel_measurable_Re [measurable]: "Re \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on1 continuous_intros)
+ by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_Im [measurable]: "Im \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on1 continuous_intros)
+ by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_of_real [measurable]: "(of_real :: _ \<Rightarrow> (_::real_normed_algebra)) \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on1 continuous_intros)
+ by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_sin [measurable]: "(sin :: _ \<Rightarrow> (_::{real_normed_field,banach})) \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on1 continuous_intros)
+ by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_cos [measurable]: "(cos :: _ \<Rightarrow> (_::{real_normed_field,banach})) \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on1 continuous_intros)
+ by (intro borel_measurable_continuous_onI continuous_intros)
lemma borel_measurable_arctan [measurable]: "arctan \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on1 continuous_intros)
+ by (intro borel_measurable_continuous_onI continuous_intros)
lemma\<^marker>\<open>tag important\<close> borel_measurable_complex_iff:
"f \<in> borel_measurable M \<longleftrightarrow>
@@ -1692,10 +1692,10 @@
statements are usually done on type classes. \<close>
lemma measurable_enn2ereal[measurable]: "enn2ereal \<in> borel \<rightarrow>\<^sub>M borel"
- by (intro borel_measurable_continuous_on1 continuous_on_enn2ereal)
+ by (intro borel_measurable_continuous_onI continuous_on_enn2ereal)
lemma measurable_e2ennreal[measurable]: "e2ennreal \<in> borel \<rightarrow>\<^sub>M borel"
- by (intro borel_measurable_continuous_on1 continuous_on_e2ennreal)
+ by (intro borel_measurable_continuous_onI continuous_on_e2ennreal)
lemma borel_measurable_enn2real[measurable (raw)]:
"f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> (\<lambda>x. enn2real (f x)) \<in> M \<rightarrow>\<^sub>M borel"
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Wed Jul 17 14:02:50 2019 +0100
@@ -2844,7 +2844,7 @@
by (simp add: Lim_at dist_norm inverse_eq_divide)
show ?thesis
apply (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right)
- apply (rule Lim_transform [OF * Lim_eventually])
+ apply (rule Lim_transform [OF * tendsto_eventually])
using \<open>open S\<close> x apply (force simp: dist_norm open_contains_ball inverse_eq_divide [symmetric] eventually_at)
done
qed
@@ -2948,7 +2948,7 @@
by (simp add: Lim_within dist_norm inverse_eq_divide)
show ?thesis
apply (simp add: has_field_derivative_def has_derivative_within bounded_linear_mult_right)
- apply (rule Lim_transform [OF * Lim_eventually])
+ apply (rule Lim_transform [OF * tendsto_eventually])
using linordered_field_no_ub
apply (force simp: inverse_eq_divide [symmetric] eventually_at)
done
--- a/src/HOL/Analysis/Change_Of_Vars.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Wed Jul 17 14:02:50 2019 +0100
@@ -3402,7 +3402,7 @@
next
show "(\<lambda>k. if x \<in> (\<Union>m\<le>k. g ` F m) then norm (f x) else 0)
\<longlonglongrightarrow> (if x \<in> (\<Union>m. g ` F m) then norm (f x) else 0)" for x
- by (force intro: Lim_eventually eventually_sequentiallyI)
+ by (force intro: tendsto_eventually eventually_sequentiallyI)
qed auto
next
show "(\<lambda>k. if x \<in> (\<Union>m\<le>k. g ` F m) then f x else 0)
@@ -3411,7 +3411,7 @@
fix m y
assume "y \<in> F m"
show "(\<lambda>k. if \<exists>x\<in>{..k}. g y \<in> g ` F x then f (g y) else 0) \<longlonglongrightarrow> f (g y)"
- using \<open>y \<in> F m\<close> by (force intro: Lim_eventually eventually_sequentiallyI [of m])
+ using \<open>y \<in> F m\<close> by (force intro: tendsto_eventually eventually_sequentiallyI [of m])
qed
qed auto
then show fai: "f absolutely_integrable_on (\<Union>m. g ` F m)"
@@ -3483,7 +3483,7 @@
unfolding integral_restrict_UNIV image_UN [symmetric] o_def by simp
next
show "(\<lambda>k. if x \<in> ?U k then norm (?D x) else 0) \<longlonglongrightarrow> (if x \<in> (\<Union>n. F n) then norm (?D x) else 0)" for x
- by (force intro: Lim_eventually eventually_sequentiallyI)
+ by (force intro: tendsto_eventually eventually_sequentiallyI)
qed auto
next
show "(\<lambda>k. if x \<in> ?U k then ?D x else 0) \<longlonglongrightarrow> (if x \<in> (\<Union>n. F n) then ?D x else 0)" for x
@@ -3491,7 +3491,7 @@
fix n
assume "x \<in> F n"
show "(\<lambda>m. if \<exists>j\<in>{..m}. x \<in> F j then ?D x else 0) \<longlonglongrightarrow> ?D x"
- using \<open>x \<in> F n\<close> by (auto intro!: Lim_eventually eventually_sequentiallyI [of n])
+ using \<open>x \<in> F n\<close> by (auto intro!: tendsto_eventually eventually_sequentiallyI [of n])
qed
qed auto
then show Dai: "?D absolutely_integrable_on (\<Union>n. F n)"
--- a/src/HOL/Analysis/Complex_Transcendental.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Wed Jul 17 14:02:50 2019 +0100
@@ -1299,11 +1299,11 @@
lemma continuous_at_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z) Ln"
by (simp add: field_differentiable_imp_continuous_at field_differentiable_within_Ln)
-lemma isCont_Ln' [simp]:
+lemma isCont_Ln' [simp,continuous_intros]:
"\<lbrakk>isCont f z; f z \<notin> \<real>\<^sub>\<le>\<^sub>0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. Ln (f x)) z"
by (blast intro: isCont_o2 [OF _ continuous_at_Ln])
-lemma continuous_within_Ln: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within S) Ln"
+lemma continuous_within_Ln [continuous_intros]: "z \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> continuous (at z within S) Ln"
using continuous_at_Ln continuous_at_imp_continuous_within by blast
lemma continuous_on_Ln [continuous_intros]: "(\<And>z. z \<in> S \<Longrightarrow> z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> continuous_on S Ln"
--- a/src/HOL/Analysis/Conformal_Mappings.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Wed Jul 17 14:02:50 2019 +0100
@@ -1000,7 +1000,7 @@
done
then show ?thesis
apply (simp add: lim_at_infinity_0)
- apply (rule Lim_eventually)
+ apply (rule tendsto_eventually)
apply (simp add: eventually_at)
apply (rule_tac x=r in exI)
apply (simp add: \<open>0 < r\<close> dist_norm)
--- a/src/HOL/Analysis/Derivative.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Derivative.thy Wed Jul 17 14:02:50 2019 +0100
@@ -2340,7 +2340,7 @@
have [tendsto_intros]: "((\<lambda>x. \<Sum>i. ?e i x) \<longlongrightarrow> A) ?F"
by (auto intro!: swap_uniform_limit[where f="\<lambda>n x. \<Sum>i < n. ?e i x" and F = sequentially])
have [tendsto_intros]: "((\<lambda>x. if x = t then 0 else 1) \<longlongrightarrow> 1) ?F"
- by (rule Lim_eventually) (simp add: eventually_at_filter)
+ by (rule tendsto_eventually) (simp add: eventually_at_filter)
have "((\<lambda>y. ((y - t) / abs (y - t)) *\<^sub>R ((\<Sum>n. ?e n y) - A)) \<longlongrightarrow> 0) (at t within T)"
unfolding *
by (rule tendsto_norm_zero_cancel) (auto intro!: tendsto_eq_intros)
--- a/src/HOL/Analysis/Elementary_Topology.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Topology.thy Wed Jul 17 14:02:50 2019 +0100
@@ -1325,9 +1325,6 @@
subsection \<open>Limits\<close>
-lemma Lim_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> (f \<longlongrightarrow> l) net"
- by (rule topological_tendstoI) (auto elim: eventually_mono)
-
text \<open>The expected monotonicity property.\<close>
lemma Lim_Un:
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Jul 17 14:02:50 2019 +0100
@@ -1474,7 +1474,7 @@
have 2: "\<And>k x. indicat_real (\<Union>m\<le>k. S m) x \<le> (indicat_real (\<Union>m\<le>Suc k. S m) x)"
by (simp add: indicator_def)
have 3: "\<And>x. (\<lambda>k. indicat_real (\<Union>m\<le>k. S m) x) \<longlonglongrightarrow> (indicat_real (\<Union>n. S n) x)"
- by (force simp: indicator_def eventually_sequentially intro: Lim_eventually)
+ by (force simp: indicator_def eventually_sequentially intro: tendsto_eventually)
have 4: "bounded (range (\<lambda>k. integral UNIV (indicat_real (\<Union>m\<le>k. S m))))"
by (simp add: 0)
have *: "indicat_real (\<Union>n. S n) integrable_on UNIV \<and>
@@ -1914,7 +1914,7 @@
have 2: "\<And>n x::'a. indicat_real (S n) x \<le> (indicat_real (S (Suc n)) x)"
by (simp add: indicator_leI nest rev_subsetD)
have 3: "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (\<Union>(S ` UNIV)) x)"
- apply (rule Lim_eventually)
+ apply (rule tendsto_eventually)
apply (simp add: indicator_def)
by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
have 4: "bounded (range (\<lambda>n. integral UNIV (indicat_real (S n))))"
@@ -3712,7 +3712,7 @@
show "\<forall>x\<in>UNIV.
(\<lambda>n. if x \<in> (\<Union>m\<le>n. s m) then f x else 0)
\<longlonglongrightarrow> (if x \<in> \<Union>(s ` UNIV) then f x else 0)"
- by (force intro: Lim_eventually eventually_sequentiallyI)
+ by (force intro: tendsto_eventually eventually_sequentiallyI)
qed auto
then show "?F \<longlonglongrightarrow> ?I"
by (simp only: integral_restrict_UNIV)
@@ -3829,7 +3829,7 @@
then have "eventually (\<lambda>n. ?f n x = ?fR x) sequentially"
by (auto intro!: eventually_sequentiallyI[where c=n] split: split_indicator)
then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
- by (rule Lim_eventually)
+ by (rule tendsto_eventually)
qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>lborel)"
by simp
--- a/src/HOL/Analysis/Extended_Real_Limits.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy Wed Jul 17 14:02:50 2019 +0100
@@ -849,7 +849,7 @@
then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
then have "min x n = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
then have "eventually (\<lambda>n. min x n = x) sequentially" using eventually_at_top_linorder by blast
- then show ?thesis by (simp add: Lim_eventually)
+ then show ?thesis by (simp add: tendsto_eventually)
next
case (PInf)
then have "min x n = n" for n::nat by (auto simp add: min_def)
@@ -870,7 +870,7 @@
then have "min x n = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
then have "real_of_ereal(min x n) = r" if "n \<ge> K" for n using real that by auto
then have "eventually (\<lambda>n. real_of_ereal(min x n) = r) sequentially" using eventually_at_top_linorder by blast
- then have "(\<lambda>n. real_of_ereal(min x n)) \<longlonglongrightarrow> r" by (simp add: Lim_eventually)
+ then have "(\<lambda>n. real_of_ereal(min x n)) \<longlonglongrightarrow> r" by (simp add: tendsto_eventually)
then show ?thesis using real by auto
next
case (PInf)
@@ -886,7 +886,7 @@
then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
then have "max x (-real n) = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
then have "eventually (\<lambda>n. max x (-real n) = x) sequentially" using eventually_at_top_linorder by blast
- then show ?thesis by (simp add: Lim_eventually)
+ then show ?thesis by (simp add: tendsto_eventually)
next
case (MInf)
then have "max x (-real n) = (-1)* ereal(real n)" for n::nat by (auto simp add: max_def)
@@ -909,7 +909,7 @@
then have "max x (-real n) = x" if "n \<ge> K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
then have "real_of_ereal(max x (-real n)) = r" if "n \<ge> K" for n using real that by auto
then have "eventually (\<lambda>n. real_of_ereal(max x (-real n)) = r) sequentially" using eventually_at_top_linorder by blast
- then have "(\<lambda>n. real_of_ereal(max x (-real n))) \<longlonglongrightarrow> r" by (simp add: Lim_eventually)
+ then have "(\<lambda>n. real_of_ereal(max x (-real n))) \<longlonglongrightarrow> r" by (simp add: tendsto_eventually)
then show ?thesis using real by auto
next
case (MInf)
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Wed Jul 17 14:02:50 2019 +0100
@@ -1224,7 +1224,7 @@
lemma measurable_product_coordinates [measurable (raw)]:
"(\<lambda>x. x i) \<in> measurable borel borel"
-by (rule borel_measurable_continuous_on1[OF continuous_on_product_coordinates])
+by (rule borel_measurable_continuous_onI[OF continuous_on_product_coordinates])
lemma measurable_product_then_coordinatewise:
fixes f::"'a \<Rightarrow> 'b \<Rightarrow> ('c::topological_space)"
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Wed Jul 17 14:02:50 2019 +0100
@@ -7447,7 +7447,7 @@
by (simp add: filterlim_at_top)
with x have "eventually (\<lambda>n. f n x = x powr e) at_top"
by (auto elim!: eventually_mono simp: f_def)
- thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: Lim_eventually)
+ thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: tendsto_eventually)
next
have "norm (integral {a..} (f n)) \<le> -F a" for n :: nat
proof (cases "n \<ge> a")
--- a/src/HOL/Analysis/Improper_Integral.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Improper_Integral.thy Wed Jul 17 14:02:50 2019 +0100
@@ -1335,7 +1335,7 @@
by (blast intro: equiintegrable_on_subset [OF equiintegrable_closed_interval_restrictions [OF int_f']])
have 2: "(\<lambda>n. if x \<in> cbox (u n) (v n) then if x \<in> S then 0 else f x else 0)
\<longlonglongrightarrow> (if x \<in> cbox c d then if x \<in> S then 0 else f x else 0)" for x
- by (fastforce simp: dest: get_n intro: Lim_eventually eventually_sequentiallyI)
+ by (fastforce simp: dest: get_n intro: tendsto_eventually eventually_sequentiallyI)
have [simp]: "cbox c d \<inter> cbox a b = cbox c d"
using c d by (force simp: mem_box)
have [simp]: "cbox (u n) (v n) \<inter> cbox a b = cbox (u n) (v n)" for n
@@ -1529,7 +1529,7 @@
show "?\<phi> k x \<le> ?\<phi> (Suc k) x" if "x \<in> box a b" for k x
using cb12 box_subset_cbox that by (force simp: intro!: fg)
show "(\<lambda>k. ?\<phi> k x) \<longlonglongrightarrow> g x - f x \<bullet> j" if x: "x \<in> box a b" for x
- proof (rule Lim_eventually)
+ proof (rule tendsto_eventually)
obtain N::nat where N: "\<And>k. k \<ge> N \<Longrightarrow> x \<in> cbox (a + (b - a) /\<^sub>R real k) (b - (b - a) /\<^sub>R real k)"
using getN [OF x] by blast
show "\<forall>\<^sub>F k in sequentially. ?\<phi> k x = g x - f x \<bullet> j"
@@ -1609,7 +1609,7 @@
show "?\<phi> k x \<le> ?\<phi> (Suc k) x" if "x \<in> box a b" for k x
using cb12 box_subset_cbox that by (force simp: intro!: gf)
show "(\<lambda>k. ?\<phi> k x) \<longlonglongrightarrow> f x \<bullet> j - g x" if x: "x \<in> box a b" for x
- proof (rule Lim_eventually)
+ proof (rule tendsto_eventually)
obtain N::nat where N: "\<And>k. k \<ge> N \<Longrightarrow> x \<in> cbox (a + (b - a) /\<^sub>R real k) (b - (b - a) /\<^sub>R real k)"
using getN [OF x] by blast
show "\<forall>\<^sub>F k in sequentially. ?\<phi> k x = f x \<bullet> j - g x"
--- a/src/HOL/Analysis/Infinite_Products.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy Wed Jul 17 14:02:50 2019 +0100
@@ -1673,7 +1673,7 @@
by (force simp add: eventually_sequentially intro: that)
qed
with \<theta>to\<Theta> have "(\<lambda>n. (\<Sum>j\<le>n. Im (Ln (z j)))) \<longlonglongrightarrow> \<Theta> + of_int K * (2*pi)"
- by (simp add: k tendsto_add tendsto_mult Lim_eventually)
+ by (simp add: k tendsto_add tendsto_mult tendsto_eventually)
moreover have "(\<lambda>n. (\<Sum>k\<le>n. Re (Ln (z k)))) \<longlonglongrightarrow> Re (Ln \<xi>)"
using assms continuous_imp_tendsto [OF isCont_ln tendsto_norm [OF L]]
by (simp add: o_def flip: prod_norm ln_prod)
--- a/src/HOL/Analysis/Interval_Integral.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Wed Jul 17 14:02:50 2019 +0100
@@ -518,7 +518,7 @@
then have "eventually (\<lambda>i. f x * indicator {l i..u i} x = f x) sequentially"
by eventually_elim auto }
then show ?thesis
- unfolding approx(1) by (auto intro!: AE_I2 Lim_eventually split: split_indicator)
+ unfolding approx(1) by (auto intro!: AE_I2 tendsto_eventually split: split_indicator)
qed
have 4: "(\<lambda>i. \<integral> x. indicator {l i..u i} x *\<^sub>R f x \<partial>lborel) \<longlonglongrightarrow> C"
using lbint_lim by (simp add: interval_integral_Icc [unfolded set_lebesgue_integral_def] approx less_imp_le)
@@ -556,7 +556,7 @@
show "\<And>i. AE x in lborel. norm (indicator {l i..u i} x *\<^sub>R f x) \<le> norm (indicator (einterval a b) x *\<^sub>R f x)"
by (intro AE_I2) (auto simp: approx split: split_indicator)
show "AE x in lborel. (\<lambda>i. indicator {l i..u i} x *\<^sub>R f x) \<longlonglongrightarrow> indicator (einterval a b) x *\<^sub>R f x"
- proof (intro AE_I2 tendsto_intros Lim_eventually)
+ proof (intro AE_I2 tendsto_intros tendsto_eventually)
fix x
{ fix i assume "l i \<le> x" "x \<le> u i"
with \<open>incseq u\<close>[THEN incseqD, of i] \<open>decseq l\<close>[THEN decseqD, of i]
--- a/src/HOL/Analysis/Riemann_Mapping.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Riemann_Mapping.thy Wed Jul 17 14:02:50 2019 +0100
@@ -576,7 +576,7 @@
(contour_integral (?g z) f - (contour_integral (?g x) f + f x * (z - x))) -
(contour_integral (linepath x z) f - f x * (z - x)) /\<^sub>R norm (z - x))
\<midarrow>x\<rightarrow> 0"
- apply (rule Lim_eventually)
+ apply (rule tendsto_eventually)
apply (simp add: eventually_at)
apply (rule_tac x=d in exI)
using \<open>d > 0\<close> * by simp
--- a/src/HOL/Analysis/Set_Integral.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Analysis/Set_Integral.thy Wed Jul 17 14:02:50 2019 +0100
@@ -397,7 +397,7 @@
then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
using \<open>x \<in> A i\<close> \<open>mono A\<close> by (auto simp: eventually_sequentially mono_def)
show ?thesis
- apply (intro Lim_eventually)
+ apply (intro tendsto_eventually)
using *
apply eventually_elim
apply (auto split: split_indicator)
@@ -1002,7 +1002,7 @@
have "eventually (\<lambda>n. x \<le> X n) sequentially"
unfolding filterlim_at_top_ge[where c=x] by auto
then show "(\<lambda>n. indicator {a..X n} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {a..} x *\<^sub>R f x"
- by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
+ by (intro tendsto_eventually) (auto split: split_indicator elim!: eventually_mono)
qed
fix n show "AE x in M. norm (indicator {a..X n} x *\<^sub>R f x) \<le>
indicator {a..} x *\<^sub>R norm (f x)"
@@ -1039,7 +1039,7 @@
have "eventually (\<lambda>n. x \<ge> X n) sequentially"
unfolding filterlim_at_bot_le[where c=x] by auto
then show "(\<lambda>n. indicator {X n..b} x *\<^sub>R f x) \<longlonglongrightarrow> indicat_real {..b} x *\<^sub>R f x"
- by (intro Lim_eventually) (auto split: split_indicator elim!: eventually_mono)
+ by (intro tendsto_eventually) (auto split: split_indicator elim!: eventually_mono)
qed
fix n show "AE x in M. norm (indicator {X n..b} x *\<^sub>R f x) \<le>
indicator {..b} x *\<^sub>R norm (f x)"
--- a/src/HOL/Archimedean_Field.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Archimedean_Field.thy Wed Jul 17 14:02:50 2019 +0100
@@ -26,18 +26,10 @@
apply (force simp: abs_le_iff bdd_above_def)
done
next
+ have *: "\<And>x. x \<in> S \<Longrightarrow> Inf S \<le> x"
+ by (meson abs_le_iff bdd bdd_below_def cInf_lower minus_le_iff)
show "Sup (uminus ` S) \<le> - Inf S"
- apply (rule cSup_least)
- using \<open>S \<noteq> {}\<close>
- apply force
- apply clarsimp
- apply (rule cInf_lower)
- apply assumption
- using bdd
- apply (simp add: bdd_below_def)
- apply (rule_tac x = "- a" in exI)
- apply force
- done
+ using \<open>S \<noteq> {}\<close> by (force intro: * cSup_least)
qed
with cSup_abs_le [of "uminus ` S"] assms show ?thesis
by fastforce
@@ -754,6 +746,9 @@
finally show "x \<in> \<int>" .
qed (auto simp: frac_def)
+lemma frac_1_eq: "frac (x+1) = frac x"
+ by (simp add: frac_def)
+
subsection \<open>Rounding to the nearest integer\<close>
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Jul 17 14:02:50 2019 +0100
@@ -6117,19 +6117,6 @@
apply simp
done
-lemma nat_induct2: "P 0 \<Longrightarrow> P 1 \<Longrightarrow> (\<And>n. P n \<Longrightarrow> P (n + 2)) \<Longrightarrow> P (n::nat)"
- unfolding One_nat_def numeral_2_eq_2
- apply (induct n rule: nat_less_induct)
- apply (case_tac n)
- apply simp
- apply (rename_tac m)
- apply (case_tac m)
- apply simp
- apply (rename_tac k)
- apply (case_tac k)
- apply simp_all
- done
-
lemma nat_add_1_add_1: "(n::nat) + 1 + 1 = n + 2"
by simp
--- a/src/HOL/Int.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Int.thy Wed Jul 17 14:02:50 2019 +0100
@@ -1154,7 +1154,12 @@
fixes x:: "'a :: linordered_idom"
shows "\<lbrakk>x \<in> Ints; abs x < 1\<rbrakk> \<Longrightarrow> x = 0"
using Ints_nonzero_abs_ge1 [of x] by auto
-
+
+lemma Ints_eq_abs_less1:
+ fixes x:: "'a :: linordered_idom"
+ shows "\<lbrakk>x \<in> Ints; y \<in> Ints\<rbrakk> \<Longrightarrow> x = y \<longleftrightarrow> abs (x-y) < 1"
+ using eq_iff_diff_eq_0 by (fastforce intro: Ints_nonzero_abs_less1)
+
subsection \<open>The functions \<^term>\<open>nat\<close> and \<^term>\<open>int\<close>\<close>
--- a/src/HOL/Library/Discrete.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Library/Discrete.thy Wed Jul 17 14:02:50 2019 +0100
@@ -332,7 +332,8 @@
have "(Discrete.sqrt n)^2 < m^2" by linarith
with power2_less_imp_less have lt_m: "Discrete.sqrt n < m" by blast
from m_def Suc_sqrt_power2_gt[of "n"]
- have "m^2 \<le> (Suc(Discrete.sqrt n))^2" by simp
+ have "m^2 \<le> (Suc(Discrete.sqrt n))^2"
+ by linarith
with power2_nat_le_eq_le have "m \<le> Suc (Discrete.sqrt n)" by blast
with lt_m have "m = Suc (Discrete.sqrt n)" by simp
with lhs m_def show ?thesis by fastforce
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Wed Jul 17 14:02:50 2019 +0100
@@ -148,11 +148,6 @@
"(\<And>x y. mono (F x y)) \<Longrightarrow> mono (\<lambda>z x. INF y \<in> X x. F x y z :: 'a :: complete_lattice)"
by (auto intro!: INF_mono[OF bexI] simp: le_fun_def mono_def)
-lemma continuous_on_max:
- fixes f g :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
- shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. max (f x) (g x))"
- by (auto simp: continuous_on_def intro!: tendsto_max)
-
lemma continuous_on_cmult_ereal:
"\<bar>c::ereal\<bar> \<noteq> \<infinity> \<Longrightarrow> continuous_on A f \<Longrightarrow> continuous_on A (\<lambda>x. c * f x)"
using tendsto_cmult_ereal[of c f "f x" "at x within A" for x]
--- a/src/HOL/Library/Extended_Real.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Library/Extended_Real.thy Wed Jul 17 14:02:50 2019 +0100
@@ -2951,10 +2951,6 @@
thus "((\<lambda>x. ereal (real_of_ereal (f x))) \<longlongrightarrow> 0) F" by (simp add: zero_ereal_def)
qed
-lemma tendsto_explicit:
- "f \<longlonglongrightarrow> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
- unfolding tendsto_def eventually_sequentially by auto
-
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
--- a/src/HOL/Library/Landau_Symbols.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy Wed Jul 17 14:02:50 2019 +0100
@@ -1642,7 +1642,7 @@
subsection \<open>Asymptotic Equivalence\<close>
(* TODO Move *)
-lemma Lim_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
+lemma tendsto_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
named_theorems asymp_equiv_intros
@@ -1775,13 +1775,13 @@
next
case True
with asymp_equiv_eventually_zeros[OF assms] show ?thesis
- by (simp add: Lim_eventually)
+ by (simp add: tendsto_eventually)
qed
lemma asymp_equiv_refl_ev:
assumes "eventually (\<lambda>x. f x = g x) F"
shows "f \<sim>[F] g"
- by (intro asymp_equivI Lim_eventually)
+ by (intro asymp_equivI tendsto_eventually)
(insert assms, auto elim!: eventually_mono)
lemma asymp_equiv_sandwich:
--- a/src/HOL/Limits.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Limits.thy Wed Jul 17 14:02:50 2019 +0100
@@ -779,6 +779,11 @@
for c :: "'a::topological_semigroup_mult"
by (rule tendsto_mult [OF _ tendsto_const])
+lemma lim_const_over_n [tendsto_intros]:
+ fixes a :: "'a::real_normed_field"
+ shows "(\<lambda>n. a / of_nat n) \<longlonglongrightarrow> 0"
+ using tendsto_mult [OF tendsto_const [of a] lim_1_over_n] by simp
+
lemmas continuous_of_real [continuous_intros] =
bounded_linear.continuous [OF bounded_linear_of_real]
--- a/src/HOL/Nat.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Nat.thy Wed Jul 17 14:02:50 2019 +0100
@@ -1863,6 +1863,22 @@
end
+lemma Nats_diff [simp]:
+ fixes a:: "'a::linordered_idom"
+ assumes "a \<in> \<nat>" "b \<in> \<nat>" "b \<le> a" shows "a - b \<in> \<nat>"
+proof -
+ obtain i where i: "a = of_nat i"
+ using Nats_cases assms by blast
+ obtain j where j: "b = of_nat j"
+ using Nats_cases assms by blast
+ have "j \<le> i"
+ using \<open>b \<le> a\<close> i j of_nat_le_iff by blast
+ then have *: "of_nat i - of_nat j = (of_nat (i-j) :: 'a)"
+ by (simp add: of_nat_diff)
+ then show ?thesis
+ by (simp add: * i j)
+qed
+
subsection \<open>Further arithmetic facts concerning the natural numbers\<close>
--- a/src/HOL/NthRoot.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/NthRoot.thy Wed Jul 17 14:02:50 2019 +0100
@@ -226,6 +226,10 @@
lemma real_root_abs: "0 < n \<Longrightarrow> root n \<bar>x\<bar> = \<bar>root n x\<bar>"
by (simp add: abs_if real_root_minus)
+lemma root_abs_power: "n > 0 \<Longrightarrow> abs (root n (y ^n)) = abs y"
+ using root_sgn_power [of n]
+ by (metis abs_ge_zero power_abs real_root_abs real_root_power_cancel)
+
lemma real_root_power: "0 < n \<Longrightarrow> root n (x ^ k) = root n x ^ k"
by (induct k) (simp_all add: real_root_mult)
--- a/src/HOL/Parity.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Parity.thy Wed Jul 17 14:02:50 2019 +0100
@@ -574,6 +574,28 @@
\<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close>
using that by auto
+lemma nat_induct2 [case_names 0 1 step]:
+ assumes "P 0" "P 1" and step: "\<And>n::nat. P n \<Longrightarrow> P (n + 2)"
+ shows "P n"
+proof (induct n rule: less_induct)
+ case (less n)
+ show ?case
+ proof (cases "n < Suc (Suc 0)")
+ case True
+ then show ?thesis
+ using assms by (auto simp: less_Suc_eq)
+ next
+ case False
+ then obtain k where k: "n = Suc (Suc k)"
+ by (force simp: not_less nat_le_iff_add)
+ then have "k<n"
+ by simp
+ with less assms have "P (k+2)"
+ by blast
+ then show ?thesis
+ by (simp add: k)
+ qed
+qed
subsection \<open>Parity and powers\<close>
--- a/src/HOL/Power.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Power.thy Wed Jul 17 14:02:50 2019 +0100
@@ -476,6 +476,10 @@
lemma power_strict_mono [rule_format]: "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n"
by (induct n) (auto simp: mult_strict_mono le_less_trans [of 0 a b])
+lemma power_mono_iff [simp]:
+ shows "\<lbrakk>a \<ge> 0; b \<ge> 0; n>0\<rbrakk> \<Longrightarrow> a ^ n \<le> b ^ n \<longleftrightarrow> a \<le> b"
+ using power_mono [of a b] power_strict_mono [of b a] not_le by auto
+
text\<open>Lemma for \<open>power_strict_decreasing\<close>\<close>
lemma power_Suc_less: "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n"
by (induct n) (auto simp: mult_strict_left_mono)
--- a/src/HOL/Probability/Characteristic_Functions.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Probability/Characteristic_Functions.thy Wed Jul 17 14:02:50 2019 +0100
@@ -91,7 +91,7 @@
qed
lemma (in real_distribution) char_measurable [measurable]: "char M \<in> borel_measurable borel"
- by (auto intro!: borel_measurable_continuous_on1 continuous_at_imp_continuous_on isCont_char)
+ by (auto intro!: borel_measurable_continuous_onI continuous_at_imp_continuous_on isCont_char)
subsection \<open>Independence\<close>
--- a/src/HOL/Probability/Distributions.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Probability/Distributions.thy Wed Jul 17 14:02:50 2019 +0100
@@ -116,7 +116,7 @@
show "?X \<longlonglongrightarrow> (\<integral>\<^sup>+x. ennreal (x^k * exp (-x)) * indicator {0 ..} x \<partial>lborel)"
apply (intro nn_integral_LIMSEQ)
apply (auto simp: incseq_def le_fun_def eventually_sequentially
- split: split_indicator intro!: Lim_eventually)
+ split: split_indicator intro!: tendsto_eventually)
apply (metis nat_ceiling_le_eq)
done
--- a/src/HOL/Probability/Sinc_Integral.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Probability/Sinc_Integral.thy Wed Jul 17 14:02:50 2019 +0100
@@ -138,7 +138,7 @@
by (auto simp: isCont_sinc)
lemma borel_measurable_sinc[measurable]: "sinc \<in> borel_measurable borel"
- by (intro borel_measurable_continuous_on1 continuous_at_imp_continuous_on ballI isCont_sinc)
+ by (intro borel_measurable_continuous_onI continuous_at_imp_continuous_on ballI isCont_sinc)
lemma sinc_AE: "AE x in lborel. sin x / x = sinc x"
by (rule AE_I [where N = "{0}"], auto)
@@ -205,7 +205,7 @@
using DERIV_Si by (rule DERIV_isCont)
lemma borel_measurable_Si[measurable]: "Si \<in> borel_measurable borel"
- by (auto intro: isCont_Si continuous_at_imp_continuous_on borel_measurable_continuous_on1)
+ by (auto intro: isCont_Si continuous_at_imp_continuous_on borel_measurable_continuous_onI)
lemma Si_at_top_LBINT:
"((\<lambda>t. (LBINT x=0..\<infinity>. exp (-(x * t)) * (x * sin t + cos t) / (1 + x^2))) \<longlongrightarrow> 0) at_top"
--- a/src/HOL/Probability/Weak_Convergence.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Probability/Weak_Convergence.thy Wed Jul 17 14:02:50 2019 +0100
@@ -284,7 +284,7 @@
"(\<lambda> n. integral\<^sup>L (\<mu> n) f) \<longlonglongrightarrow> integral\<^sup>L M f"
using assms
by (intro weak_conv_imp_bdd_ae_continuous_conv)
- (auto intro!: borel_measurable_continuous_on1 continuous_at_imp_continuous_on)
+ (auto intro!: borel_measurable_continuous_onI continuous_at_imp_continuous_on)
theorem weak_conv_imp_continuity_set_conv:
fixes f :: "real \<Rightarrow> real"
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy Wed Jul 17 14:02:50 2019 +0100
@@ -4611,7 +4611,7 @@
lemma expands_to_real_imp_filterlim:
assumes "(f expands_to (c :: real)) basis"
shows "(f \<longlongrightarrow> c) at_top"
- using assms by (auto elim!: expands_to.cases simp: eq_commute[of c] Lim_eventually)
+ using assms by (auto elim!: expands_to.cases simp: eq_commute[of c] tendsto_eventually)
lemma expands_to_MSLNil_imp_filterlim:
assumes "(f expands_to MS MSLNil f') basis"
@@ -4620,7 +4620,7 @@
from assms have "eventually (\<lambda>x. f' x = 0) at_top" "eventually (\<lambda>x. f' x = f x) at_top"
by (auto elim!: expands_to.cases is_expansion_aux.cases[of MSLNil])
hence "eventually (\<lambda>x. f x = 0) at_top" by eventually_elim auto
- thus ?thesis by (simp add: Lim_eventually)
+ thus ?thesis by (simp add: tendsto_eventually)
qed
lemma expands_to_neg_exponent_imp_filterlim:
@@ -5193,7 +5193,7 @@
hence "eventually (\<lambda>n. of_nat (f n) = (of_nat c :: 'a)) F"
by eventually_elim simp
thus "filterlim (\<lambda>n. of_nat (f n)) (nhds (of_nat c :: 'a)) F"
- by (rule Lim_eventually)
+ by (rule tendsto_eventually)
qed
lemma tendsto_of_int_iff:
@@ -5210,7 +5210,7 @@
hence "eventually (\<lambda>n. of_int (f n) = (of_int c :: 'a)) F"
by eventually_elim simp
thus "filterlim (\<lambda>n. of_int (f n)) (nhds (of_int c :: 'a)) F"
- by (rule Lim_eventually)
+ by (rule tendsto_eventually)
qed
lemma filterlim_at_top_int_iff_filterlim_real:
--- a/src/HOL/Set_Interval.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Set_Interval.thy Wed Jul 17 14:02:50 2019 +0100
@@ -1995,6 +1995,20 @@
finally show ?thesis .
qed
+lemma in_pairs: "F g {2*m..Suc(2*n)} = F (\<lambda>i. g(2*i) \<^bold>* g(Suc(2*i))) {m..n}"
+proof (induction n)
+ case 0
+ show ?case
+ by (cases "m=0") auto
+next
+ case (Suc n)
+ then show ?case
+ by (auto simp: assoc split: if_split_asm)
+qed
+
+lemma in_pairs_0: "F g {..Suc(2*n)} = F (\<lambda>i. g(2*i) \<^bold>* g(Suc(2*i))) {..n}"
+ using in_pairs [of _ 0 n] by (simp add: atLeast0AtMost)
+
end
lemma sum_natinterval_diff:
--- a/src/HOL/Topological_Spaces.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Topological_Spaces.thy Wed Jul 17 14:02:50 2019 +0100
@@ -782,6 +782,9 @@
lemma tendsto_bot [simp]: "(f \<longlongrightarrow> a) bot"
by (simp add: tendsto_def)
+lemma tendsto_eventually: "eventually (\<lambda>x. f x = l) net \<Longrightarrow> ((\<lambda>x. f x) \<longlongrightarrow> l) net"
+ by (rule topological_tendstoI) (auto elim: eventually_mono)
+
end
lemma (in topological_space) filterlim_within_subset:
@@ -1142,6 +1145,10 @@
lemma lim_def: "lim X = (THE L. X \<longlonglongrightarrow> L)"
unfolding Lim_def ..
+lemma tendsto_explicit:
+ "f \<longlonglongrightarrow> f0 \<longleftrightarrow> (\<forall>S. open S \<longrightarrow> f0 \<in> S \<longrightarrow> (\<exists>N. \<forall>n\<ge>N. f n \<in> S))"
+ unfolding tendsto_def eventually_sequentially by auto
+
subsection \<open>Monotone sequences and subsequences\<close>
@@ -1706,7 +1713,7 @@
lemma LIM_cong: "a = b \<Longrightarrow> (\<And>x. x \<noteq> b \<Longrightarrow> f x = g x) \<Longrightarrow> l = m \<Longrightarrow> (f \<midarrow>a\<rightarrow> l) \<longleftrightarrow> (g \<midarrow>b\<rightarrow> m)"
by (simp add: LIM_equal)
-lemma LIM_cong_limit: "f \<midarrow>x\<rightarrow> L \<Longrightarrow> K = L \<Longrightarrow> f \<midarrow>x\<rightarrow> K"
+lemma tendsto_cong_limit: "(f \<longlongrightarrow> l) F \<Longrightarrow> k = l \<Longrightarrow> (f \<longlongrightarrow> k) F"
by simp
lemma tendsto_at_iff_tendsto_nhds: "g \<midarrow>l\<rightarrow> g l \<longleftrightarrow> (g \<longlongrightarrow> g l) (nhds l)"
@@ -2249,6 +2256,26 @@
for x :: "'a::linorder_topology"
by (simp add: continuous_within filterlim_at_split)
+lemma continuous_on_max [continuous_intros]:
+ fixes f g :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
+ shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. max (f x) (g x))"
+ by (auto simp: continuous_on_def intro!: tendsto_max)
+
+lemma continuous_on_min [continuous_intros]:
+ fixes f g :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
+ shows "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. min (f x) (g x))"
+ by (auto simp: continuous_on_def intro!: tendsto_min)
+
+lemma continuous_max [continuous_intros]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::linorder_topology"
+ shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (max (f x) (g x)))"
+ by (simp add: tendsto_max continuous_def)
+
+lemma continuous_min [continuous_intros]:
+ fixes f :: "'a::t2_space \<Rightarrow> 'b::linorder_topology"
+ shows "\<lbrakk>continuous F f; continuous F g\<rbrakk> \<Longrightarrow> continuous F (\<lambda>x. (min (f x) (g x)))"
+ by (simp add: tendsto_min continuous_def)
+
text \<open>
The following open/closed Collect lemmas are ported from
Sébastien Gouëzel's \<open>Ergodic_Theory\<close>.
--- a/src/HOL/Transcendental.thy Tue Jul 16 15:39:32 2019 +0200
+++ b/src/HOL/Transcendental.thy Wed Jul 17 14:02:50 2019 +0100
@@ -2919,6 +2919,10 @@
lemma powr_half_sqrt: "0 \<le> x \<Longrightarrow> x powr (1/2) = sqrt x"
by (simp add: powr_def root_powr_inverse sqrt_def)
+lemma square_powr_half [simp]:
+ fixes x::real shows "x\<^sup>2 powr (1/2) = \<bar>x\<bar>"
+ by (simp add: powr_half_sqrt)
+
lemma ln_powr_bound: "1 \<le> x \<Longrightarrow> 0 < a \<Longrightarrow> ln x \<le> (x powr a) / a"
for x :: real
by (metis exp_gt_zero linear ln_eq_zero_iff ln_exp ln_less_self ln_powr mult.commute
@@ -4586,7 +4590,7 @@
unfolding continuous_within by (rule tendsto_tan)
lemma LIM_cos_div_sin: "(\<lambda>x. cos(x)/sin(x)) \<midarrow>pi/2\<rightarrow> 0"
- by (rule LIM_cong_limit, (rule tendsto_intros)+, simp_all)
+ by (rule tendsto_cong_limit, (rule tendsto_intros)+, simp_all)
lemma lemma_tan_total:
assumes "0 < y" shows "\<exists>x. 0 < x \<and> x < pi/2 \<and> y < tan x"