OAI/NumberTheory/DirichletL/Detector/Completed.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.ProbeCompleted.completedIndex line 14
  2. def OAI.SevenEighths.ProbeCompleted.completedMask line 16
  3. def OAI.SevenEighths.ProbeCompleted.completedCorrection line 19
  4. theorem OAI.SevenEighths.ProbeCompleted.completedCorrection_eq_phase line 24
  5. theorem OAI.SevenEighths.ProbeCompleted.completedMask_norm_le_one line 28
  6. theorem OAI.SevenEighths.ProbeCompleted.completedCorrection_norm_le_two line 33
  7. def OAI.SevenEighths.ProbeCompleted.markedSummand line 43
  8. def OAI.SevenEighths.ProbeCompleted.correctedSummand line 47
  9. def OAI.SevenEighths.ProbeCompleted.markedCompletedT line 51
  10. def OAI.SevenEighths.ProbeCompleted.correctedCompletedT line 55
  11. def OAI.SevenEighths.ProbeCompleted.correctionCoeff line 59
  12. theorem OAI.SevenEighths.ProbeCompleted.correctionCoeff_sum_norm_le line 62
  13. theorem OAI.SevenEighths.ProbeCompleted.completedIndex_eq_primaryGenerator line 68
  14. theorem OAI.SevenEighths.ProbeCompleted.completedMask_zero_of_excluded line 72
  15. theorem OAI.SevenEighths.ProbeCompleted.completedMask_zero_of_not_marked line 79
  16. theorem OAI.SevenEighths.ProbeCompleted.completedCorrection_expansion line 83
  17. theorem OAI.SevenEighths.ProbeCompleted.correctedSummand_ray_expansion line 88
  18. theorem OAI.SevenEighths.ProbeCompleted.markedSummand_summable line 102
  19. theorem OAI.SevenEighths.ProbeCompleted.correctedSummand_summable line 110
  20. theorem OAI.SevenEighths.ProbeCompleted.correctedCompletedT_ray_expansion line 118
  21. theorem OAI.SevenEighths.ProbeCompleted.correctedCompletedT_norm_le line 129