--- a/src/HOL/Analysis/Uniform_Limit.thy Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Analysis/Uniform_Limit.thy Fri Apr 04 15:30:03 2025 +0200
@@ -112,15 +112,14 @@
by eventually_elim force
qed
-
subsection \<open>Exchange limits\<close>
-
-proposition swap_uniform_limit:
- assumes f: "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) (at x within S)"
+proposition swap_uniform_limit':
+ assumes f: "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) G"
assumes g: "(g \<longlongrightarrow> l) F"
assumes uc: "uniform_limit S f h F"
+ assumes ev: "\<forall>\<^sub>F x in G. x \<in> S"
assumes "\<not>trivial_limit F"
- shows "(h \<longlongrightarrow> l) (at x within S)"
+ shows "(h \<longlongrightarrow> l) G"
proof (rule tendstoI)
fix e :: real
define e' where "e' = e/3"
@@ -131,21 +130,19 @@
by (simp add: dist_commute)
moreover
from f
- have "\<forall>\<^sub>F n in F. \<forall>\<^sub>F x in at x within S. dist (g n) (f n x) < e'"
+ have "\<forall>\<^sub>F n in F. \<forall>\<^sub>F x in G. dist (g n) (f n x) < e'"
by eventually_elim (auto dest!: tendstoD[OF _ \<open>0 < e'\<close>] simp: dist_commute)
moreover
from tendstoD[OF g \<open>0 < e'\<close>] have "\<forall>\<^sub>F x in F. dist l (g x) < e'"
by (simp add: dist_commute)
ultimately
- have "\<forall>\<^sub>F _ in F. \<forall>\<^sub>F x in at x within S. dist (h x) l < e"
+ have "\<forall>\<^sub>F _ in F. \<forall>\<^sub>F x in G. dist (h x) l < e"
proof eventually_elim
case (elim n)
note fh = elim(1)
note gl = elim(3)
- have "\<forall>\<^sub>F x in at x within S. x \<in> S"
- by (auto simp: eventually_at_filter)
- with elim(2)
show ?case
+ using elim(2) ev
proof eventually_elim
case (elim x)
from fh[rule_format, OF \<open>x \<in> S\<close>] elim(1)
@@ -155,10 +152,17 @@
show ?case by (simp add: e'_def)
qed
qed
- thus "\<forall>\<^sub>F x in at x within S. dist (h x) l < e"
+ thus "\<forall>\<^sub>F x in G. dist (h x) l < e"
using eventually_happens by (metis \<open>\<not>trivial_limit F\<close>)
qed
+corollary swap_uniform_limit:
+ assumes "\<forall>\<^sub>F n in F. (f n \<longlongrightarrow> g n) (at x within S)"
+ assumes "(g \<longlongrightarrow> l) F" "uniform_limit S f h F" "\<not>trivial_limit F"
+ shows "(h \<longlongrightarrow> l) (at x within S)"
+ using swap_uniform_limit' eventually_at_topological assms
+ by blast
+
subsection \<open>Uniform limit theorem\<close>
@@ -998,27 +1002,98 @@
fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
assumes "r < conv_radius a"
shows "uniform_limit (cball \<xi> r) (\<lambda>n x. \<Sum>i<n. a i * (x - \<xi>) ^ i) (\<lambda>x. suminf (\<lambda>i. a i * (x - \<xi>) ^ i)) sequentially"
-using powser_uniformly_convergent [OF assms]
-by (simp add: Uniform_Limit.uniformly_convergent_uniform_limit_iff Series.suminf_eq_lim)
+ using powser_uniformly_convergent [OF assms]
+ by (simp add: Uniform_Limit.uniformly_convergent_uniform_limit_iff Series.suminf_eq_lim)
lemma powser_continuous_suminf:
fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
assumes "r < conv_radius a"
shows "continuous_on (cball \<xi> r) (\<lambda>x. suminf (\<lambda>i. a i * (x - \<xi>) ^ i))"
-apply (rule uniform_limit_theorem [OF _ powser_uniform_limit])
-apply (rule eventuallyI continuous_intros assms)+
-apply auto
-done
+ apply (rule uniform_limit_theorem [OF _ powser_uniform_limit])
+ apply (rule eventuallyI continuous_intros assms)+
+ apply auto
+ done
lemma powser_continuous_sums:
fixes a :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}"
assumes r: "r < conv_radius a"
- and sm: "\<And>x. x \<in> cball \<xi> r \<Longrightarrow> (\<lambda>n. a n * (x - \<xi>) ^ n) sums (f x)"
+ and sm: "\<And>x. x \<in> cball \<xi> r \<Longrightarrow> (\<lambda>n. a n * (x - \<xi>) ^ n) sums (f x)"
shows "continuous_on (cball \<xi> r) f"
-apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
-using sm sums_unique by fastforce
+ apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
+ using sm sums_unique by fastforce
lemmas uniform_limit_subset_union = uniform_limit_on_subset[OF uniform_limit_on_Union]
+subsection \<open>Tannery's Theorem\<close>
+
+text \<open>
+ Tannery's Theorem proves that, under certain boundedness conditions:
+ \[ \lim_{x\to\bar x} \sum_{k=0}^\infty f(k,n) = \sum_{k=0}^\infty \lim_{x\to\bar x} f(k,n) \]
+\<close>
+lemma tannerys_theorem:
+ fixes a :: "nat \<Rightarrow> _ \<Rightarrow> 'a :: {real_normed_algebra, banach}"
+ assumes limit: "\<And>k. ((\<lambda>n. a k n) \<longlongrightarrow> b k) F"
+ assumes bound: "eventually (\<lambda>(k,n). norm (a k n) \<le> M k) (at_top \<times>\<^sub>F F)"
+ assumes "summable M"
+ assumes [simp]: "F \<noteq> bot"
+ shows "eventually (\<lambda>n. summable (\<lambda>k. norm (a k n))) F \<and>
+ summable (\<lambda>n. norm (b n)) \<and>
+ ((\<lambda>n. suminf (\<lambda>k. a k n)) \<longlongrightarrow> suminf b) F"
+proof (intro conjI allI)
+ show "eventually (\<lambda>n. summable (\<lambda>k. norm (a k n))) F"
+ proof -
+ have "eventually (\<lambda>n. eventually (\<lambda>k. norm (a k n) \<le> M k) at_top) F"
+ using eventually_eventually_prod_filter2[OF bound] by simp
+ thus ?thesis
+ proof eventually_elim
+ case (elim n)
+ show "summable (\<lambda>k. norm (a k n))"
+ proof (rule summable_comparison_test_ev)
+ show "eventually (\<lambda>k. norm (norm (a k n)) \<le> M k) at_top"
+ using elim by auto
+ qed fact
+ qed
+ qed
+
+ have bound': "eventually (\<lambda>k. norm (b k) \<le> M k) at_top"
+ proof -
+ have "eventually (\<lambda>k. eventually (\<lambda>n. norm (a k n) \<le> M k) F) at_top"
+ using eventually_eventually_prod_filter1[OF bound] by simp
+ thus ?thesis
+ proof eventually_elim
+ case (elim k)
+ show "norm (b k) \<le> M k"
+ proof (rule tendsto_upperbound)
+ show "((\<lambda>n. norm (a k n)) \<longlongrightarrow> norm (b k)) F"
+ by (intro tendsto_intros limit)
+ qed (use elim in auto)
+ qed
+ qed
+ show "summable (\<lambda>n. norm (b n))"
+ by (rule summable_comparison_test_ev[OF _ \<open>summable M\<close>]) (use bound' in auto)
+
+ from bound obtain Pf Pg where
+ *: "eventually Pf at_top" "eventually Pg F" "\<And>k n. Pf k \<Longrightarrow> Pg n \<Longrightarrow> norm (a k n) \<le> M k"
+ unfolding eventually_prod_filter by auto
+
+ show "((\<lambda>n. \<Sum>k. a k n) \<longlongrightarrow> (\<Sum>k. b k)) F"
+ proof (rule swap_uniform_limit')
+ show "(\<lambda>K. (\<Sum>k<K. b k)) \<longlonglongrightarrow> (\<Sum>k. b k)"
+ using \<open>summable (\<lambda>n. norm (b n))\<close>
+ by (intro summable_LIMSEQ) (auto dest: summable_norm_cancel)
+ show "\<forall>\<^sub>F K in sequentially. ((\<lambda>n. \<Sum>k<K. a k n) \<longlongrightarrow> (\<Sum>k<K. b k)) F"
+ by (intro tendsto_intros always_eventually allI limit)
+ show "\<forall>\<^sub>F x in F. x \<in> {n. Pg n}"
+ using *(2) by simp
+ show "uniform_limit {n. Pg n} (\<lambda>K n. \<Sum>k<K. a k n) (\<lambda>n. \<Sum>k. a k n) sequentially"
+ proof (rule Weierstrass_m_test_ev)
+ show "\<forall>\<^sub>F k in at_top. \<forall>n\<in>{n. Pg n}. norm (a k n) \<le> M k"
+ using *(1) by eventually_elim (use *(3) in auto)
+ show "summable M"
+ by fact
+ qed
+ qed auto
+qed
+
end
--- a/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Computational_Algebra/Formal_Laurent_Series.thy Fri Apr 04 15:30:03 2025 +0200
@@ -912,6 +912,9 @@
instance fls :: (comm_monoid_add) comm_monoid_add
by (standard, transfer, auto simp: add.commute)
+lemma fls_nth_sum: "fls_nth (\<Sum>x\<in>A. f x) n = (\<Sum>x\<in>A. fls_nth (f x) n)"
+ by (induction A rule: infinite_finite_induct) auto
+
subsubsection \<open>Subtraction and negatives\<close>
@@ -2923,6 +2926,20 @@
by simp_all
qed
+lemma one_plus_fls_X_powi_eq:
+ "(1 + fls_X) powi n = fps_to_fls (fps_binomial (of_int n :: 'a :: field_char_0))"
+proof (cases "n \<ge> 0")
+ case True
+ thus ?thesis
+ using fps_binomial_of_nat[of "nat n", where ?'a = 'a]
+ by (simp add: power_int_def fps_to_fls_power)
+next
+ case False
+ thus ?thesis
+ using fps_binomial_minus_of_nat[of "nat (-n)", where ?'a = 'a]
+ by (simp add: power_int_def fps_to_fls_power fps_inverse_power flip: fls_inverse_fps_to_fls)
+qed
+
instance fls :: (field) field
by (standard, simp_all add: field_simps)
--- a/src/HOL/Deriv.thy Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Deriv.thy Fri Apr 04 15:30:03 2025 +0200
@@ -1130,18 +1130,19 @@
using DERIV_power [OF DERIV_ident] by simp
lemma DERIV_power_int [derivative_intros]:
- assumes [derivative_intros]: "(f has_field_derivative d) (at x within s)" and [simp]: "f x \<noteq> 0"
+ assumes [derivative_intros]: "(f has_field_derivative d) (at x within s)"
+ and "n \<ge> 0 \<or> f x \<noteq> 0"
shows "((\<lambda>x. power_int (f x) n) has_field_derivative
(of_int n * power_int (f x) (n - 1) * d)) (at x within s)"
proof (cases n rule: int_cases4)
case (nonneg n)
thus ?thesis
- by (cases "n = 0")
- (auto intro!: derivative_eq_intros simp: field_simps power_int_diff
- simp flip: power_Suc power_Suc2 power_add)
+ by (cases "n = 0"; cases "f x = 0")
+ (auto intro!: derivative_eq_intros simp: field_simps power_int_diff
+ power_diff power_int_0_left_if)
next
case (neg n)
- thus ?thesis
+ thus ?thesis using assms(2)
by (auto intro!: derivative_eq_intros simp: field_simps power_int_diff power_int_minus
simp flip: power_Suc power_Suc2 power_add)
qed
--- a/src/HOL/Filter.thy Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Filter.thy Fri Apr 04 15:30:03 2025 +0200
@@ -1132,6 +1132,38 @@
by (intro exI[of _ P] exI[of _ "\<lambda>x. True"]) auto
qed
+lemma eventually_eventually_prod_filter1:
+ assumes "eventually P (F \<times>\<^sub>F G)"
+ shows "eventually (\<lambda>x. eventually (\<lambda>y. P (x, y)) G) F"
+proof -
+ from assms obtain Pf Pg where
+ *: "eventually Pf F" "eventually Pg G" "\<And>x y. Pf x \<Longrightarrow> Pg y \<Longrightarrow> P (x, y)"
+ unfolding eventually_prod_filter by auto
+ show ?thesis
+ using *(1)
+ proof eventually_elim
+ case x: (elim x)
+ show ?case
+ using *(2) by eventually_elim (use x *(3) in auto)
+ qed
+qed
+
+lemma eventually_eventually_prod_filter2:
+ assumes "eventually P (F \<times>\<^sub>F G)"
+ shows "eventually (\<lambda>y. eventually (\<lambda>x. P (x, y)) F) G"
+proof -
+ from assms obtain Pf Pg where
+ *: "eventually Pf F" "eventually Pg G" "\<And>x y. Pf x \<Longrightarrow> Pg y \<Longrightarrow> P (x, y)"
+ unfolding eventually_prod_filter by auto
+ show ?thesis
+ using *(2)
+ proof eventually_elim
+ case y: (elim y)
+ show ?case
+ using *(1) by eventually_elim (use y *(3) in auto)
+ qed
+qed
+
lemma INF_filter_bot_base:
fixes F :: "'a \<Rightarrow> 'b filter"
assumes *: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. F k \<le> F i \<sqinter> F j"
--- a/src/HOL/Fun.thy Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Fun.thy Fri Apr 04 15:30:03 2025 +0200
@@ -368,6 +368,15 @@
lemma bij_betw_singletonI [intro]: "f x = y \<Longrightarrow> bij_betw f {x} {y}"
by auto
+lemma bij_betw_imp_empty_iff: "bij_betw f A B \<Longrightarrow> A = {} \<longleftrightarrow> B = {}"
+ unfolding bij_betw_def by blast
+
+lemma bij_betw_imp_Ex_iff: "bij_betw f {x. P x} {x. Q x} \<Longrightarrow> (\<exists>x. P x) \<longleftrightarrow> (\<exists>x. Q x)"
+ unfolding bij_betw_def by blast
+
+lemma bij_betw_imp_Bex_iff: "bij_betw f {x\<in>A. P x} {x\<in>B. Q x} \<Longrightarrow> (\<exists>x\<in>A. P x) \<longleftrightarrow> (\<exists>x\<in>B. Q x)"
+ unfolding bij_betw_def by blast
+
lemma bij_betw_apply: "\<lbrakk>bij_betw f A B; a \<in> A\<rbrakk> \<Longrightarrow> f a \<in> B"
unfolding bij_betw_def by auto
--- a/src/HOL/Groups_Big.thy Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Groups_Big.thy Fri Apr 04 15:30:03 2025 +0200
@@ -1580,6 +1580,16 @@
qed
qed
+lemma prod_uminus: "(\<Prod>x\<in>A. -f x :: 'a :: comm_ring_1) = (-1) ^ card A * (\<Prod>x\<in>A. f x)"
+ by (induction A rule: infinite_finite_induct) (auto simp: algebra_simps)
+
+lemma prod_diff:
+ fixes f :: "'a \<Rightarrow> 'b :: field"
+ assumes "finite A" "B \<subseteq> A" "\<And>x. x \<in> B \<Longrightarrow> f x \<noteq> 0"
+ shows "prod f (A - B) = prod f A / prod f B"
+ by (metis assms finite_subset nonzero_eq_divide_eq prod.subset_diff
+ prod_zero_iff)
+
lemma sum_zero_power [simp]: "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
for c :: "nat \<Rightarrow> 'a::division_ring"
by (induct A rule: infinite_finite_induct) auto
@@ -1712,10 +1722,22 @@
for y :: "'a::comm_monoid_mult"
by (induct A rule: infinite_finite_induct) simp_all
+lemma prod_diff_swap:
+ fixes f :: "'a \<Rightarrow> 'b :: comm_ring_1"
+ shows "prod (\<lambda>x. f x - g x) A = (-1) ^ card A * prod (\<lambda>x. g x - f x) A"
+ using prod.distrib[of "\<lambda>_. -1" "\<lambda>x. f x - g x" A]
+ by simp
+
lemma prod_power_distrib: "prod f A ^ n = prod (\<lambda>x. (f x) ^ n) A"
for f :: "'a \<Rightarrow> 'b::comm_semiring_1"
by (induct A rule: infinite_finite_induct) (auto simp add: power_mult_distrib)
+lemma power_inject_exp':
+ assumes "a \<noteq> 1" "a > (0 :: 'a :: linordered_semidom)"
+ shows "a ^ m = a ^ n \<longleftrightarrow> m = n"
+ by (metis assms not_less_iff_gr_or_eq order_le_less power_decreasing_iff
+ power_inject_exp)
+
lemma power_sum: "c ^ (\<Sum>a\<in>A. f a) = (\<Prod>a\<in>A. c ^ f a)"
by (induct A rule: infinite_finite_induct) (simp_all add: power_add)
--- a/src/HOL/Library/Infinite_Typeclass.thy Wed Apr 02 11:26:40 2025 +0200
+++ b/src/HOL/Library/Infinite_Typeclass.thy Fri Apr 04 15:30:03 2025 +0200
@@ -27,6 +27,9 @@
by auto
qed
+lemma arb_inj_on_finite_infinite: "finite(A :: 'b set) \<Longrightarrow> \<exists>f :: 'b \<Rightarrow> 'a. inj_on f A"
+by (meson arb_finite_subset card_le_inj infinite_imp_nonempty)
+
lemma arb_countable_map: "finite Y \<Longrightarrow> \<exists>f :: (nat \<Rightarrow> 'a). inj f \<and> range f \<subseteq> UNIV - Y"
using infinite_UNIV
by (auto simp: infinite_countable_subset)