The Divergence of the Prime Harmonic Series

In this work, we prove the lower bound ln(Hn)−ln(5 3 ) for the partial sum of the Prime Harmonic series and, based on this, the divergence of the Prime Harmonic Series n p=1[p prime] · 1 p . The proof relies on the unique squarefree decomposition of natural numbers. This proof is similar to Euler’s original proof (which was highly informal and morally questionable). Its advantage over proofs by contradiction, like the famous one by Paul Erd˝os, is that it provides a relatively good lower bound for the partial sums. Contents 1 Auxiliary lemmas 1 2 Squarefree decomposition of natural numbers 2 3 The Prime Harmonic Series 4 3.1 Auxiliary equalities and inequalities . . . . . . . . . . . . . . 4 3.2 Estimating the partial sums of the Prime Harmonic Series . . 5 1 Auxiliary lemmas theory Prime-Harmonic-Misc imports Complex-Main ∼∼ /src/HOL/Number-Theory/Number-Theory begin lemma listsum-nonneg: ∀ x∈set xs. x ≥ 0 =⇒ listsum xs ≥ (0 :: a :: ordered-ab-group-add) proof lem...

• Type: Journal
• Year: 2015
• Where: AFP
• Authors: Manuel Eberl
• Keywords: AFP 2015, Formal Methods