--- a/src/HOL/Analysis/Harmonic_Numbers.thy Thu Aug 27 17:15:33 2020 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy Fri Aug 28 12:04:53 2020 +0100
@@ -445,8 +445,8 @@
note sums = ln_series_quadratic[OF x(1)]
define c where "c = inverse (2*y^(2*n+1))"
let ?d = "c * (ln x - (\<Sum>k<n. ?f k))"
- have "\<forall>k. y\<^sup>2^k / of_nat (2*(k+n)+1) \<le> y\<^sup>2 ^ k / of_nat (2*n+1)"
- by (intro allI divide_left_mono mult_right_mono mult_pos_pos zero_le_power[of "y^2"]) simp_all
+ have "\<And>k. y\<^sup>2^k / of_nat (2*(k+n)+1) \<le> y\<^sup>2 ^ k / of_nat (2*n+1)"
+ by (intro divide_left_mono mult_right_mono mult_pos_pos zero_le_power[of "y^2"]) simp_all
moreover {
have "(\<lambda>k. ?f (k + n)) sums (ln x - (\<Sum>k<n. ?f k))"
using sums_split_initial_segment[OF sums] by (simp add: y_def)
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Thu Aug 27 17:15:33 2020 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Fri Aug 28 12:04:53 2020 +0100
@@ -77,7 +77,7 @@
using compact_continuous_image compact_imp_bounded contf by blast
then obtain M where M: "\<And>x. 0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> \<bar>f x\<bar> \<le> M"
by (force simp add: bounded_iff)
- then have Mge0: "0 \<le> M" by force
+ then have "0 \<le> M" by force
have ucontf: "uniformly_continuous_on {0..1} f"
using compact_uniformly_continuous contf by blast
then obtain d where d: "d>0" "\<And>x x'. \<lbrakk> x \<in> {0..1}; x' \<in> {0..1}; \<bar>x' - x\<bar> < d\<rbrakk> \<Longrightarrow> \<bar>f x' - f x\<bar> < e/2"
@@ -124,20 +124,20 @@
then have "\<bar>(f x - f (k/n))\<bar> < e/2"
using d x kn by (simp add: abs_minus_commute)
also have "... \<le> (e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2)"
- using Mge0 d by simp
+ using \<open>M\<ge>0\<close> d by simp
finally show ?thesis by simp
next
case ged
then have dle: "d\<^sup>2 \<le> (x - k/n)\<^sup>2"
by (metis d(1) less_eq_real_def power2_abs power_mono)
+ have \<section>: "1 \<le> (x - real k / real n)\<^sup>2 / d\<^sup>2"
+ using dle \<open>d>0\<close> by auto
have "\<bar>(f x - f (k/n))\<bar> \<le> \<bar>f x\<bar> + \<bar>f (k/n)\<bar>"
by (rule abs_triangle_ineq4)
also have "... \<le> M+M"
by (meson M add_mono_thms_linordered_semiring(1) kn x)
also have "... \<le> 2 * M * ((x - k/n)\<^sup>2 / d\<^sup>2)"
- apply simp
- apply (rule Rings.ordered_semiring_class.mult_left_mono [of 1 "((x - k/n)\<^sup>2 / d\<^sup>2)", simplified])
- using dle \<open>d>0\<close> \<open>M\<ge>0\<close> by auto
+ using \<section> \<open>M\<ge>0\<close> mult_left_mono by fastforce
also have "... \<le> e/2 + 2 * M / d\<^sup>2 * (x - k/n)\<^sup>2"
using e by simp
finally show ?thesis .
@@ -145,19 +145,16 @@
} note * = this
have "\<bar>f x - (\<Sum>k\<le>n. f(k / n) * Bernstein n k x)\<bar> \<le> \<bar>\<Sum>k\<le>n. (f x - f(k / n)) * Bernstein n k x\<bar>"
by (simp add: sum_subtractf sum_distrib_left [symmetric] algebra_simps)
+ also have "... \<le> (\<Sum>k\<le>n. \<bar>(f x - f(k / n)) * Bernstein n k x\<bar>)"
+ by (rule sum_abs)
also have "... \<le> (\<Sum>k\<le>n. (e/2 + (2 * M / d\<^sup>2) * (x - k / n)\<^sup>2) * Bernstein n k x)"
- apply (rule order_trans [OF sum_abs sum_mono])
using *
- apply (simp add: abs_mult Bernstein_nonneg x mult_right_mono)
- done
+ by (force simp add: abs_mult Bernstein_nonneg x mult_right_mono intro: sum_mono)
also have "... \<le> e/2 + (2 * M) / (d\<^sup>2 * n)"
- apply (simp only: sum.distrib Rings.semiring_class.distrib_right sum_distrib_left [symmetric] mult.assoc sum_bern)
- using \<open>d>0\<close> x
- apply (simp add: divide_simps Mge0 mult_le_one mult_left_le)
- done
+ unfolding sum.distrib Rings.semiring_class.distrib_right sum_distrib_left [symmetric] mult.assoc sum_bern
+ using \<open>d>0\<close> x by (simp add: divide_simps \<open>M\<ge>0\<close> mult_le_one mult_left_le)
also have "... < e"
- apply (simp add: field_simps)
- using \<open>d>0\<close> nbig e \<open>n>0\<close>
+ using \<open>d>0\<close> nbig e \<open>n>0\<close>
apply (simp add: field_split_simps)
using ed0 by linarith
finally have "\<bar>f x - (\<Sum>k\<le>n. f (real k / real n) * Bernstein n k x)\<bar> < e" .
@@ -204,10 +201,14 @@
definition\<^marker>\<open>tag important\<close> normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real"
where "normf f \<equiv> SUP x\<in>S. \<bar>f x\<bar>"
- lemma normf_upper: "\<lbrakk>continuous_on S f; x \<in> S\<rbrakk> \<Longrightarrow> \<bar>f x\<bar> \<le> normf f"
- apply (simp add: normf_def)
- apply (rule cSUP_upper, assumption)
- by (simp add: bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs)
+ lemma normf_upper:
+ assumes "continuous_on S f" "x \<in> S" shows "\<bar>f x\<bar> \<le> normf f"
+ proof -
+ have "bdd_above ((\<lambda>x. \<bar>f x\<bar>) ` S)"
+ by (simp add: assms(1) bounded_imp_bdd_above compact compact_continuous_image compact_imp_bounded continuous_on_rabs)
+ then show ?thesis
+ using assms cSUP_upper normf_def by fastforce
+ qed
lemma normf_least: "S \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<le> M) \<Longrightarrow> normf f \<le> M"
by (simp add: normf_def cSUP_least)
@@ -371,11 +372,10 @@
also have "... \<le> (1/(k * (p t))^n) * (1 - p t ^ n) ^ (k^n) * (1 + k^n * (p t)^n)"
using pt_pos [OF t] \<open>k>0\<close>
apply simp
- apply (simp only: times_divide_eq_right [symmetric])
+ apply (simp flip: times_divide_eq_right)
apply (rule mult_left_mono [of "1::real", simplified])
- apply (simp_all add: power_mult_distrib)
- apply (rule zero_le_power)
- using ptn_le by linarith
+ apply (simp_all add: power_mult_distrib ptn_le)
+ done
also have "... \<le> (1/(k * (p t))^n) * (1 - p t ^ n) ^ (k^n) * (1 + (p t)^n) ^ (k^n)"
apply (rule mult_left_mono [OF Bernoulli_inequality [of "p t ^ n" "k^n"]])
using \<open>k>0\<close> ptn_pos ptn_le
@@ -398,12 +398,15 @@
have NN: "of_nat (NN e) > ln e / ln (real k * \<delta> / 2)" "of_nat (NN e) > - ln e / ln (real k * \<delta>)"
if "0<e" for e
unfolding NN_def by linarith+
- have NN1: "\<And>e. e>0 \<Longrightarrow> (k * \<delta> / 2)^NN e < e"
- apply (subst Transcendental.ln_less_cancel_iff [symmetric])
- prefer 3 apply (subst ln_realpow)
- using \<open>k>0\<close> \<open>\<delta>>0\<close> NN k\<delta>
- apply (force simp add: field_simps)+
- done
+ have NN1: "(k * \<delta> / 2)^NN e < e" if "e>0" for e
+ proof -
+ have "ln ((real k * \<delta> / 2) ^ NN e) < ln e"
+ apply (subst ln_realpow)
+ using NN k\<delta> that
+ by (force simp add: field_simps)+
+ then show ?thesis
+ by (simp add: \<open>\<delta>>0\<close> \<open>0 < k\<close> that)
+ qed
have NN0: "(1/(k*\<delta>)) ^ (NN e) < e" if "e>0" for e
proof -
have "0 < ln (real k) + ln \<delta>"
@@ -483,15 +486,11 @@
have pff01: "pff x \<in> {0..1}" if t: "x \<in> S" for x
proof -
have "0 \<le> pff x"
- using subA cardp t
- apply (simp add: pff_def field_split_simps sum_nonneg)
- apply (rule Groups_Big.linordered_semidom_class.prod_nonneg)
- using ff by fastforce
+ using subA cardp t ff
+ by (fastforce simp: pff_def field_split_simps sum_nonneg intro: prod_nonneg)
moreover have "pff x \<le> 1"
- using subA cardp t
- apply (simp add: pff_def field_split_simps sum_nonneg)
- apply (rule prod_mono [where g = "\<lambda>x. 1", simplified])
- using ff by fastforce
+ using subA cardp t ff
+ by (fastforce simp add: pff_def field_split_simps sum_nonneg intro: prod_mono [where g = "\<lambda>x. 1", simplified])
ultimately show ?thesis
by auto
qed
@@ -501,16 +500,16 @@
from subA v have "pff x = ff v x * (\<Prod>w \<in> subA - {v}. ff w x)"
unfolding pff_def by (metis prod.remove)
also have "... \<le> ff v x * 1"
- apply (rule Rings.ordered_semiring_class.mult_left_mono)
- apply (rule prod_mono [where g = "\<lambda>x. 1", simplified])
- using ff [THEN conjunct2, THEN conjunct1] v subA x
- apply auto
- apply (meson atLeastAtMost_iff contra_subsetD imageI)
- apply (meson atLeastAtMost_iff contra_subsetD image_eqI)
- using atLeastAtMost_iff by blast
+ proof -
+ have "\<And>i. i \<in> subA - {v} \<Longrightarrow> 0 \<le> ff i x \<and> ff i x \<le> 1"
+ by (metis Diff_subset atLeastAtMost_iff ff image_subset_iff subA(1) subsetD x(2))
+ moreover have "0 \<le> ff v x"
+ using ff subA(1) v x(2) by fastforce
+ ultimately show ?thesis
+ by (metis mult_left_mono prod_mono [where g = "\<lambda>x. 1", simplified])
+ qed
also have "... < e / card subA"
- using ff [THEN conjunct2, THEN conjunct2, THEN conjunct1] v subA x
- by auto
+ using ff subA(1) v x by auto
also have "... \<le> e"
using cardp e by (simp add: field_split_simps)
finally have "pff x < e" .
@@ -528,18 +527,18 @@
also have "... = (\<Prod>w \<in> subA. 1 - e / card subA)"
by (simp add: subA(2))
also have "... < pff x"
+ proof -
+ have "\<And>i. i \<in> subA \<Longrightarrow> e / real (card subA) \<le> 1 \<and> 1 - e / real (card subA) < ff i x"
+ using e \<open>B \<subseteq> S\<close> ff subA(1) x by (force simp: field_split_simps)
+ then show ?thesis
apply (simp add: pff_def)
apply (rule prod_mono_strict [where f = "\<lambda>x. 1 - e / card subA", simplified])
- apply (simp_all add: subA(2))
- apply (intro ballI conjI)
- using e apply (force simp: field_split_simps)
- using ff [THEN conjunct2, THEN conjunct2, THEN conjunct2] subA B x
- apply blast
- done
+ apply (simp_all add: subA(2))
+ done
+ qed
finally have "1 - e < pff x" .
}
- ultimately
- show ?thesis by blast
+ ultimately show ?thesis by blast
qed
lemma (in function_ring_on) two:
@@ -550,11 +549,8 @@
shows "\<exists>f \<in> R. f ` S \<subseteq> {0..1} \<and> (\<forall>x \<in> A. f x < e) \<and> (\<forall>x \<in> B. f x > 1 - e)"
proof (cases "A \<noteq> {} \<and> B \<noteq> {}")
case True then show ?thesis
- apply (simp flip: ex_in_conv)
using assms
- apply safe
- apply (force simp add: intro!: two_special)
- done
+ by (force simp flip: ex_in_conv intro!: two_special)
next
case False with e show ?thesis
apply simp
@@ -1387,24 +1383,26 @@
also have "... = (\<Sum>i\<in>B. (norm (((f x - g x) \<bullet> i) *\<^sub>R i))\<^sup>2)"
by (simp add: algebra_simps)
also have "... \<le> (\<Sum>i\<in>B. (norm (f x - g x))\<^sup>2)"
- apply (rule sum_mono)
- apply (simp add: B1)
- apply (rule order_trans [OF Cauchy_Schwarz_ineq])
- by (simp add: B1 dot_square_norm)
+ proof -
+ have "\<And>i. i \<in> B \<Longrightarrow> ((f x - g x) \<bullet> i)\<^sup>2 \<le> (norm (f x - g x))\<^sup>2"
+ by (metis B1 Cauchy_Schwarz_ineq inner_commute mult.left_neutral norm_eq_1 power2_norm_eq_inner)
+ then show ?thesis
+ by (intro sum_mono) (simp add: sum_mono B1)
+ qed
also have "... = n * norm (f x - g x)^2"
by (simp add: \<open>n = card B\<close>)
also have "... \<le> n * (e / (n+2))^2"
- apply (rule mult_left_mono)
- apply (meson dual_order.order_iff_strict g norm_ge_zero power_mono that, simp)
- done
+ proof (rule mult_left_mono)
+ show "(norm (f x - g x))\<^sup>2 \<le> (e / real (n + 2))\<^sup>2"
+ by (meson dual_order.order_iff_strict g norm_ge_zero power_mono that)
+ qed auto
also have "... \<le> e^2 / (n+2)"
using \<open>0 < e\<close> by (simp add: divide_simps power2_eq_square)
also have "... < e^2"
using \<open>0 < e\<close> by (simp add: divide_simps)
finally have "(norm (\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i))\<^sup>2 < e^2" .
then have "(norm (\<Sum>i\<in>B. (f x \<bullet> i) *\<^sub>R i - (g x \<bullet> i) *\<^sub>R i)) < e"
- apply (rule power2_less_imp_less)
- using \<open>0 < e\<close> by auto
+ by (simp add: \<open>0 < e\<close> norm_lt_square power2_norm_eq_inner)
then show ?thesis
using fx that by (simp add: sum_subtractf)
qed
--- a/src/HOL/Analysis/ex/Approximations.thy Thu Aug 27 17:15:33 2020 +0200
+++ b/src/HOL/Analysis/ex/Approximations.thy Fri Aug 28 12:04:53 2020 +0100
@@ -99,9 +99,8 @@
from assms show "(exp x - approx) \<ge> 0"
by (intro sums_le[OF _ sums_zero sums]) auto
- have "\<forall>k. x^n * (x^k / fact (n+k)) \<le> (x^n / fact n) * (x / 2)^k"
- proof
- fix k :: nat
+ have "x^n * (x^k / fact (n+k)) \<le> (x^n / fact n) * (x / 2)^k" for k::nat
+ proof -
have "x^n * (x^k / fact (n + k)) = x^(n+k) / fact (n + k)" by (simp add: power_add)
also from assms have "\<dots> \<le> x^(n+k) / (2^k * fact n)"
by (intro divide_left_mono two_power_fact_le_fact zero_le_power) simp_all
--- a/src/HOL/Complex_Analysis/Complex_Singularities.thy Thu Aug 27 17:15:33 2020 +0200
+++ b/src/HOL/Complex_Analysis/Complex_Singularities.thy Fri Aug 28 12:04:53 2020 +0100
@@ -33,8 +33,7 @@
proof -
define g where "g \<equiv> \<lambda>x. if x=z then 0 else inverse (f x)"
have "isCont g z" unfolding isCont_def using is_pole_tendsto[OF pole]
- apply (subst Lim_cong_at[where b=z and y=0 and g="inverse \<circ> f"])
- by (simp_all add:g_def)
+ by (simp add: g_def cong: LIM_cong)
moreover have "continuous_on (s-{z}) f" using f_holo holomorphic_on_imp_continuous_on by auto
hence "continuous_on (s-{z}) (inverse o f)" unfolding comp_def
by (auto elim!:continuous_on_inverse simp add:non_z)
--- a/src/HOL/Computational_Algebra/Polynomial.thy Thu Aug 27 17:15:33 2020 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Fri Aug 28 12:04:53 2020 +0100
@@ -2613,7 +2613,7 @@
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)
+ using IVT [of "poly p" a 0 b] by (auto simp add: order_le_less)
lemma poly_IVT_neg: "a < b \<Longrightarrow> 0 < poly p a \<Longrightarrow> poly p b < 0 \<Longrightarrow> \<exists>x. a < x \<and> x < b \<and> poly p x = 0"
for a b :: real
--- a/src/HOL/Deriv.thy Thu Aug 27 17:15:33 2020 +0200
+++ b/src/HOL/Deriv.thy Fri Aug 28 12:04:53 2020 +0100
@@ -141,7 +141,15 @@
lemma has_derivative_at_within:
"(f has_derivative f') (at x within s) \<longleftrightarrow>
(bounded_linear f' \<and> ((\<lambda>y. ((f y - f x) - f' (y - x)) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within s))"
- by (cases "at x within s = bot") (simp_all add: has_derivative_def Lim_ident_at)
+proof (cases "at x within s = bot")
+ case True
+ then show ?thesis
+ by (metis (no_types, lifting) has_derivative_within tendsto_bot)
+next
+ case False
+ then show ?thesis
+ by (simp add: Lim_ident_at has_derivative_def)
+qed
lemma has_derivative_iff_norm:
"(f has_derivative f') (at x within s) \<longleftrightarrow>
--- a/src/HOL/Library/Extended_Real.thy Thu Aug 27 17:15:33 2020 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri Aug 28 12:04:53 2020 +0100
@@ -4008,11 +4008,15 @@
proof -
have **: "((\<lambda>x. ereal (inverse x)) \<longlongrightarrow> ereal 0) at_infinity"
by (intro tendsto_intros tendsto_inverse_0)
-
- show ?thesis
- by (simp add: at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def)
- (auto simp: eventually_at_top_linorder exI[of _ 1] zero_ereal_def at_top_le_at_infinity
- intro!: filterlim_mono_eventually[OF **])
+ then have "((\<lambda>x. if x = 0 then \<infinity> else ereal (inverse x)) \<longlongrightarrow> 0) at_top"
+ proof (rule filterlim_mono_eventually)
+ show "nhds (ereal 0) \<le> nhds 0"
+ by (simp add: zero_ereal_def)
+ show "(at_top::real filter) \<le> at_infinity"
+ by (simp add: at_top_le_at_infinity)
+ qed auto
+ then show ?thesis
+ unfolding at_infty_ereal_eq_at_top tendsto_compose_filtermap[symmetric] comp_def by auto
qed
lemma inverse_ereal_tendsto_pos:
--- a/src/HOL/Limits.thy Thu Aug 27 17:15:33 2020 +0200
+++ b/src/HOL/Limits.thy Fri Aug 28 12:04:53 2020 +0100
@@ -116,9 +116,6 @@
lemma BseqI': "(\<And>n. norm (X n) \<le> K) \<Longrightarrow> Bseq X"
by (intro BfunI) (auto simp: eventually_sequentially)
-lemma BseqI2': "\<forall>n\<ge>N. norm (X n) \<le> K \<Longrightarrow> Bseq X"
- by (intro BfunI) (auto simp: eventually_sequentially)
-
lemma Bseq_def: "Bseq X \<longleftrightarrow> (\<exists>K>0. \<forall>n. norm (X n) \<le> K)"
unfolding Bfun_def eventually_sequentially
proof safe
@@ -343,7 +340,7 @@
subsubsection\<^marker>\<open>tag unimportant\<close> \<open>Polynomal function extremal theorem, from HOL Light\<close>
-lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*)
+lemma polyfun_extremal_lemma:
fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
assumes "0 < e"
shows "\<exists>M. \<forall>z. M \<le> norm(z) \<longrightarrow> norm (\<Sum>i\<le>n. c(i) * z^i) \<le> e * norm(z) ^ (Suc n)"
@@ -386,14 +383,13 @@
proof (induction n)
case 0
then show ?case
- using k by simp
+ using k by simp
next
case (Suc m)
- let ?even = ?case
- show ?even
+ show ?case
proof (cases "c (Suc m) = 0")
case True
- then show ?even using Suc k
+ then show ?thesis using Suc k
by auto (metis antisym_conv less_eq_Suc_le not_le)
next
case False
@@ -424,7 +420,7 @@
apply (simp add: field_simps norm_mult norm_power)
done
qed
- then show ?even
+ then show ?thesis
by (simp add: eventually_at_infinity)
qed
qed
@@ -1526,10 +1522,12 @@
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 filterlim_at_bot 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
+proof (rule filtermap_fun_inverse[symmetric])
+ show "filterlim uminus at_top (at_bot::'a filter)"
+ using eventually_at_bot_linorder filterlim_at_top le_minus_iff by force
+ show "filterlim uminus (at_bot::'a filter) at_top"
+ by (simp add: filterlim_at_bot minus_le_iff)
+qed auto
lemma at_top_mirror :
shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot"
@@ -1992,9 +1990,8 @@
proof (intro filterlim_at_infinity[THEN iffD2] allI impI)
fix y :: real
assume "0 < y"
- have "0 < norm x - 1" by simp
- then obtain N :: nat where "y < real N * (norm x - 1)"
- by (blast dest: reals_Archimedean3)
+ obtain N :: nat where "y < real N * (norm x - 1)"
+ by (meson diff_gt_0_iff_gt reals_Archimedean3 x)
also have "\<dots> \<le> real N * (norm x - 1) + 1"
by simp
also have "\<dots> \<le> (norm x - 1 + 1) ^ N"
@@ -2181,9 +2178,7 @@
text \<open>A congruence rule allowing us to transform limits assuming not at point.\<close>
-(* FIXME: Only one congruence rule for tendsto can be used at a time! *)
-
-lemma Lim_cong_within(*[cong add]*):
+lemma Lim_cong_within:
assumes "a = b"
and "x = y"
and "S = T"
@@ -2192,13 +2187,6 @@
unfolding tendsto_def eventually_at_topological
using assms by simp
-lemma Lim_cong_at(*[cong add]*):
- assumes "a = b" "x = y"
- and "\<And>x. x \<noteq> a \<Longrightarrow> f x = g x"
- shows "((\<lambda>x. f x) \<longlongrightarrow> x) (at a) \<longleftrightarrow> ((g \<longlongrightarrow> y) (at a))"
- unfolding tendsto_def eventually_at_topological
- using assms by simp
-
text \<open>An unbounded sequence's inverse tends to 0.\<close>
lemma LIMSEQ_inverse_zero:
assumes "\<And>r::real. \<exists>N. \<forall>n\<ge>N. r < X n"
@@ -2963,19 +2951,6 @@
\<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<forall>N. N < M \<longrightarrow> (\<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x))"
using isCont_eq_Ub[of a b f] by auto
-(*HOL style here: object-level formulations*)
-lemma IVT_objl:
- "(f a \<le> y \<and> y \<le> f b \<and> a \<le> b \<and> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x)) \<longrightarrow>
- (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y)"
- for a y :: real
- by (blast intro: IVT)
-
-lemma IVT2_objl:
- "(f b \<le> y \<and> y \<le> f a \<and> a \<le> b \<and> (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x)) \<longrightarrow>
- (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = y)"
- for b y :: real
- by (blast intro: IVT2)
-
lemma isCont_Lb_Ub:
fixes f :: "real \<Rightarrow> real"
assumes "a \<le> b" "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x"
--- a/src/HOL/Series.thy Thu Aug 27 17:15:33 2020 +0200
+++ b/src/HOL/Series.thy Fri Aug 28 12:04:53 2020 +0100
@@ -200,7 +200,7 @@
subsection \<open>Infinite summability on ordered, topological monoids\<close>
-lemma sums_le: "\<forall>n. f n \<le> g n \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t"
+lemma sums_le: "(\<And>n. f n \<le> g n) \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t"
for f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology}"
by (rule LIMSEQ_le) (auto intro: sum_mono simp: sums_def)
@@ -208,24 +208,26 @@
fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology}"
begin
-lemma suminf_le: "\<forall>n. f n \<le> g n \<Longrightarrow> summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f \<le> suminf g"
- by (auto dest: sums_summable intro: sums_le)
+lemma suminf_le: "(\<And>n. f n \<le> g n) \<Longrightarrow> summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f \<le> suminf g"
+ using sums_le by blast
lemma sum_le_suminf:
- shows "summable f \<Longrightarrow> finite I \<Longrightarrow> \<forall>m\<in>- I. 0 \<le> f m \<Longrightarrow> sum f I \<le> suminf f"
+ shows "summable f \<Longrightarrow> finite I \<Longrightarrow> (\<And>n. n \<in>- I \<Longrightarrow> 0 \<le> f n) \<Longrightarrow> sum f I \<le> suminf f"
by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
-lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
+lemma suminf_nonneg: "summable f \<Longrightarrow> (\<And>n. 0 \<le> f n) \<Longrightarrow> 0 \<le> suminf f"
using sum_le_suminf by force
lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. sum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
by (metis LIMSEQ_le_const2 summable_LIMSEQ)
-lemma suminf_eq_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
+lemma suminf_eq_zero_iff:
+ assumes "summable f" and pos: "\<And>n. 0 \<le> f n"
+ shows "suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
proof
- assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n"
+ assume "suminf f = 0"
then have f: "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> 0"
- using summable_LIMSEQ[of f] by simp
+ using summable_LIMSEQ[of f] assms by simp
then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
proof (rule LIMSEQ_le_const)
show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> sum f {..<n}" for i
@@ -235,11 +237,11 @@
by (auto intro!: antisym)
qed (metis suminf_zero fun_eq_iff)
-lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
+lemma suminf_pos_iff: "summable f \<Longrightarrow> (\<And>n. 0 \<le> f n) \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
using sum_le_suminf[of "{}"] suminf_eq_zero_iff by (simp add: less_le)
lemma suminf_pos2:
- assumes "summable f" "\<forall>n. 0 \<le> f n" "0 < f i"
+ assumes "summable f" "\<And>n. 0 \<le> f n" "0 < f i"
shows "0 < suminf f"
proof -
have "0 < (\<Sum>n<Suc i. f n)"
@@ -249,7 +251,7 @@
finally show ?thesis .
qed
-lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
+lemma suminf_pos: "summable f \<Longrightarrow> (\<And>n. 0 < f n) \<Longrightarrow> 0 < suminf f"
by (intro suminf_pos2[where i=0]) (auto intro: less_imp_le)
end
@@ -259,13 +261,13 @@
begin
lemma sum_less_suminf2:
- "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> sum f {..<n} < suminf f"
+ "summable f \<Longrightarrow> (\<And>m. m\<ge>n \<Longrightarrow> 0 \<le> f m) \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> sum f {..<n} < suminf f"
using sum_le_suminf[of f "{..< Suc i}"]
and add_strict_increasing[of "f i" "sum f {..<n}" "sum f {..<i}"]
and sum_mono2[of "{..<i}" "{..<n}" f]
by (auto simp: less_imp_le ac_simps)
-lemma sum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> sum f {..<n} < suminf f"
+lemma sum_less_suminf: "summable f \<Longrightarrow> (\<And>m. m\<ge>n \<Longrightarrow> 0 < f m) \<Longrightarrow> sum f {..<n} < suminf f"
using sum_less_suminf2[of n n] by (simp add: less_imp_le)
end
@@ -460,11 +462,15 @@
by (auto simp: norm_minus_commute suminf_minus_initial_segment[OF \<open>summable f\<close>])
qed
-lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f \<longlonglongrightarrow> 0"
- apply (drule summable_iff_convergent [THEN iffD1])
- apply (drule convergent_Cauchy)
- apply (simp only: Cauchy_iff LIMSEQ_iff)
- by (metis add.commute add_diff_cancel_right' diff_zero le_SucI sum.lessThan_Suc)
+lemma summable_LIMSEQ_zero:
+ assumes "summable f" shows "f \<longlonglongrightarrow> 0"
+proof -
+ have "Cauchy (\<lambda>n. sum f {..<n})"
+ using LIMSEQ_imp_Cauchy assms summable_LIMSEQ by blast
+ then show ?thesis
+ unfolding Cauchy_iff LIMSEQ_iff
+ by (metis add.commute add_diff_cancel_right' diff_zero le_SucI sum.lessThan_Suc)
+qed
lemma summable_imp_convergent: "summable f \<Longrightarrow> convergent f"
by (force dest!: summable_LIMSEQ_zero simp: convergent_def)
@@ -1286,7 +1292,6 @@
from eventually_conj[OF this bound] obtain x0 where x0:
"\<And>x. x \<ge> x0 \<Longrightarrow> \<bar>g x\<bar> < \<epsilon>" "\<And>a b. x0 \<le> a \<Longrightarrow> a < b \<Longrightarrow> norm (sum f {a<..b}) \<le> g a"
unfolding eventually_at_top_linorder by auto
-
show ?case
proof (intro exI[of _ x0] allI impI)
fix m n assume mn: "x0 \<le> m" "m < n"
--- a/src/HOL/Transcendental.thy Thu Aug 27 17:15:33 2020 +0200
+++ b/src/HOL/Transcendental.thy Fri Aug 28 12:04:53 2020 +0100
@@ -743,7 +743,7 @@
then have "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))"
by (rule summable_norm)
also from 1 3 2 have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)"
- by (rule suminf_le)
+ by (simp add: suminf_le)
also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h"
by (rule suminf_mult2 [symmetric])
finally show "norm (suminf (g h)) \<le> suminf f * norm h" .
@@ -1003,7 +1003,7 @@
have *: "((\<lambda>x. if x = 0 then a 0 else f x) \<longlongrightarrow> a 0) (at 0)"
by (rule powser_limit_0 [OF s]) (auto simp: powser_sums_zero sm)
show ?thesis
- by (simp add: * LIM_equal [where g = "(\<lambda>x. if x = 0 then a 0 else f x)"])
+ using "*" by (auto cong: Lim_cong_within)
qed
@@ -1574,10 +1574,7 @@
have "1 + x \<le> (\<Sum>n<2. inverse (fact n) * x^n)"
by (auto simp: numeral_2_eq_2)
also have "\<dots> \<le> (\<Sum>n. inverse (fact n) * x^n)"
- proof (rule sum_le_suminf [OF summable_exp])
- show "\<forall>m\<in>- {..<2}. 0 \<le> inverse (fact m) * x ^ m"
- using \<open>0 < x\<close> by (auto simp add: zero_le_mult_iff)
- qed auto
+ using \<open>0 < x\<close> by (auto simp add: zero_le_mult_iff intro: sum_le_suminf [OF summable_exp])
finally show "1 + x \<le> exp x"
by (simp add: exp_def)
qed auto
@@ -3643,9 +3640,7 @@
have sums: "?f sums sin x"
by (rule sin_paired [THEN sums_group]) simp
show "0 < sin x"
- unfolding sums_unique [OF sums]
- using sums_summable [OF sums] pos
- by (rule suminf_pos)
+ unfolding sums_unique [OF sums] using sums_summable [OF sums] pos by (simp add: suminf_pos)
qed
lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
--- a/src/HOL/ex/HarmonicSeries.thy Thu Aug 27 17:15:33 2020 +0200
+++ b/src/HOL/ex/HarmonicSeries.thy Fri Aug 28 12:04:53 2020 +0100
@@ -280,8 +280,8 @@
then obtain n::nat where ndef: "n = nat \<lceil>2 * ?s\<rceil>" by simp
then have ngt: "1 + real n/2 > ?s" by linarith
define j where "j = (2::nat)^n"
- have "\<forall>m\<ge>j. 0 < ?f m" by simp
- with sf have "(\<Sum>i<j. ?f i) < ?s" by (rule sum_less_suminf)
+ have "(\<Sum>i<j. ?f i) < ?s"
+ using sf by (simp add: sum_less_suminf)
then have "(\<Sum>i\<in>{Suc 0..<Suc j}. 1/(real i)) < ?s"
unfolding sum.shift_bounds_Suc_ivl by (simp add: atLeast0LessThan)
with j_def have