--- a/src/HOL/Analysis/Complex_Transcendental.thy Mon Mar 24 14:29:52 2025 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Mon Mar 24 21:24:03 2025 +0000
@@ -2605,10 +2605,21 @@
thus ?thesis by simp
qed
-lemma continuous_powr_complex:
- assumes "f (netlimit F) \<notin> \<real>\<^sub>\<le>\<^sub>0" "continuous F f" "continuous F g"
+lemma continuous_powr_complex [continuous_intros]:
+ assumes "continuous F f" "continuous F g"
+ assumes "Re (f (netlimit F)) \<ge> 0 \<or> Im (f (netlimit F)) \<noteq> 0"
+ assumes "f (netlimit F) = 0 \<longrightarrow> Re (g (netlimit F)) > 0"
shows "continuous F (\<lambda>z. f z powr g z :: complex)"
- using assms unfolding continuous_def by (intro tendsto_powr_complex) simp_all
+ using assms
+ unfolding continuous_def
+ by (intro tendsto_powr_complex')
+ (auto simp: complex_nonpos_Reals_iff complex_eq_iff)
+
+lemma continuous_powr_real [continuous_intros]:
+ assumes "continuous F f" "continuous F g"
+ assumes "f (netlimit F) = 0 \<longrightarrow> g (netlimit F) > 0 \<and> (\<forall>\<^sub>F z in F. 0 \<le> f z)"
+ shows "continuous F (\<lambda>z. f z powr g z :: real)"
+ using assms unfolding continuous_def by (intro tendsto_intros) auto
lemma isCont_powr_complex [continuous_intros]:
assumes "f z \<notin> \<real>\<^sub>\<le>\<^sub>0" "isCont f z" "isCont g z"
@@ -2637,6 +2648,43 @@
qed
qed
+lemma analytic_on_powr [analytic_intros]:
+ assumes "f analytic_on X" "g analytic_on X" "\<And>x. x \<in> X \<Longrightarrow> f x \<notin> \<real>\<^sub>\<le>\<^sub>0"
+ shows "(\<lambda>x. f x powr g x) analytic_on X"
+proof -
+ from assms(1) obtain X1 where X1: "open X1" "X \<subseteq> X1" "f analytic_on X1"
+ unfolding analytic_on_holomorphic by blast
+ from assms(2) obtain X2 where X2: "open X2" "X \<subseteq> X2" "g analytic_on X2"
+ unfolding analytic_on_holomorphic by blast
+ have X: "open (X2 \<inter> (X1 \<inter> f -` (-\<real>\<^sub>\<le>\<^sub>0)))"
+ by (rule open_Int[OF _ continuous_open_preimage])
+ (use X1 X2 in \<open>auto intro!: holomorphic_on_imp_continuous_on analytic_imp_holomorphic\<close>)
+ have X': "X \<subseteq> X2 \<inter> (X1 \<inter> f -` (-\<real>\<^sub>\<le>\<^sub>0))"
+ using assms(3) X1(2) X2(2) by blast
+ note [holomorphic_intros] =
+ analytic_imp_holomorphic[OF analytic_on_subset[OF X1(3)]]
+ analytic_imp_holomorphic[OF analytic_on_subset[OF X2(3)]]
+ have "(\<lambda>x. exp (ln (f x) * g x)) holomorphic_on (X2 \<inter> (X1 \<inter> f -` (-\<real>\<^sub>\<le>\<^sub>0)))"
+ by (intro holomorphic_intros) auto
+ also have "?this \<longleftrightarrow> (\<lambda>x. f x powr g x) holomorphic_on (X2 \<inter> (X1 \<inter> f -` (-\<real>\<^sub>\<le>\<^sub>0)))"
+ by (intro holomorphic_cong) (auto simp: powr_def mult.commute)
+ finally show ?thesis
+ using X X' unfolding analytic_on_holomorphic by blast
+qed
+
+lemma holomorphic_on_powr [holomorphic_intros]:
+ assumes "f holomorphic_on X" "g holomorphic_on X" "\<And>x. x \<in> X \<Longrightarrow> f x \<notin> \<real>\<^sub>\<le>\<^sub>0"
+ shows "(\<lambda>x. f x powr g x) holomorphic_on X"
+proof -
+ have [simp]: "f x \<noteq> 0" if "x \<in> X" for x
+ using assms(3)[OF that] by auto
+ have "(\<lambda>x. exp (ln (f x) * g x)) holomorphic_on X"
+ by (auto intro!: holomorphic_intros assms(1,2)) (use assms(3) in auto)
+ also have "?this \<longleftrightarrow> ?thesis"
+ by (intro holomorphic_cong) (use assms(3) in \<open>auto simp: powr_def mult_ac\<close>)
+ finally show ?thesis .
+qed
+
subsection\<^marker>\<open>tag unimportant\<close>\<open>Some Limits involving Logarithms\<close>
lemma lim_Ln_over_power:
--- a/src/HOL/Analysis/FPS_Convergence.thy Mon Mar 24 14:29:52 2025 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy Mon Mar 24 21:24:03 2025 +0000
@@ -1057,4 +1057,34 @@
by (intro that[of ?s']) (auto simp: has_fps_expansion_def zero_ereal_def)
qed
+lemma has_fps_expansionI:
+ fixes f :: "'a :: {banach, real_normed_div_algebra} \<Rightarrow> 'a"
+ assumes "eventually (\<lambda>u. (\<lambda>n. fps_nth F n * u ^ n) sums f u) (nhds 0)"
+ shows "f has_fps_expansion F"
+proof -
+ from assms obtain X where X: "open X" "0 \<in> X" "\<And>u. u \<in> X \<Longrightarrow> (\<lambda>n. fps_nth F n * u ^ n) sums f u"
+ unfolding eventually_nhds by blast
+ obtain r where r: "r > 0" "cball 0 r \<subseteq> X"
+ using X(1,2) open_contains_cball by blast
+ have "0 < norm (of_real r :: 'a)"
+ using r(1) by simp
+ also have "fps_conv_radius F \<ge> norm (of_real r :: 'a)"
+ unfolding fps_conv_radius_def
+ proof (rule conv_radius_geI)
+ have "of_real r \<in> X"
+ using r by auto
+ from X(3)[OF this] show "summable (\<lambda>n. fps_nth F n * of_real r ^ n)"
+ by (simp add: sums_iff)
+ qed
+ finally have "fps_conv_radius F > 0"
+ by (simp_all add: zero_ereal_def)
+ moreover have "(\<forall>\<^sub>F z in nhds 0. eval_fps F z = f z)"
+ using assms by eventually_elim (auto simp: sums_iff eval_fps_def)
+ ultimately show ?thesis
+ unfolding has_fps_expansion_def ..
+qed
+
+lemma fps_mult_numeral_left [simp]: "fps_nth (numeral c * f) n = numeral c * fps_nth f n"
+ by (simp add: fps_numeral_fps_const)
+
end
\ No newline at end of file
--- a/src/HOL/Complex_Analysis/Laurent_Convergence.thy Mon Mar 24 14:29:52 2025 +0100
+++ b/src/HOL/Complex_Analysis/Laurent_Convergence.thy Mon Mar 24 21:24:03 2025 +0000
@@ -385,6 +385,43 @@
using Suc by simp
qed auto
+lemma eval_fls_eq:
+ assumes "N \<le> fls_subdegree F" "fls_subdegree F \<ge> 0 \<or> z \<noteq> 0"
+ assumes "(\<lambda>n. fls_nth F (int n + N) * z powi (int n + N)) sums S"
+ shows "eval_fls F z = S"
+proof (cases "z = 0")
+ case [simp]: True
+ have "(\<lambda>n. fls_nth F (int n + N) * z powi (int n + N)) =
+ (\<lambda>n. if n \<in> (if N \<le> 0 then {nat (-N)} else {}) then fls_nth F (int n + N) else 0)"
+ by (auto simp: fun_eq_iff split: if_splits)
+ also have "\<dots> sums (\<Sum>n\<in>(if N \<le> 0 then {nat (-N)} else {}). fls_nth F (int n + N))"
+ by (rule sums_If_finite_set) auto
+ also have "\<dots> = fls_nth F 0"
+ using assms by auto
+ also have "\<dots> = eval_fls F z"
+ using assms by (auto simp: eval_fls_def eval_fps_at_0 power_int_0_left_if)
+ finally show ?thesis
+ using assms by (simp add: sums_iff)
+next
+ case [simp]: False
+ define N' where "N' = fls_subdegree F"
+ define d where "d = nat (N' - N)"
+
+ have "(\<lambda>n. fls_nth F (int n + N) * z powi (int n + N)) sums S"
+ by fact
+ also have "?this \<longleftrightarrow> (\<lambda>n. fls_nth F (int (n+d) + N) * z powi (int (n+d) + N)) sums S"
+ by (rule sums_zero_iff_shift [symmetric]) (use assms in \<open>auto simp: d_def N'_def\<close>)
+ also have "(\<lambda>n. int (n+d) + N) = (\<lambda>n. int n + N')"
+ using assms by (auto simp: N'_def d_def)
+ finally have "(\<lambda>n. fls_nth F (int n + N') * z powi (int n + N')) sums S" .
+ hence "(\<lambda>n. z powi (-N') * (fls_nth F (int n + N') * z powi (int n + N'))) sums (z powi (-N') * S)"
+ by (intro sums_mult)
+ hence "(\<lambda>n. fls_nth F (int n + N') * z ^ n) sums (z powi (-N') * S)"
+ by (simp add: power_int_add power_int_minus field_simps)
+ thus ?thesis
+ by (simp add: eval_fls_def eval_fps_def sums_iff power_int_minus N'_def)
+qed
+
lemma norm_summable_fls:
"norm z < fls_conv_radius f \<Longrightarrow> summable (\<lambda>n. norm (fls_nth f n * z ^ n))"
using norm_summable_fps[of z "fls_regpart f"] by (simp add: fls_conv_radius_def)
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Mon Mar 24 14:29:52 2025 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Mon Mar 24 21:24:03 2025 +0000
@@ -5166,6 +5166,18 @@
"fps_compose f (-fps_X :: 'a :: comm_ring_1 fps) = Abs_fps (\<lambda>n. (-1)^n * f $ n)"
using fps_compose_linear[of f "-1"]
by (simp only: fps_const_neg [symmetric] fps_const_1_eq_1) simp
+lemma fps_nth_compose_linear [simp]:
+ fixes f :: "'a :: comm_ring_1 fps"
+ shows "fps_nth (fps_compose f (fps_const c * fps_X)) n = c ^ n * fps_nth f n"
+proof -
+ have "fps_nth (fps_compose f (fps_const c * fps_X)) n =
+ (\<Sum>i\<in>{n}. fps_nth f i * fps_nth ((fps_const c * fps_X) ^ i) n)"
+ unfolding fps_compose_nth
+ by (intro sum.mono_neutral_cong_right) (auto simp: power_mult_distrib)
+ also have "\<dots> = c ^ n * fps_nth f n"
+ by (simp add: power_mult_distrib)
+ finally show ?thesis .
+qed
subsection \<open>Elementary series\<close>
--- a/src/HOL/Filter.thy Mon Mar 24 14:29:52 2025 +0100
+++ b/src/HOL/Filter.thy Mon Mar 24 21:24:03 2025 +0000
@@ -966,6 +966,8 @@
definition finite_subsets_at_top where
"finite_subsets_at_top A = (\<Sqinter> X\<in>{X. finite X \<and> X \<subseteq> A}. principal {Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A})"
+abbreviation "finite_sets_at_top \<equiv> finite_subsets_at_top UNIV"
+
lemma eventually_finite_subsets_at_top:
"eventually P (finite_subsets_at_top A) \<longleftrightarrow>
(\<exists>X. finite X \<and> X \<subseteq> A \<and> (\<forall>Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A \<longrightarrow> P Y))"
--- a/src/HOL/Limits.thy Mon Mar 24 14:29:52 2025 +0100
+++ b/src/HOL/Limits.thy Mon Mar 24 21:24:03 2025 +0000
@@ -1266,9 +1266,9 @@
lemma continuous_on_power_int [continuous_intros]:
fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
- assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
+ assumes "continuous_on s f" and "n \<ge> 0 \<or> (\<forall>x\<in>s. f x \<noteq> 0)"
shows "continuous_on s (\<lambda>x. power_int (f x) n)"
- using assms unfolding continuous_on_def by (blast intro: tendsto_power_int)
+ using assms by (cases "n \<ge> 0") (auto simp: power_int_def intro!: continuous_intros)
lemma tendsto_power_int' [tendsto_intros]:
fixes a :: "'a::real_normed_div_algebra"
--- a/src/HOL/Topological_Spaces.thy Mon Mar 24 14:29:52 2025 +0100
+++ b/src/HOL/Topological_Spaces.thy Mon Mar 24 21:24:03 2025 +0000
@@ -359,6 +359,35 @@
by (fastforce intro: exI[of _ y] lt_ex)
qed
+lemma filterlim_atLeastAtMost_at_bot_at_top:
+ fixes f g :: "'a \<Rightarrow> 'b :: linorder_topology"
+ assumes "filterlim f at_bot F" "filterlim g at_top F"
+ assumes [simp]: "\<And>a b. finite {a..b::'b}"
+ shows "filterlim (\<lambda>x. {f x..g x}) finite_sets_at_top F"
+ unfolding filterlim_finite_subsets_at_top
+proof safe
+ fix X :: "'b set"
+ assume X: "finite X"
+ from X obtain lb where lb: "\<And>x. x \<in> X \<Longrightarrow> lb \<le> x"
+ by (metis finite_has_minimal2 nle_le)
+ from X obtain ub where ub: "\<And>x. x \<in> X \<Longrightarrow> x \<le> ub"
+ by (metis all_not_in_conv finite_has_maximal nle_le)
+ have "eventually (\<lambda>x. f x \<le> lb) F" "eventually (\<lambda>x. g x \<ge> ub) F"
+ using assms by (simp_all add: filterlim_at_bot filterlim_at_top)
+ thus "eventually (\<lambda>x. finite {f x..g x} \<and> X \<subseteq> {f x..g x} \<and> {f x..g x} \<subseteq> UNIV) F"
+ proof eventually_elim
+ case (elim x)
+ have "X \<subseteq> {f x..g x}"
+ proof
+ fix y assume "y \<in> X"
+ thus "y \<in> {f x..g x}"
+ using lb[of y] ub[of y] elim by auto
+ qed
+ thus ?case
+ by auto
+ qed
+qed
+
subsection \<open>Setup some topologies\<close>