OAI/NumberTheory/DirichletL/Hecke/DetectorRawFiber.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SevenEighths.HeckeDetectorRawFiber.Fiber line 16
  2. def OAI.SevenEighths.HeckeDetectorRawFiber.Fiber.r line 54
  3. def OAI.SevenEighths.HeckeDetectorRawFiber.Fiber.m line 55
  4. def OAI.SevenEighths.HeckeDetectorRawFiber.Fiber.q line 56
  5. def OAI.SevenEighths.HeckeDetectorRawFiber.Fiber.inverseProfile line 57
  6. def OAI.SevenEighths.HeckeDetectorRawFiber.Fiber.physicalProduct line 58
  7. structure OAI.SevenEighths.HeckeDetectorRawFiber.Moments line 62
  8. theorem OAI.SevenEighths.HeckeDetectorRawFiber.Fiber.mean_bounds line 83