OAI/NumberTheory/Ostmann/Preliminaries/MertensHarmonicBands.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Mertens' second theorem on the iterated-logarithm band

F. Mertens, Ein Beitrag zur analytischen Zahlentheorie, J. reine angew. Math. 78 (1874), 46–62, second theorem. We only require its weaker bounded error consequence sum_{p≤Q} 1/p = log log Q + O(1). The pinned PNT library states this specialization as Mertens.sum_prime_div_eq_log_log.

  1. def OAI.Ostmann.MertensHarmonicEstimate line 19

    Source documentation

    Precise published Mertens-second input, weaker than its convergent-error form and sufficient for the favorable-prime harmonic mass.

    def MertensHarmonicEstimate (C : ℝ) : Prop :=
…
  2. def OAI.Ostmann.logLogPrimeBand line 22
  3. theorem OAI.Ostmann.floor_exp_loglog_bounds line 26
  4. theorem OAI.Ostmann.logLogPrimeBand_mem line 50
  5. theorem OAI.Ostmann.logLogPrimeBand_harmonic_lower line 66
  6. theorem OAI.Ostmann.logLogPrimeBand_harmonic_upper line 85
  7. theorem OAI.Ostmann.eventual_logLogPrimeBand_harmonic_le line 104