OAI/NumberTheory/TwoPoint/ShortIntervals/MRTCharacterZeroDistance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Horizontal separation of all zeros in the normalized disk from a point in a narrower high-height strip.

  1. lemma OAI.TwoPointCorrelations.mrt_character_physical_zero_height line 16
  2. lemma OAI.TwoPointCorrelations.mrt_character_physical_zero_height_lower line 29
  3. lemma OAI.TwoPointCorrelations.mrt_character_physical_zero_log_height line 43
  4. lemma OAI.TwoPointCorrelations.mrt_character_zero_distance_of_strip line 60