# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1752514901 -3600
# Node ID 3e1521dc095df327e956f30ec23b8bf27ab9430b
# Parent  0b38dccd8cf59c514f72c95c020c93f535c350e9
A few more lemmas

diff -r 0b38dccd8cf5 -r 3e1521dc095d src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Mon Jul 14 12:33:34 2025 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Mon Jul 14 18:41:41 2025 +0100
@@ -2465,6 +2465,7 @@
 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"
diff -r 0b38dccd8cf5 -r 3e1521dc095d src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon Jul 14 12:33:34 2025 +0100
+++ b/src/HOL/Complex.thy	Mon Jul 14 18:41:41 2025 +0100
@@ -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 0b38dccd8cf5 -r 3e1521dc095d src/HOL/Series.thy
--- a/src/HOL/Series.thy	Mon Jul 14 12:33:34 2025 +0100
+++ b/src/HOL/Series.thy	Mon Jul 14 18:41:41 2025 +0100
@@ -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 -