OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/SmoothBlock.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinarySmoothRough.smoothBlock line 23
  2. def OAI.OrdinarySmoothRough.roughBlock line 26
  3. def OAI.OrdinarySmoothRough.hyperbolaRectangle line 29
  4. def OAI.OrdinarySmoothRough.smoothSlice line 32
  5. lemma OAI.OrdinarySmoothRough.rough_of_coprime_product line 35
  6. lemma OAI.OrdinarySmoothRough.rectangle_subset_slice line 41
  7. theorem OAI.OrdinarySmoothRough.slice_defect_card line 66
  8. theorem OAI.OrdinarySmoothRough.slice_defect_sieve line 121