OAI/NumberTheory/DirichletL/Hecke/DetectorPartition.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.HeckeDetectorPartition.partition line 10
  2. theorem OAI.SevenEighths.HeckeDetectorPartition.finite_pair_reassembly line 20
  3. theorem OAI.SevenEighths.HeckeDetectorPartition.annular_support line 53
  4. def OAI.SevenEighths.HeckeDetectorPartition.length line 76
  5. theorem OAI.SevenEighths.HeckeDetectorPartition.norm_le_last_scale line 78
  6. theorem OAI.SevenEighths.HeckeDetectorPartition.length_bound line 83
  7. theorem OAI.SevenEighths.HeckeDetectorPartition.pair_scale_bounds line 90
  8. def OAI.SevenEighths.HeckeDetectorPartition.pairCoefficient line 134
  9. theorem OAI.SevenEighths.HeckeDetectorPartition.actual_pair_reassembly line 141
  10. theorem OAI.SevenEighths.HeckeDetectorPartition.exists_large_pair line 161