OAI/NumberTheory/Ostmann/Construction/PrimeLogLogIntervalMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform harmonic mass bounds in the iterated-log coordinate

Only the upper half of the already recorded Mertens input is needed here. The constant need not be sharp: a uniform density ceiling suffices for the finite density-increment selection.

  1. theorem OAI.Ostmann.prime_loglog_unit_mass_upper line 17
  2. theorem OAI.Ostmann.prime_loglog_interval_mass_upper line 63

    Source documentation

    This applies to every subset of the primes, uniformly in its choice.

    theorem prime_loglog_interval_mass_upper {C : ℝ} (hM : MertensEstimate C)
    (P : Finset ℕ) (hP : ∀ p ∈ P, p.Prime)
    (a b : ℝ) (ha : max C 0 ≤ a) (hab : a ≤ b) :
    weightedIntervalMass P (fun p => Real.log (Real.log p)) (fun p => (p : ℝ)⁻¹)
      a b ≤ (Real.exp 1 + 1) * (b - a + 1) := by
…

    Mentions: OAI.Ostmann.MertensEstimate, OAI.Ostmann.weightedIntervalMass