# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1742851443 0
# Node ID 1eb12389c49995f016f29dfc181ee0551a119090
# Parent  3ae491533076134d3dcc8c431b14b2cf0420708e
New material by Manuel Eberl

diff -r 3ae491533076 -r 1eb12389c499 src/HOL/Analysis/Complex_Transcendental.thy
--- 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:
diff -r 3ae491533076 -r 1eb12389c499 src/HOL/Analysis/FPS_Convergence.thy
--- 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
diff -r 3ae491533076 -r 1eb12389c499 src/HOL/Complex_Analysis/Laurent_Convergence.thy
--- 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)
diff -r 3ae491533076 -r 1eb12389c499 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- 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>
 
diff -r 3ae491533076 -r 1eb12389c499 src/HOL/Filter.thy
--- 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))"
diff -r 3ae491533076 -r 1eb12389c499 src/HOL/Limits.thy
--- 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"
diff -r 3ae491533076 -r 1eb12389c499 src/HOL/Topological_Spaces.thy
--- 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>