OAI/NumberTheory/TwoPointCorrelations/ModFiveZeroDistance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Quantitative separation between the inner evaluation point and all zeros in the fixed disk, using the zero-free strip for the modulus-five L-functions.

  1. lemma OAI.TwoPointCorrelations.modFive_log_height_ge_half line 15

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

  2. lemma OAI.TwoPointCorrelations.modFive_physical_zero_height line 22

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroDistance.lean:23 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.modFive_physical_zero_log_height line 35

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroDistance.lean:36 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.modFive_zero_distance_of_strip line 45

    Also declared: OAI/NumberTheory/TwoPoint/Fourier/ModFiveZeroDistance.lean:46 (same declaration text).