OAI/NumberTheory/TwoPoint/ShortIntervals/MRTQuadraticLowZeros.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The effective quadratic disk supplies the bounded-height part of a zero-free strip, with its polynomial modulus dependence displayed.

  1. lemma OAI.TwoPointCorrelations.mrt_character_height_half line 14
  2. lemma OAI.TwoPointCorrelations.mrt_real_shift_norm line 23
  3. lemma OAI.TwoPointCorrelations.mrt_real_shift_inv_norm line 31
  4. lemma OAI.TwoPointCorrelations.mrt_quadratic_zero_cost line 39
  5. lemma OAI.TwoPointCorrelations.mrt_quadratic_zero_combine line 50
  6. theorem OAI.TwoPointCorrelations.mrt_quadratic_bounded_height_zero_free line 68

    Source documentation

    The constant can depend on the fixed height cutoff, but not the modulus.

    theorem mrt_quadratic_bounded_height_zero_free (T : ℝ) :
    ∃ c : ℝ, 0 < c ∧ ∀ (q : ℕ) [NeZero q],
      ∀ (χ : DirichletCharacter ℂ q), χ ≠ 1 → χ ^ 2 = 1 →
      ∀ t beta : ℝ, |t| ≤ T →
        1 - c / ((q : ℝ) ^ 2 * mrtCharacterHeight q t) ≤ beta →
        DirichletCharacter.LFunction χ ((beta : ℂ) + Complex.I * (t : ℂ)) ≠ 0 := by
…

    Mentions: OAI.TwoPointCorrelations.mrtCharacterHeight