MRTMovingNorm.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Local growth uniformly at nearby centers gives a logarithmic-derivative norm bound. The quantitative loss is B²/r, with no polynomial height loss.

theorem OAI.TwoPointCorrelations.mrt_moving_local_logderiv line 15

Source documentation

A local pair of growth bounds suffices for the actual logarithmic derivative on the segment immediately to the right of one.

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

Mentions: OAI.TwoPointCorrelations.mrtMovingLFunction