OAI/NumberTheory/TwoPoint/ShortIntervals/MRTMovingInverse.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The center normalization on shrinking disks costs only the reciprocal radius. This uses the absolutely convergent Möbius inverse and the proved residue of the Riemann zeta function; no zero-free hypothesis is used.

  1. lemma OAI.TwoPointCorrelations.mrt_character_inverse_real_majorant line 16
  2. theorem OAI.TwoPointCorrelations.mrt_moving_center_inverse line 51

    Source documentation

    The local center reciprocal has an absolute radius threshold, independent of the modulus, character and height.

    theorem mrt_moving_center_inverse : ∃ r₀ : ℝ, 0 < r₀ ∧ r₀ ≤ 1 / 4 ∧
    ∀ r : ℝ, 0 < r → r ≤ r₀ → ∀ (q : ℕ) [NeZero q],
      ∀ (χ : DirichletCharacter ℂ q) (t : ℝ),
        ‖(DirichletCharacter.LFunction χ (mrtMovingPoint r t 0))⁻¹‖ ≤ 1 / r := by
…

    Mentions: OAI.TwoPointCorrelations.mrtMovingPoint