OAI/NumberTheory/DirichletL/Detector/Calibration.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ProbePhysical.crtCharacter line 12
  2. theorem OAI.SevenEighths.ProbePhysical.crtCharacter_pow_six line 28
  3. theorem OAI.SevenEighths.ProbePhysical.residue_char_ne_two_of_lambda_mem line 43
  4. theorem OAI.SevenEighths.ProbePhysical.exists_local_calibration line 58
  5. def OAI.SevenEighths.ProbePhysical.localCalibration line 85
  6. theorem OAI.SevenEighths.ProbePhysical.localCalibration_nonprincipal line 88
  7. theorem OAI.SevenEighths.ProbePhysical.localCalibration_pow_six line 91
  8. def OAI.SevenEighths.ProbePhysical.calibrationFromPrimes line 94
  9. theorem OAI.SevenEighths.ProbePhysical.calibrationFromPrimes_pow_six line 106
  10. theorem OAI.SevenEighths.ProbePhysical.calibrationFromPrimes_tau_norm line 113
  11. theorem OAI.SevenEighths.ProbePhysical.calibrationFromPrimes_tau_ne_zero line 150
  12. def OAI.SevenEighths.ProbePhysical.calibrationForSet line 156
  13. theorem OAI.SevenEighths.ProbePhysical.calibrationForSet_excluded line 161
  14. theorem OAI.SevenEighths.ProbePhysical.calibrationForSet_span line 167
  15. theorem OAI.SevenEighths.ProbePhysical.calibrationForSet_pow_six line 173
  16. theorem OAI.SevenEighths.ProbePhysical.calibrationForSet_tau_norm line 179
  17. theorem OAI.SevenEighths.ProbePhysical.calibrationForSet_tau_ne_zero line 185