--- a/src/HOL/Analysis/Complex_Transcendental.thy Wed Feb 15 12:48:53 2023 +0000
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Feb 16 10:42:28 2023 +0000
@@ -2768,7 +2768,7 @@
apply (subst filterlim_sequentially_Suc [symmetric])
by (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide)
-lemma lim_1_over_Ln: "((\<lambda>n. 1 / Ln(of_nat n)) \<longlongrightarrow> 0) sequentially"
+lemma lim_1_over_Ln: "(\<lambda>n. 1 / Ln (complex_of_nat n)) \<longlonglongrightarrow> 0"
proof (clarsimp simp add: lim_sequentially dist_norm norm_divide field_split_simps)
fix r::real
assume "0 < r"
@@ -2790,7 +2790,7 @@
by (rule_tac x=n in exI) (force simp: field_split_simps intro: less_le_trans)
qed
-lemma lim_1_over_ln: "((\<lambda>n. 1 / ln(real_of_nat n)) \<longlongrightarrow> 0) sequentially"
+lemma lim_1_over_ln: "(\<lambda>n. 1 / ln (real n)) \<longlonglongrightarrow> 0"
using lim_1_over_Ln [THEN filterlim_sequentially_Suc [THEN iffD2]]
apply (subst filterlim_sequentially_Suc [symmetric])
by (simp add: lim_sequentially dist_norm Ln_Reals_eq norm_powr_real_powr norm_divide)
@@ -2824,19 +2824,14 @@
qed
lemma lim_ln_over_ln1: "(\<lambda>n. ln n / ln(Suc n)) \<longlonglongrightarrow> 1"
-proof -
- have "(\<lambda>n. inverse (ln(Suc n) / ln n)) \<longlonglongrightarrow> inverse 1"
- by (rule tendsto_inverse [OF lim_ln1_over_ln]) auto
- then show ?thesis
- by simp
-qed
+ using tendsto_inverse [OF lim_ln1_over_ln] by force
subsection\<^marker>\<open>tag unimportant\<close>\<open>Relation between Square Root and exp/ln, hence its derivative\<close>
lemma csqrt_exp_Ln:
assumes "z \<noteq> 0"
- shows "csqrt z = exp(Ln(z) / 2)"
+ shows "csqrt z = exp(Ln z / 2)"
proof -
have "(exp (Ln z / 2))\<^sup>2 = (exp (Ln z))"
by (metis exp_double nonzero_mult_div_cancel_left times_divide_eq_right zero_neq_numeral)
@@ -2936,12 +2931,7 @@
by (simp add: continuous_at_imp_continuous_on continuous_within_csqrt)
lemma holomorphic_on_csqrt [holomorphic_intros]: "csqrt holomorphic_on -\<real>\<^sub>\<le>\<^sub>0"
-proof -
- have *: "(\<lambda>z. exp (ln z / 2)) holomorphic_on -\<real>\<^sub>\<le>\<^sub>0"
- by (intro holomorphic_intros) auto
- then show ?thesis
- using field_differentiable_within_csqrt holomorphic_on_def by auto
-qed
+ by (simp add: field_differentiable_within_csqrt holomorphic_on_def)
lemma holomorphic_on_csqrt' [holomorphic_intros]:
"f holomorphic_on A \<Longrightarrow> (\<And>z. z \<in> A \<Longrightarrow> f z \<notin> \<real>\<^sub>\<le>\<^sub>0) \<Longrightarrow> (\<lambda>z. csqrt (f z)) holomorphic_on A"
@@ -2956,8 +2946,7 @@
lemma continuous_within_closed_nontrivial:
"closed s \<Longrightarrow> a \<notin> s ==> continuous (at a within s) f"
- using open_Compl
- by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
+ using Compl_iff continuous_within_topological open_Compl by fastforce
lemma continuous_within_csqrt_posreal:
"continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
@@ -3017,17 +3006,13 @@
lemma tan_Arctan:
assumes "z\<^sup>2 \<noteq> -1"
- shows [simp]:"tan(Arctan z) = z"
+ shows [simp]: "tan(Arctan z) = z"
proof -
- have "1 + \<i>*z \<noteq> 0"
- by (metis assms complex_i_mult_minus i_squared minus_unique power2_eq_square power2_minus)
- moreover
- have "1 - \<i>*z \<noteq> 0"
- by (metis assms complex_i_mult_minus i_squared power2_eq_square power2_minus right_minus_eq)
- ultimately
- show ?thesis
- by (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus csqrt_exp_Ln [symmetric]
- divide_simps power2_eq_square [symmetric])
+ obtain "1 + \<i>*z \<noteq> 0" "1 - \<i>*z \<noteq> 0"
+ by (metis add_diff_cancel_left' assms diff_0 i_times_eq_iff mult_cancel_left2 power2_i power2_minus right_minus_eq)
+ then show ?thesis
+ by (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus divide_simps
+ flip: csqrt_exp_Ln power2_eq_square)
qed
lemma Arctan_tan [simp]:
@@ -3050,8 +3035,7 @@
by (simp add: algebra_simps)
also have "\<dots> \<longleftrightarrow> False"
using assms ge_pi2
- apply (auto simp: algebra_simps)
- by (metis abs_mult_pos not_less of_nat_less_0_iff of_nat_numeral)
+ by (metis eq_divide_eq linorder_not_less mult.commute zero_neq_numeral)
finally have "exp (\<i>*z)*exp (\<i>*z) + 1 \<noteq> 0"
by (auto simp: add.commute minus_unique)
then show "exp (2 * z / \<i>) = (1 - \<i> * tan z) / (1 + \<i> * tan z)"
@@ -3137,7 +3121,7 @@
define G where [abs_def]: "G z = (\<Sum>n. g n * z^n)" for z
have summable: "summable (\<lambda>n. g n * u^n)" if "norm u < 1" for u
proof (cases "u = 0")
- assume u: "u \<noteq> 0"
+ case False
have "(\<lambda>n. ereal (norm (h u n) / norm (h u (Suc n)))) = (\<lambda>n. ereal (inverse (norm u)^2) *
ereal ((2 + inverse (real (Suc n))) / (2 - inverse (real (Suc n)))))"
proof
@@ -3158,10 +3142,10 @@
by (intro tendsto_intros LIMSEQ_inverse_real_of_nat) simp_all
finally have "liminf (\<lambda>n. ereal (cmod (h u n) / cmod (h u (Suc n)))) = inverse (norm u)^2"
by (intro lim_imp_Liminf) simp_all
- moreover from power_strict_mono[OF that, of 2] u have "inverse (norm u)^2 > 1"
+ moreover from power_strict_mono[OF that, of 2] False have "inverse (norm u)^2 > 1"
by (simp add: field_split_simps)
ultimately have A: "liminf (\<lambda>n. ereal (cmod (h u n) / cmod (h u (Suc n)))) > 1" by simp
- from u have "summable (h u)"
+ from False have "summable (h u)"
by (intro summable_norm_cancel[OF ratio_test_convergence[OF _ A]])
(auto simp: h_def norm_divide norm_mult norm_power simp del: of_nat_Suc
intro!: mult_pos_pos divide_pos_pos always_eventually)
@@ -3263,7 +3247,7 @@
by (simp add: Arctan_def)
next
have "tan (Re (Arctan (of_real x))) = Re (tan (Arctan (of_real x)))"
- by (auto simp: tan_def Complex.Re_divide Re_sin Re_cos Im_sin Im_cos field_simps power2_eq_square)
+ by (metis Im_Arctan_of_real Re_complex_of_real complex_is_Real_iff of_real_Re tan_of_real)
also have "\<dots> = x"
proof -
have "(complex_of_real x)\<^sup>2 \<noteq> - 1"
@@ -3305,8 +3289,7 @@
show 12: "- (pi / 2) < arctan x + arctan y" "arctan x + arctan y < pi / 2"
using assms by linarith+
show "tan (arctan x + arctan y) = (x + y) / (1 - x * y)"
- using cos_gt_zero_pi [OF 12]
- by (simp add: arctan tan_add)
+ using cos_gt_zero_pi [OF 12] by (simp add: arctan tan_add)
qed
lemma arctan_inverse:
@@ -3350,8 +3333,7 @@
lemma arctan_bounds:
assumes "0 \<le> x" "x < 1"
shows arctan_lower_bound:
- "(\<Sum>k<2 * n. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1))) \<le> arctan x"
- (is "(\<Sum>k<_. (- 1)^ k * ?a k) \<le> _")
+ "(\<Sum>k<2 * n. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1))) \<le> arctan x" (is "(\<Sum>k<_. _ * ?a k) \<le> _")
and arctan_upper_bound:
"arctan x \<le> (\<Sum>k<2 * n + 1. (- 1) ^ k * (1 / real (k * 2 + 1) * x ^ (k * 2 + 1)))"
proof -
@@ -3397,7 +3379,7 @@
lemma Arcsin_body_lemma: "\<i> * z + csqrt(1 - z\<^sup>2) \<noteq> 0"
using power2_csqrt [of "1 - z\<^sup>2"]
- by (metis add.inverse_inverse complex_i_mult_minus diff_0 diff_add_cancel diff_minus_eq_add mult.assoc mult.commute numeral_One power2_eq_square zero_neq_numeral)
+ by (metis add.inverse_unique diff_0 diff_add_cancel mult.left_commute mult_minus1_right power2_i power2_minus power_mult_distrib zero_neq_one)
lemma Arcsin_range_lemma: "\<bar>Re z\<bar> < 1 \<Longrightarrow> 0 < Re(\<i> * z + csqrt(1 - z\<^sup>2))"
using Complex.cmod_power2 [of z, symmetric]
@@ -3725,8 +3707,9 @@
next
assume L: ?L
let ?goal = "(\<exists>k::int. x = arccos y + 2*k*pi \<or> x = - arccos y + 2*k*pi)"
- obtain k::int where k: "-pi < x-k*2*pi" "x-k*2*pi \<le> pi"
- by (metis Arg_bounded Arg_exp_diff_2pi complex.sel(2) mult.assoc of_int_mult of_int_numeral)
+ obtain k::int where k: "-pi < x - k*(2*pi)" "x - k*(2*pi) \<le> pi"
+ using ceiling_divide_lower [of "2*pi" "x-pi"] ceiling_divide_upper [of "2*pi" "x-pi"]
+ by (simp add: divide_simps algebra_simps) (metis mult.commute)
have *: "cos (x - k * 2*pi) = y"
using cos.periodic_simps(3)[of x "-k"] L by (auto simp add:field_simps)
then have \<section>: ?goal when "x-k*2*pi \<ge> 0"
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Wed Feb 15 12:48:53 2023 +0000
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Thu Feb 16 10:42:28 2023 +0000
@@ -332,6 +332,9 @@
lemma fls_shift_eq0_iff: "fls_shift m f = 0 \<longleftrightarrow> f = 0"
using fls_shift_eq_iff[of m f 0] by simp
+lemma fls_shift_eq_1_iff: "fls_shift n f = 1 \<longleftrightarrow> f = fls_shift (-n) 1"
+ by (metis add_minus_cancel fls_shift_eq_iff fls_shift_fls_shift)
+
lemma fls_shift_nonneg_subdegree: "m \<le> fls_subdegree f \<Longrightarrow> fls_subdegree (fls_shift m f) \<ge> 0"
by (cases "f=0") (auto intro: fls_subdegree_geI)
@@ -699,6 +702,9 @@
thus "f $ n = g $ n" by simp
qed
+lemma fps_to_fls_eq_iff [simp]: "fps_to_fls f = fps_to_fls g \<longleftrightarrow> f = g"
+ using fps_to_fls_eq_imp_fps_eq by blast
+
lemma fps_zero_to_fls [simp]: "fps_to_fls 0 = 0"
by (intro fls_zero_eqI) simp
@@ -723,9 +729,12 @@
lemma fps_X_to_fls [simp]: "fps_to_fls fps_X = fls_X"
by (fastforce intro: fls_eqI)
-lemma fps_to_fls_eq_zero_iff: "(fps_to_fls f = 0) \<longleftrightarrow> (f=0)"
+lemma fps_to_fls_eq_0_iff [simp]: "(fps_to_fls f = 0) \<longleftrightarrow> (f=0)"
using fps_to_fls_nonzeroI by auto
+lemma fps_to_fls_eq_1_iff [simp]: "fps_to_fls f = 1 \<longleftrightarrow> f = 1"
+ using fps_to_fls_eq_iff by fastforce
+
lemma fls_subdegree_fls_to_fps_gt0: "fls_subdegree (fps_to_fls f) \<ge> 0"
proof (cases "f=0")
case False show ?thesis
@@ -780,6 +789,25 @@
using fls_base_factor_fps_to_fls[of f] fls_regpart_fps_trivial[of "unit_factor f"]
by simp
+lemma fls_as_fps:
+ fixes f :: "'a :: zero fls" and n :: int
+ assumes n: "n \<ge> -fls_subdegree f"
+ obtains f' where "f = fls_shift n (fps_to_fls f')"
+proof -
+ have "fls_subdegree (fls_shift (- n) f) \<ge> 0"
+ by (rule fls_shift_nonneg_subdegree) (use n in simp)
+ hence "f = fls_shift n (fps_to_fls (fls_regpart (fls_shift (-n) f)))"
+ by (subst fls_regpart_to_fls_trivial) simp_all
+ thus ?thesis
+ by (rule that)
+qed
+
+lemma fls_as_fps':
+ fixes f :: "'a :: zero fls" and n :: int
+ assumes n: "n \<ge> -fls_subdegree f"
+ shows "\<exists>f'. f = fls_shift n (fps_to_fls f')"
+ using fls_as_fps[OF assms] by metis
+
abbreviation
"fls_regpart_as_fls f \<equiv> fps_to_fls (fls_regpart f)"
abbreviation
@@ -1719,10 +1747,12 @@
by (simp add: fls_times_conv_fps_times)
qed simp
+lemma fps_to_fls_power: "fps_to_fls (f ^ n) = fps_to_fls f ^ n"
+ by (simp add: fls_pow_conv_fps_pow fls_subdegree_fls_to_fps_gt0)
+
lemma fls_pow_conv_regpart:
"fls_subdegree f \<ge> 0 \<Longrightarrow> fls_regpart (f ^ n) = (fls_regpart f) ^ n"
- using fls_pow_subdegree_ge0[of f n] fls_pow_conv_fps_pow[of f n]
- by (intro fps_to_fls_eq_imp_fps_eq) simp
+ by (simp add: fls_pow_conv_fps_pow)
text \<open>These two lemmas show that shifting 1 is equivalent to powers of the implied variable.\<close>
@@ -1995,17 +2025,7 @@
lemma fls_lr_inverse_eq0_imp_starting0:
"fls_left_inverse f x = 0 \<Longrightarrow> x = 0"
"fls_right_inverse f x = 0 \<Longrightarrow> x = 0"
-proof-
- assume "fls_left_inverse f x = 0"
- hence "fps_left_inverse (fls_base_factor_to_fps f) x = 0"
- using fls_shift_eq_iff fps_to_fls_eq_zero_iff by fastforce
- thus "x = 0" using fps_lr_inverse_eq0_imp_starting0(1) by fast
-next
- assume "fls_right_inverse f x = 0"
- hence "fps_right_inverse (fls_base_factor_to_fps f) x = 0"
- using fls_shift_eq_iff fps_to_fls_eq_zero_iff by fastforce
- thus "x = 0" using fps_lr_inverse_eq0_imp_starting0(2) by fast
-qed
+ by (metis fls_lr_inverse_base fls_nonzeroI)+
lemma fls_lr_inverse_eq_0_iff:
fixes x :: "'a::{comm_monoid_add,mult_zero,uminus}"
@@ -3231,10 +3251,146 @@
thus "\<exists>g. 1 = g * f" by fast
qed
+subsection \<open>Composition\<close>
+
+definition fls_compose_fps :: "'a :: field fls \<Rightarrow> 'a fps \<Rightarrow> 'a fls" where
+ "fls_compose_fps f g =
+ (if f = 0 then 0
+ else if fls_subdegree f \<ge> 0 then fps_to_fls (fps_compose (fls_regpart f) g)
+ else fps_to_fls (fps_compose (fls_base_factor_to_fps f) g) /
+ fps_to_fls g ^ nat (-fls_subdegree f))"
+
+lemma fls_compose_fps_fps [simp]:
+ "fls_compose_fps (fps_to_fls f) g = fps_to_fls (fps_compose f g)"
+ by (simp add: fls_compose_fps_def fls_subdegree_fls_to_fps_gt0 fps_to_fls_eq_0_iff)
+
+lemma fls_const_transfer [transfer_rule]:
+ "rel_fun (=) (pcr_fls (=))
+ (\<lambda>c n. if n = 0 then c else 0) fls_const"
+ by (auto simp: fls_const_def rel_fun_def pcr_fls_def OO_def cr_fls_def)
+
+lemma fls_shift_transfer [transfer_rule]:
+ "rel_fun (=) (rel_fun (pcr_fls (=)) (pcr_fls (=)))
+ (\<lambda>n f k. f (k+n)) fls_shift"
+ by (auto simp: fls_const_def rel_fun_def pcr_fls_def OO_def cr_fls_def)
+
+lift_definition fls_compose_power :: "'a :: zero fls \<Rightarrow> nat \<Rightarrow> 'a fls" is
+ "\<lambda>f d n. if d > 0 \<and> int d dvd n then f (n div int d) else 0"
+proof -
+ fix f :: "int \<Rightarrow> 'a" and d :: nat
+ assume *: "eventually (\<lambda>n. f (-int n) = 0) cofinite"
+ show "eventually (\<lambda>n. (if d > 0 \<and> int d dvd -int n then f (-int n div int d) else 0) = 0) cofinite"
+ proof (cases "d = 0")
+ case False
+ from * have "eventually (\<lambda>n. f (-int n) = 0) at_top"
+ by (simp add: cofinite_eq_sequentially)
+ hence "eventually (\<lambda>n. f (-int (n div d)) = 0) at_top"
+ by (rule eventually_compose_filterlim[OF _ filterlim_at_top_div_const_nat]) (use False in auto)
+ hence "eventually (\<lambda>n. (if d > 0 \<and> int d dvd -int n then f (-int n div int d) else 0) = 0) at_top"
+ by eventually_elim (auto simp: zdiv_int dvd_neg_div)
+ thus ?thesis
+ by (simp add: cofinite_eq_sequentially)
+ qed auto
+qed
+
+lemma fls_nth_compose_power:
+ assumes "d > 0"
+ shows "fls_nth (fls_compose_power f d) n = (if int d dvd n then fls_nth f (n div int d) else 0)"
+ using assms by transfer auto
+
+
+lemma fls_compose_power_0_left [simp]: "fls_compose_power 0 d = 0"
+ by transfer auto
+
+lemma fls_compose_power_1_left [simp]: "d > 0 \<Longrightarrow> fls_compose_power 1 d = 1"
+ by transfer (auto simp: fun_eq_iff)
+
+lemma fls_compose_power_const_left [simp]:
+ "d > 0 \<Longrightarrow> fls_compose_power (fls_const c) d = fls_const c"
+ by transfer (auto simp: fun_eq_iff)
+
+lemma fls_compose_power_shift [simp]:
+ "d > 0 \<Longrightarrow> fls_compose_power (fls_shift n f) d = fls_shift (d * n) (fls_compose_power f d)"
+ by transfer (auto simp: fun_eq_iff add_ac mult_ac)
+
+lemma fls_compose_power_X_intpow [simp]:
+ "d > 0 \<Longrightarrow> fls_compose_power (fls_X_intpow n) d = fls_X_intpow (int d * n)"
+ by simp
+
+lemma fls_compose_power_X [simp]:
+ "d > 0 \<Longrightarrow> fls_compose_power fls_X d = fls_X_intpow (int d)"
+ by transfer (auto simp: fun_eq_iff)
+
+lemma fls_compose_power_X_inv [simp]:
+ "d > 0 \<Longrightarrow> fls_compose_power fls_X_inv d = fls_X_intpow (-int d)"
+ by (simp add: fls_X_inv_conv_shift_1)
+
+lemma fls_compose_power_0_right [simp]: "fls_compose_power f 0 = 0"
+ by transfer auto
+
+lemma fls_compose_power_add [simp]:
+ "fls_compose_power (f + g) d = fls_compose_power f d + fls_compose_power g d"
+ by transfer auto
+
+lemma fls_compose_power_diff [simp]:
+ "fls_compose_power (f - g) d = fls_compose_power f d - fls_compose_power g d"
+ by transfer auto
+
+lemma fls_compose_power_uminus [simp]:
+ "fls_compose_power (-f) d = -fls_compose_power f d"
+ by transfer auto
+
+lemma fps_nth_compose_X_power:
+ "fps_nth (f oo (fps_X ^ d)) n = (if d dvd n then fps_nth f (n div d) else 0)"
+proof -
+ have "fps_nth (f oo (fps_X ^ d)) n = (\<Sum>i = 0..n. f $ i * (fps_X ^ (d * i)) $ n)"
+ unfolding fps_compose_def by (simp add: power_mult)
+ also have "\<dots> = (\<Sum>i\<in>(if d dvd n then {n div d} else {}). f $ i * (fps_X ^ (d * i)) $ n)"
+ by (intro sum.mono_neutral_right) auto
+ also have "\<dots> = (if d dvd n then fps_nth f (n div d) else 0)"
+ by auto
+ finally show ?thesis .
+qed
+
+lemma fls_compose_power_fps_to_fls:
+ assumes "d > 0"
+ shows "fls_compose_power (fps_to_fls f) d = fps_to_fls (fps_compose f (fps_X ^ d))"
+ using assms
+ by (intro fls_eqI) (auto simp: fls_nth_compose_power fps_nth_compose_X_power
+ pos_imp_zdiv_neg_iff div_neg_pos_less0 nat_div_distrib
+ simp flip: int_dvd_int_iff)
+
+lemma fls_compose_power_mult [simp]:
+ "fls_compose_power (f * g :: 'a :: idom fls) d = fls_compose_power f d * fls_compose_power g d"
+proof (cases "d > 0")
+ case True
+ define n where "n = nat (max 0 (max (- fls_subdegree f) (- fls_subdegree g)))"
+ have n_ge: "-fls_subdegree f \<le> int n" "-fls_subdegree g \<le> int n"
+ unfolding n_def by auto
+ obtain f' where f': "f = fls_shift n (fps_to_fls f')"
+ using fls_as_fps[OF n_ge(1)] by (auto simp: n_def)
+ obtain g' where g': "g = fls_shift n (fps_to_fls g')"
+ using fls_as_fps[OF n_ge(2)] by (auto simp: n_def)
+ show ?thesis using \<open>d > 0\<close>
+ by (simp add: f' g' fls_shifted_times_simps mult_ac fls_compose_power_fps_to_fls
+ fps_compose_mult_distrib flip: fls_times_fps_to_fls)
+qed auto
+
+lemma fls_compose_power_power [simp]:
+ assumes "d > 0 \<or> n > 0"
+ shows "fls_compose_power (f ^ n :: 'a :: idom fls) d = fls_compose_power f d ^ n"
+proof (cases "d > 0")
+ case True
+ thus ?thesis by (induction n) auto
+qed (use assms in auto)
+
+lemma fls_nth_compose_power' [simp]:
+ "d = 0 \<or> \<not>d dvd n \<Longrightarrow> fls_nth (fls_compose_power f d) n = 0"
+ "d dvd n \<Longrightarrow> d > 0 \<Longrightarrow> fls_nth (fls_compose_power f d) n = fls_nth f (n div d)"
+ by (transfer; force; fail)+
subsection \<open>Formal differentiation and integration\<close>
-
subsubsection \<open>Derivative definition and basic properties\<close>
definition "fls_deriv f = Abs_fls (\<lambda>n. of_int (n+1) * f$$(n+1))"
--- a/src/HOL/Filter.thy Wed Feb 15 12:48:53 2023 +0000
+++ b/src/HOL/Filter.thy Thu Feb 16 10:42:28 2023 +0000
@@ -1511,7 +1511,21 @@
fixes f :: "'a \<Rightarrow> ('b::unbounded_dense_linorder)" and c :: "'b"
shows "(LIM x F. f x :> at_bot) \<longleftrightarrow> (\<forall>Z<c. eventually (\<lambda>x. Z \<ge> f x) F)"
by (metis filterlim_at_bot filterlim_at_bot_le lt_ex order_le_less_trans)
-
+
+lemma filterlim_at_top_div_const_nat:
+ assumes "c > 0"
+ shows "filterlim (\<lambda>x::nat. x div c) at_top at_top"
+ unfolding filterlim_at_top
+proof
+ fix C :: nat
+ have *: "n div c \<ge> C" if "n \<ge> C * c" for n
+ using assms that by (metis div_le_mono div_mult_self_is_m)
+ have "eventually (\<lambda>n. n \<ge> C * c) at_top"
+ by (rule eventually_ge_at_top)
+ thus "eventually (\<lambda>n. n div c \<ge> C) at_top"
+ by eventually_elim (use * in auto)
+qed
+
lemma filterlim_finite_subsets_at_top:
"filterlim f (finite_subsets_at_top A) F \<longleftrightarrow>
(\<forall>X. finite X \<and> X \<subseteq> A \<longrightarrow> eventually (\<lambda>y. finite (f y) \<and> X \<subseteq> f y \<and> f y \<subseteq> A) F)"