OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterZeroTerms.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Transfer the normalized disk expansion back to the actual L-functions. Every zero in the finite disk lies left of the line of evaluation, so its logarithmic-derivative contribution has nonnegative real part.

  1. def OAI.TwoPointCorrelations.mrtCharacterPhysicalPoint line 17
  2. def OAI.TwoPointCorrelations.mrtCharacterRealDiskPoint line 20
  3. lemma OAI.TwoPointCorrelations.mrtCharacterPhysicalPoint_real line 23
  4. lemma OAI.TwoPointCorrelations.mrtCharacterNormalizedLFunction_deriv line 30
  5. lemma OAI.TwoPointCorrelations.mrtCharacterNormalized_logderiv_eq line 41
  6. lemma OAI.TwoPointCorrelations.mrtCharacterNormalizedZeros_physical_zero line 54
  7. lemma OAI.TwoPointCorrelations.mrtCharacterNormalizedZeros_re line 63
  8. lemma OAI.TwoPointCorrelations.mrtCharacterRealDiskPoint_norm line 73
  9. lemma OAI.TwoPointCorrelations.mrtCharacter_zeroTerm_re_nonneg line 79
  10. theorem OAI.TwoPointCorrelations.mrtCharacter_neg_logderiv_re_le line 94

    Source documentation

    A logarithmic-derivative upper bound to the right of one, obtained by dropping the nonnegative zero terms from the actual finite expansion.

    theorem mrtCharacter_neg_logderiv_re_le (χ : DirichletCharacter ℂ q)
    (hχ : χ ≠ 1) (t : ℝ) {σ : ℝ} (hσ : 1 < σ) (hσ2 : σ ≤ 2) :
    (-deriv (DirichletCharacter.LFunction χ) ((σ : ℂ) + Complex.I * (t : ℂ)) /
      DirichletCharacter.LFunction χ ((σ : ℂ) + Complex.I * (t : ℂ))).re ≤
        (2 / 3 : ℝ) * mrtCharacterLogDerivativeConstant *
          Real.log ((2 * q : ℝ) * mrtCharacterInverseConstant * (|t| + 4)) := by
…

    Mentions: OAI.TwoPointCorrelations.mrtCharacterLogDerivativeConstant, OAI.TwoPointCorrelations.mrtCharacterInverseConstant

  11. lemma OAI.TwoPointCorrelations.mrtCharacter_zero_multiplicity_pos line 121
  12. lemma OAI.TwoPointCorrelations.mrtCharacter_real_zero_mem line 139
  13. lemma OAI.TwoPointCorrelations.mrtCharacter_zero_sum_lower line 154

    Source documentation

    A zero at height t contributes its full reciprocal distance; the other zeros have nonnegative real contributions.

    lemma mrtCharacter_zero_sum_lower (χ : DirichletCharacter ℂ q) (hχ : χ ≠ 1)
    (t : ℝ) {σ β : ℝ} (hσ : 1 < σ) (hβ : 3 / 4 ≤ β) (hβ1 : β ≤ 1)
    (hzero : DirichletCharacter.LFunction χ ((β : ℂ) + Complex.I * (t : ℂ)) = 0) :
    (3 / 2 : ℝ) / (σ - β) ≤
      ∑ ρ ∈ (mrtCharacterNormalizedZeros_finite χ hχ t).toFinset,
        (((analyticOrderAt (mrtCharacterNormalizedLFunction χ t) ρ).toNat : ℂ) /
          (mrtCharacterRealDiskPoint σ - ρ)).re := by
…

    Mentions: OAI.TwoPointCorrelations.mrtCharacterNormalizedZeros_finite, OAI.TwoPointCorrelations.mrtCharacterNormalizedLFunction, OAI.TwoPointCorrelations.mrtCharacterRealDiskPoint

  14. theorem OAI.TwoPointCorrelations.mrtCharacter_neg_logderiv_re_le_of_zero line 188

    Source documentation

    The one-zero upper bound, with its negative reciprocal term retained.

    theorem mrtCharacter_neg_logderiv_re_le_of_zero (χ : DirichletCharacter ℂ q)
    (hχ : χ ≠ 1) (t : ℝ) {σ β : ℝ} (hσ : 1 < σ) (hσ2 : σ ≤ 2)
    (hβ : 3 / 4 ≤ β) (hβ1 : β ≤ 1)
    (hzero : DirichletCharacter.LFunction χ ((β : ℂ) + Complex.I * (t : ℂ)) = 0) :
    (-deriv (DirichletCharacter.LFunction χ) ((σ : ℂ) + Complex.I * (t : ℂ)) /
      DirichletCharacter.LFunction χ ((σ : ℂ) + Complex.I * (t : ℂ))).re ≤
        (2 / 3 : ℝ) * mrtCharacterLogDerivativeConstant *
          Real.log ((2 * q : ℝ) * mrtCharacterInverseConstant * (|t| + 4)) - 1 / (σ - β) := by
…

    Mentions: OAI.TwoPointCorrelations.mrtCharacterLogDerivativeConstant, OAI.TwoPointCorrelations.mrtCharacterInverseConstant