OAI/NumberTheory/TwoPoint/Fourier/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. The only strip used below is the one already proved for the actual modulus-five L-functions.

  1. lemma OAI.TwoPointCorrelations.modFive_log_height_ge_half line 16

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveZeroDistance.lean:15 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.modFive_physical_zero_height line 23

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveZeroDistance.lean:22 (same declaration text).

  3. lemma OAI.TwoPointCorrelations.modFive_physical_zero_log_height line 36

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveZeroDistance.lean:35 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.modFive_zero_distance_of_strip line 46

    Also declared: OAI/NumberTheory/TwoPointCorrelations/ModFiveZeroDistance.lean:45 (same declaration text).