OAI/NumberTheory/DirichletL/Detector/LowTruePeriodPuncture.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SevenEighths.ProbePhysical.physicalRayPeriodicBase_support line 13
  2. def OAI.SevenEighths.ProbePhysical.lowTruePeriodGenerator line 33
  3. lemma OAI.SevenEighths.ProbePhysical.lowPeriodIdeal_ne_zero line 36
  4. lemma OAI.SevenEighths.ProbePhysical.lowTruePeriodGenerator_ne_zero line 44
  5. lemma OAI.SevenEighths.ProbePhysical.lowTruePeriodGenerator_span line 48
  6. lemma OAI.SevenEighths.ProbePhysical.physicalRayPeriodicBase_zero_true_puncture line 52
  7. theorem OAI.SevenEighths.ProbePhysical.physical_row_absorb_true_period line 62
  8. lemma OAI.SevenEighths.ProbePhysical.physical_true_period_residual_coprime line 72
  9. def OAI.SevenEighths.ProbePhysical.lowReflectionPeriod line 80
  10. lemma OAI.SevenEighths.ProbePhysical.lowReflectionPeriod_ne_zero line 84
  11. lemma OAI.SevenEighths.ProbePhysical.lowReflectionPeriod_actual line 88
  12. def OAI.SevenEighths.ProbePhysical.lowReflectionMask line 94
  13. lemma OAI.SevenEighths.ProbePhysical.lowReflectionMask_ne_zero line 98
  14. lemma OAI.SevenEighths.ProbePhysical.lowReflectionMask_bad line 102
  15. lemma OAI.SevenEighths.ProbePhysical.lowReflectionMask_period line 108
  16. lemma OAI.SevenEighths.ProbePhysical.physical_markedCompletedT_absorb_true_period line 113