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