OAI/NumberTheory/Ostmann/Construction/RoundedTailScale.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Integer endpoints for a whole harmonic prime band at every real scale

  1. theorem OAI.Ostmann.eventual_rounded_tail_scale line 11

    Source documentation

    Choose a literal integer endpoint above the band, while retaining a linear bound on the logarithm of its logarithm.

    theorem eventual_rounded_tail_scale (β : ℝ) (hβ : 0 < β) (T₀ : ℝ) :
    ∀ᶠ L : ℝ in atTop, ∃ (X : ℕ) (T : ℝ), T₀ ≤ T ∧
      (X : ℝ) = Real.exp T ∧
      Real.log T ≤ (β + 1) * L + Real.log 1000 ∧
      Real.exp (β * L) ≤ T / 4 := by
…