OAI/NumberTheory/DirichletL/Detector/RayCharacterFamily.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ProbeRayCharacterFamily.fixedTwistSupport line 22
  2. theorem OAI.SevenEighths.ProbeRayCharacterFamily.fixedTwistSupport_prime line 26
  3. lemma OAI.SevenEighths.ProbeRayCharacterFamily.inverse_twist_base_modulus line 30
  4. theorem OAI.SevenEighths.ProbeRayCharacterFamily.large_supported_twists_nonprincipal line 36
  5. theorem OAI.SevenEighths.ProbeRayCharacterFamily.raw_twisted_conductor line 65
  6. theorem OAI.SevenEighths.ProbeRayCharacterFamily.canonical_amplitude_raw line 73
  7. theorem OAI.SevenEighths.ProbeRayCharacterFamily.large_supported_twists_eventually line 98
  8. theorem OAI.SevenEighths.ProbeRayCharacterFamily.source_maximum_dominates line 109
  9. theorem OAI.SevenEighths.ProbeRayCharacterFamily.source_nonprincipal_maximum_dominates line 121