MRTMovingStrip.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A zero-free strip deduced from two local shrinking-disk growth bounds. The analytic growth assumption remains explicit; the proof itself is the exact three-factor positivity argument for the actual L-functions.

theorem OAI.TwoPointCorrelations.mrt_moving_zero_free line 17

Source documentation

Two disks of radius 3r with logarithmic growth budget B give a zero-free horizontal distance proportional to r/B.

theorem mrt_moving_zero_free : ∃ c r₀ : ℝ, 0 < c ∧ 0 < r₀ ∧
    ∀ (q : ℕ) [NeZero q], ∀ (χ : DirichletCharacter ℂ q),
    ∀ (r t B β : ℝ), 0 < r → r ≤ r₀ → 3 * r < |t| → 1 ≤ B →
      (∀ z ∈ Metric.closedBall (0 : ℂ) (15 / 16),
        ‖mrtMovingLFunction χ r t z‖ ≤ Real.exp B) →
      (∀ z ∈ Metric.closedBall (0 : ℂ) (15 / 16),
        ‖mrtMovingLFunction (χ ^ 2) r (2 * t) z‖ ≤ Real.exp B) →
      1 - c * r / B ≤ β →
        DirichletCharacter.LFunction χ ((β : ℂ) + Complex.I * (t : ℂ)) ≠ 0 := by
…

Mentions: OAI.TwoPointCorrelations.mrtMovingLFunction