OAI/NumberTheory/TwoPointCorrelations/ModFiveLogDerivative.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed-radius logarithmic-derivative expansion for the three modulus-five functions. The analytic disk theorem applies with explicit analyticity, finite-zero, normalization and growth hypotheses.

  1. def OAI.TwoPointCorrelations.modFiveNormalizedZeros line 16

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLogDerivative.lean:16 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFiveNormalizedZeros_finite line 19

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLogDerivative.lean:19 (same declaration text).

  3. def OAI.TwoPointCorrelations.modFiveLogDerivativeConstant line 29

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLogDerivative.lean:29 (same declaration text).

  4. theorem OAI.TwoPointCorrelations.modFiveNormalized_logderiv line 34

    Source documentation

    Exact finite zero-sum approximation on the inner disk.

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveLogDerivative.lean:34 (same declaration text).

    theorem modFiveNormalized_logderiv (χ : DirichletCharacter ℂ 5)
    (hχ : χ ≠ 1) (t : ℝ) {z : ℂ} (hz : ‖z‖ ≤ 3 / 4)
    (hn : modFiveNormalizedLFunction χ t z ≠ 0) :
    ‖deriv (modFiveNormalizedLFunction χ t) z / modFiveNormalizedLFunction χ t z -
      ∑ ρ ∈ (modFiveNormalizedZeros_finite χ hχ t).toFinset,
        (analyticOrderAt (modFiveNormalizedLFunction χ t) ρ).toNat / (z - ρ)‖ ≤
      modFiveLogDerivativeConstant *
        Real.log (8 * modFiveInverseConstant * (|t| + 4)) := by
…

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