OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Reciprocal.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinarySelbergWeights.reciprocal line 14
  2. theorem OAI.OrdinarySelbergWeights.reciprocal_apply line 16
  3. theorem OAI.OrdinarySelbergWeights.reciprocal_mult line 18
  4. def OAI.OrdinarySelbergWeights.reciprocalSieve line 24
  5. def OAI.OrdinarySelbergWeights.actualWeights line 42
  6. def OAI.OrdinarySelbergWeights.actualMass line 45
  7. lemma OAI.OrdinarySelbergWeights.actualWeights_one line 48
  8. lemma OAI.OrdinarySelbergWeights.actualWeights_abs_le line 51
  9. lemma OAI.OrdinarySelbergWeights.actualWeights_zero_above line 56
  10. lemma OAI.OrdinarySelbergWeights.actualMass_log_bound line 60
  11. theorem OAI.OrdinarySelbergWeights.actualWeights_diagonal line 65
  12. theorem OAI.OrdinarySelbergWeights.actualWeights_l1 line 85
  13. def OAI.OrdinarySelbergWeights.sieveWeight line 108
  14. lemma OAI.OrdinarySelbergWeights.sieveWeight_nonneg line 111
  15. lemma OAI.OrdinarySelbergWeights.sieveWeight_eq_one_of_coprime line 114
  16. lemma OAI.OrdinarySelbergWeights.rough_indicator_le line 131
  17. theorem OAI.OrdinarySelbergWeights.sieveWeight_expansion line 137