Some facts on the Mangoldt function
authoreberlm <eberlm@in.tum.de>
Mon Dec 11 17:28:32 2017 +0100 (17 months ago)
changeset 67166a77d54ef718b
parent 67165 22a5822f52f7
child 67167 88d1c9d86f48
Some facts on the Mangoldt function
src/HOL/Number_Theory/Prime_Powers.thy
     1.1 --- a/src/HOL/Number_Theory/Prime_Powers.thy	Fri Dec 08 19:25:47 2017 +0000
     1.2 +++ b/src/HOL/Number_Theory/Prime_Powers.thy	Mon Dec 11 17:28:32 2017 +0100
     1.3 @@ -422,7 +422,13 @@
     1.4  
     1.5  definition mangoldt :: "nat \<Rightarrow> 'a :: real_algebra_1" where
     1.6    "mangoldt n = (if primepow n then of_real (ln (real (aprimedivisor n))) else 0)"
     1.7 -  
     1.8 +
     1.9 +lemma mangoldt_0 [simp]: "mangoldt 0 = 0"
    1.10 +  by (simp add: mangoldt_def)
    1.11 +
    1.12 +lemma mangoldt_Suc_0 [simp]: "mangoldt (Suc 0) = 0"
    1.13 +  by (simp add: mangoldt_def)
    1.14 +
    1.15  lemma of_real_mangoldt [simp]: "of_real (mangoldt n) = mangoldt n"
    1.16    by (simp add: mangoldt_def)
    1.17  
    1.18 @@ -481,6 +487,10 @@
    1.19    with True show ?thesis by (auto simp: mangoldt_def abs_if)
    1.20  qed (auto simp: mangoldt_def)
    1.21  
    1.22 +lemma Re_mangoldt [simp]: "Re (mangoldt n) = mangoldt n"
    1.23 +  and Im_mangoldt [simp]: "Im (mangoldt n) = 0"
    1.24 +  by (simp_all add: mangoldt_def)
    1.25 +
    1.26  lemma abs_mangoldt [simp]: "abs (mangoldt n :: real) = mangoldt n"
    1.27    using norm_mangoldt[of n, where ?'a = real, unfolded real_norm_def] .
    1.28