OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/MobiusInverse.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinarySelbergWeights.mobiusInverse line 14
  2. theorem OAI.OrdinarySelbergWeights.sum_mobiusInverse line 17
  3. theorem OAI.OrdinarySelbergWeights.upper_divisor_sum line 22
  4. def OAI.OrdinarySelbergWeights.upperInverse line 40
  5. theorem OAI.OrdinarySelbergWeights.upperInverse_sum line 43
  6. theorem OAI.OrdinarySelbergWeights.upperInverse_one line 51
  7. def OAI.OrdinarySelbergWeights.mass line 59
  8. def OAI.OrdinarySelbergWeights.target line 62
  9. def OAI.OrdinarySelbergWeights.weights line 65
  10. theorem OAI.OrdinarySelbergWeights.mass_pos line 68
  11. theorem OAI.OrdinarySelbergWeights.weights_one line 77
  12. theorem OAI.OrdinarySelbergWeights.weights_upper_sum line 95
  13. theorem OAI.OrdinarySelbergWeights.weights_mainSum line 105
  14. theorem OAI.OrdinarySelbergWeights.upperInverse_explicit line 128
  15. theorem OAI.OrdinarySelbergWeights.target_abs line 143
  16. theorem OAI.OrdinarySelbergWeights.upperInverse_target_abs_le line 156
  17. theorem OAI.OrdinarySelbergWeights.weights_abs_le line 182
  18. theorem OAI.OrdinarySelbergWeights.weights_zero_above line 188