# HG changeset patch
# User wenzelm
# Date 1752609906 -7200
# Node ID fa1c57d4269987f193dceaa7a8694ff9eec4ac60
# Parent  3e1521dc095df327e956f30ec23b8bf27ab9430b# Parent  d19f589fe9ad46bc27ace846044a69d1df99d9e9
merged

diff -r d19f589fe9ad -r fa1c57d42699 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jul 15 14:25:30 2025 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Jul 15 22:05:06 2025 +0200
@@ -284,6 +284,12 @@
 lemma exp_plus_2pin [simp]: "exp (z + \<i> * (of_int n * (of_real pi * 2))) = exp z"
   by (simp add: exp_eq)
 
+lemma exp_2pi_1_int [simp]: "exp (\<i> * (of_int j * (of_real pi * 2))) = 1"
+  by (metis exp_add exp_not_eq_zero exp_plus_2pin mult_cancel_left1)
+
+lemma exp_2pi_1_nat [simp]: "exp (\<i> * (of_nat j * (of_real pi * 2))) = 1"
+  by (metis exp_2pi_1_int of_int_of_nat_eq)
+
 lemma exp_integer_2pi_plus1:
   assumes "n \<in> \<int>"
   shows "exp(((2 * n + 1) * pi) * \<i>) = - 1"
@@ -2408,6 +2414,24 @@
   fixes x::complex shows "x powr (numeral n) = x ^ (numeral n)"
   by (metis of_nat_numeral power_zero_numeral powr_nat)
 
+lemma powr_times_real_left:
+  assumes "x \<in> \<real>" "Re x \<ge> 0"
+  shows   "(x * y) powr z = x powr z * y powr z"
+proof (cases "x = 0 \<or> y = 0")
+  case nz: False
+  from assms obtain t where x_eq: "x = of_real t" and "t \<ge> 0"  "t \<noteq> 0"
+    by (metis nz of_real_0 of_real_Re)
+  with \<open>t \<ge> 0\<close> have t: "t > 0"
+    by simp
+  have "(x * y) powr z = exp (z * ln (of_real t * y))"
+    using nz by (simp add: powr_def x_eq)
+  also have "ln (of_real t * y) = ln x + ln y"
+    by (subst Ln_times_of_real) (use t nz in \<open>auto simp: x_eq\<close>)
+  also have "exp (z * \<dots>) = x powr z * y powr z"
+    using nz by (simp add: powr_def ring_distribs exp_add)
+  finally show ?thesis .
+qed auto
+
 lemma cnj_powr:
   assumes "Im a = 0 \<Longrightarrow> Re a \<ge> 0"
   shows   "cnj (a powr b) = cnj a powr cnj b"
@@ -2441,7 +2465,27 @@
 lemma complex_powr_of_int: "z \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> z powr of_int n = (z :: complex) powi n"
   by (cases "z = 0 \<or> n = 0")
      (auto simp: power_int_def powr_minus powr_nat powr_of_int power_0_left power_inverse)
-  
+
+lemma powr_of_neg_real:
+  fixes x::real and y::real
+  assumes "x<0"
+  shows "(complex_of_real x) powr (complex_of_real y) = of_real (\<bar>x\<bar> powr y) * exp (\<i> * pi * y)"
+proof -
+  have "complex_of_real x powr (complex_of_real y) = (\<bar>x\<bar> * exp (\<i> * pi)) powr y"
+    using assms by auto
+  also have "... = of_real (\<bar>x\<bar> powr y) * exp (\<i> * pi) powr y"
+    by (metis Re_complex_of_real Reals_of_real abs_ge_zero powr_of_real powr_times_real_left)
+  also have "... = of_real (\<bar>x\<bar> powr y) * exp (\<i> * pi * y)"
+    by (simp add: mult.commute powr_def)
+  finally show ?thesis .
+qed
+
+lemma powr_of_real_if:
+  fixes x::real and y::real
+  shows "complex_of_real x powr (complex_of_real y) = 
+           (if x<0 then of_real (\<bar>x\<bar> powr y) * exp (\<i> * pi * y) else of_real (x powr y))"
+  by (simp add: powr_of_neg_real powr_of_real)
+
 lemma powr_Reals_eq: "\<lbrakk>x \<in> \<real>; y \<in> \<real>; Re x \<ge> 0\<rbrakk> \<Longrightarrow> x powr y = of_real (Re x powr Re y)"
   by (metis of_real_Re powr_of_real)
 
diff -r d19f589fe9ad -r fa1c57d42699 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Jul 15 14:25:30 2025 +0200
+++ b/src/HOL/Complex.thy	Tue Jul 15 22:05:06 2025 +0200
@@ -349,6 +349,12 @@
 
 declare uniformity_Abort[where 'a = complex, code]
 
+lemma Re_divide': "Re (x / y) = (Re x * Re y + Im x * Im y) / (norm y)\<^sup>2"
+  by (simp add: Re_divide norm_complex_def)
+
+lemma Im_divide': "Im (x / y) = (Im x * Re y - Re x * Im y) / (norm y)\<^sup>2"
+  by (simp add: Im_divide norm_complex_def)
+
 lemma norm_ii [simp]: "norm \<i> = 1"
   by (simp add: norm_complex_def)
 
diff -r d19f589fe9ad -r fa1c57d42699 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Jul 15 14:25:30 2025 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Tue Jul 15 22:05:06 2025 +0200
@@ -956,6 +956,18 @@
 
 end
 
+lemma dist_sum_le:
+  fixes f :: "'a \<Rightarrow> 'b :: real_normed_vector"
+  shows "dist (\<Sum>x\<in>A. f x) (\<Sum>x\<in>A. g x) \<le> (\<Sum>x\<in>A. dist (f x) (g x))"
+proof -
+  have "dist (\<Sum>x\<in>A. f x) (\<Sum>x\<in>A. g x) = norm (\<Sum>x\<in>A. f x - g x)"
+    by (simp add: dist_norm sum_subtractf)
+  also have "\<dots> \<le> (\<Sum>x\<in>A. norm (f x - g x))"
+    by (rule norm_sum)
+  finally show ?thesis
+    by (simp add: dist_norm)
+qed
+
 lemma dist_scaleR [simp]: "dist (x *\<^sub>R a) (y *\<^sub>R a) = \<bar>x - y\<bar> * norm a"
   for a :: "'a::real_normed_vector"
   by (metis dist_norm norm_scaleR scaleR_left.diff)
diff -r d19f589fe9ad -r fa1c57d42699 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue Jul 15 14:25:30 2025 +0200
+++ b/src/HOL/Series.thy	Tue Jul 15 22:05:06 2025 +0200
@@ -29,9 +29,7 @@
 text\<open>Variants of the definition\<close>
 lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s"
   unfolding sums_def
-  apply (subst filterlim_sequentially_Suc [symmetric])
-  apply (simp only: lessThan_Suc_atMost atLeast0AtMost)
-  done
+  using LIMSEQ_lessThan_iff_atMost atMost_atLeast0 by auto
 
 lemma sums_def_le: "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i) \<longlonglongrightarrow> s"
   by (simp add: sums_def' atMost_atLeast0)
@@ -1034,13 +1032,14 @@
   finally show ?thesis .
 qed
 
+lemma norm_sums_le:
+  assumes "f sums F" "g sums G"
+  assumes "\<And>n. norm (f n :: 'a :: banach) \<le> g n"
+  shows   "norm F \<le> G"
+  using assms by (metis norm_suminf_le sums_iff)
+
 lemma summable_zero_power [simp]: "summable (\<lambda>n. 0 ^ n :: 'a::{comm_ring_1,topological_space})"
-proof -
-  have "(\<lambda>n. 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then 0^0 else 0)"
-    by (intro ext) (simp add: zero_power)
-  moreover have "summable \<dots>" by simp
-  ultimately show ?thesis by simp
-qed
+  by (simp add: power_0_left)
 
 lemma summable_zero_power' [simp]: "summable (\<lambda>n. f n * 0 ^ n :: 'a::{ring_1,topological_space})"
 proof -