OAI/NumberTheory/DirichletL/Detector/Physical.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SevenEighths.ProbePhysical.CalibrationData line 17
  2. def OAI.SevenEighths.ProbePhysical.elementNorm line 23
  3. def OAI.SevenEighths.ProbePhysical.CalibrationData.residueMonoid line 25
  4. def OAI.SevenEighths.ProbePhysical.CalibrationData.Xi line 28
  5. def OAI.SevenEighths.ProbePhysical.CalibrationData.tau line 31
  6. def OAI.SevenEighths.ProbePhysical.sexticGauss line 36
  7. theorem OAI.SevenEighths.ProbePhysical.sexticGauss_coefficient_mk line 41
  8. def OAI.SevenEighths.ProbePhysical.verticalIntegral line 49
  9. def OAI.SevenEighths.ProbePhysical.markedPhysicalProbe line 52
  10. def OAI.SevenEighths.ProbePhysical.physicalProbe line 69
  11. def OAI.SevenEighths.ProbePhysical.slotProduct line 73
  12. def OAI.SevenEighths.ProbePhysical.compensatedTuple line 75
  13. theorem OAI.SevenEighths.ProbePhysical.elementNorm_one line 80
  14. theorem OAI.SevenEighths.ProbePhysical.compensatedTuple_zero line 85
  15. theorem OAI.SevenEighths.ProbePhysical.compensatedTuple_one line 95
  16. def OAI.SevenEighths.ProbePhysical.compensatedPhysicalProbe line 108