OAI/NumberTheory/JointDickman/Amplification/RealDistanceDivergence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform distance separation for bounded real coefficients

  1. lemma OAI.JointDickman.real_primeDistance_lower line 10
  2. theorem OAI.JointDickman.real_primeDistance_diverges line 39

    Source documentation

    The bound is uniform in the real coefficients, including scale-dependent bin interpolants. Multiplicativity is not needed for this distance bound.

    theorem real_primeDistance_diverges (R : ℝ) :
    ∀ᶠ X : ℝ in atTop, ∀ (f : ArithmeticFunction ℂ),
      (∀ n, ‖f n‖ ≤ 1) → (∀ n, (f n).im = 0) →
      ∀ t : ℝ, 1 ≤ |t| → |t| ≤ X → R ≤ primeDistanceSquared f X t := by
…