OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Event.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.OrdinaryCorrelations.SourceBoxSieve.Box line 28
  2. def OAI.OrdinaryCorrelations.SourceBoxSieve.event line 30
  3. def OAI.OrdinaryCorrelations.SourceBoxSieve.weight line 34
  4. def OAI.OrdinaryCorrelations.SourceBoxSieve.density line 36
  5. lemma OAI.OrdinaryCorrelations.SourceBoxSieve.joint_eq_product line 40
  6. lemma OAI.OrdinaryCorrelations.SourceBoxSieve.sum_box line 54
  7. lemma OAI.OrdinaryCorrelations.SourceBoxSieve.intersection_eq_sum line 65
  8. theorem OAI.OrdinaryCorrelations.SourceBoxSieve.intersection_boundary line 78
  9. theorem OAI.OrdinaryCorrelations.SourceBoxSieve.finite_box_sieve line 100