OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/OneOrZero.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.OrdinaryCorrelations.Completion.one_or_zero line 16
  2. def OAI.OrdinaryCorrelations.Completion.arithmetic line 27
  3. lemma OAI.OrdinaryCorrelations.Completion.arithmetic_apply_pos line 30
  4. lemma OAI.OrdinaryCorrelations.Completion.arithmetic_multiplicative line 33
  5. def OAI.OrdinaryCorrelations.Completion.complete line 41
  6. lemma OAI.OrdinaryCorrelations.Completion.complete_one line 44
  7. lemma OAI.OrdinaryCorrelations.Completion.complete_mul line 46
  8. lemma OAI.OrdinaryCorrelations.Completion.complete_multiplicative line 57
  9. lemma OAI.OrdinaryCorrelations.Completion.complete_prime line 60
  10. lemma OAI.OrdinaryCorrelations.Completion.complete_pow line 63
  11. lemma OAI.OrdinaryCorrelations.Completion.complete_oneBounded line 68
  12. lemma OAI.OrdinaryCorrelations.Completion.complete_pmul_convolution line 81
  13. lemma OAI.OrdinaryCorrelations.Completion.complete_pmul_one line 91
  14. def OAI.OrdinaryCorrelations.Completion.completeInverse line 97
  15. lemma OAI.OrdinaryCorrelations.Completion.completeInverse_mul line 100
  16. def OAI.OrdinaryCorrelations.Completion.kernel line 105
  17. lemma OAI.OrdinaryCorrelations.Completion.kernel_reconstruct line 107
  18. lemma OAI.OrdinaryCorrelations.Completion.kernel_multiplicative line 110
  19. lemma OAI.OrdinaryCorrelations.Completion.complete_distanceSq line 115
  20. lemma OAI.OrdinaryCorrelations.Completion.complete_uniformlyNonpretentious line 122