# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1751638089 -3600
# Node ID 982e7128ce0f5d3f9117b8a4e15a42147119b1c3
# Parent  547335b410054f9a7dc82d91762fd9d79cd671e1
Two lemmas and a comment

diff -r 547335b41005 -r 982e7128ce0f src/HOL/Analysis/Kronecker_Approximation_Theorem.thy
--- a/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy	Thu Jul 03 13:53:14 2025 +0200
+++ b/src/HOL/Analysis/Kronecker_Approximation_Theorem.thy	Fri Jul 04 15:08:09 2025 +0100
@@ -87,6 +87,8 @@
   qed (use \<open>a < b\<close> in auto)
 qed
 
+text \<open>Theorem references below referr to Apostol, 
+  \emph{Modular Functions and Dirichlet Series in Number Theory}\<close>
 
 text \<open>Theorem 7.1\<close>
 corollary Dirichlet_approx:
diff -r 547335b41005 -r 982e7128ce0f src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Thu Jul 03 13:53:14 2025 +0200
+++ b/src/HOL/Complex.thy	Fri Jul 04 15:08:09 2025 +0100
@@ -807,6 +807,10 @@
 lemma complex_is_Real_iff: "z \<in> \<real> \<longleftrightarrow> Im z = 0"
   by (auto simp: Reals_def complex_eq_iff)
 
+lemma sgn_complex_iff: "sgn x = sgn (Re x) \<longleftrightarrow> x \<in> \<real>"
+  by (metis Im_complex_of_real Im_sgn Reals_0 complex_is_Real_iff divide_eq_0_iff 
+      norm_eq_zero of_real_Re sgn_of_real)
+
 lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
   by (auto simp: complex_is_Real_iff complex_eq_iff)
 
@@ -1417,6 +1421,21 @@
 lemma csqrt_of_real': "csqrt (of_real x) = of_real (sqrt \<bar>x\<bar>) * (if x \<ge> 0 then 1 else \<i>)"
   by (rule csqrt_unique) (auto simp flip: of_real_power simp: power_mult_distrib)
 
+lemma csqrt_minus_Reals:
+  assumes "x \<in> \<real>"
+  shows "csqrt (- x) = sgn (Re x) * \<i> * csqrt x"
+proof (cases "Re x \<ge> 0")
+  case True
+  then show ?thesis
+    using assms complex_is_Real_iff sgn_1_pos by force
+next
+  case False
+  then obtain "Im x = 0" "sgn (Re x) = -1"
+    using assms complex_is_Real_iff by auto
+  with False show ?thesis
+    by auto
+qed
+
 lemmas cmod_def = norm_complex_def
 
 lemma Complex_simps: