--- 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"
--- 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)
--- 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 -