OAI/NumberTheory/TwoPointCorrelations/ModFiveZeroTerms.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.modFivePhysicalPoint line 15

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:15 (same declaration text).

  2. def OAI.TwoPointCorrelations.modFiveRealDiskPoint line 18

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:18 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.modFivePhysicalPoint_real line 21

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:21 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.modFiveNormalizedLFunction_deriv line 28

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:28 (same declaration text).

  5. lemma OAI.TwoPointCorrelations.modFiveNormalized_logderiv_eq line 39

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:39 (same declaration text).

  6. lemma OAI.TwoPointCorrelations.modFiveNormalizedZeros_physical_zero line 52

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:52 (same declaration text).

  7. lemma OAI.TwoPointCorrelations.modFiveNormalizedZeros_re line 61

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:61 (same declaration text).

  8. lemma OAI.TwoPointCorrelations.modFiveRealDiskPoint_norm line 71

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:71 (same declaration text).

  9. lemma OAI.TwoPointCorrelations.modFive_zeroTerm_re_nonneg line 77

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:77 (same declaration text).

  10. theorem OAI.TwoPointCorrelations.modFive_neg_logderiv_re_le line 92

    Source documentation

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

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:92 (same declaration text).

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

    Mentions: OAI.TwoPointCorrelations.modFiveLogDerivativeConstant, OAI.TwoPointCorrelations.modFiveInverseConstant

  11. lemma OAI.TwoPointCorrelations.modFive_zero_multiplicity_pos line 119

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:119 (same declaration text).

  12. lemma OAI.TwoPointCorrelations.modFive_real_zero_mem line 137

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:137 (same declaration text).

  13. lemma OAI.TwoPointCorrelations.modFive_zero_sum_lower line 152

    Source documentation

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

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:152 (same declaration text).

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

    Mentions: OAI.TwoPointCorrelations.modFiveNormalizedZeros_finite, OAI.TwoPointCorrelations.modFiveNormalizedLFunction, OAI.TwoPointCorrelations.modFiveRealDiskPoint

  14. theorem OAI.TwoPointCorrelations.modFive_neg_logderiv_re_le_of_zero line 186

    Source documentation

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

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroTerms.lean:186 (same declaration text).

    theorem modFive_neg_logderiv_re_le_of_zero (χ : DirichletCharacter ℂ 5)
    (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 : ℝ) * modFiveLogDerivativeConstant *
          Real.log (8 * modFiveInverseConstant * (|t| + 4)) - 1 / (σ - β) := by
…

    Mentions: OAI.TwoPointCorrelations.modFiveLogDerivativeConstant, OAI.TwoPointCorrelations.modFiveInverseConstant