OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Euler.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryCorrelations.LocalExpansion.euler line 25
  2. lemma OAI.OrdinaryCorrelations.LocalExpansion.euler_one line 28
  3. lemma OAI.OrdinaryCorrelations.LocalExpansion.euler_multiplicative line 30
  4. lemma OAI.OrdinaryCorrelations.LocalExpansion.euler_bounded line 36
  5. lemma OAI.OrdinaryCorrelations.LocalExpansion.euler_primePow line 44
  6. lemma OAI.OrdinaryCorrelations.LocalExpansion.one_or_zero line 49
  7. lemma OAI.OrdinaryCorrelations.LocalExpansion.factorization_formula line 60
  8. lemma OAI.OrdinaryCorrelations.LocalExpansion.euler_extend line 79
  9. def OAI.OrdinaryCorrelations.LocalExpansion.patch line 87
  10. def OAI.OrdinaryCorrelations.LocalExpansion.summand line 90
  11. lemma OAI.OrdinaryCorrelations.LocalExpansion.summand_bounded line 93
  12. lemma OAI.OrdinaryCorrelations.LocalExpansion.summand_product line 101
  13. theorem OAI.OrdinaryCorrelations.LocalExpansion.signed_expansion line 127
  14. def OAI.OrdinaryCorrelations.LocalExpansion.dilation line 139
  15. def OAI.OrdinaryCorrelations.LocalExpansion.localA line 141
  16. def OAI.OrdinaryCorrelations.LocalExpansion.localB line 144
  17. def OAI.OrdinaryCorrelations.LocalExpansion.localC line 147
  18. def OAI.OrdinaryCorrelations.LocalExpansion.dilationSummand line 149
  19. lemma OAI.OrdinaryCorrelations.LocalExpansion.dilation_union line 152
  20. lemma OAI.OrdinaryCorrelations.LocalExpansion.dilation_product line 183
  21. lemma OAI.OrdinaryCorrelations.LocalExpansion.local_sub line 198
  22. theorem OAI.OrdinaryCorrelations.LocalExpansion.dilation_expansion line 206
  23. lemma OAI.OrdinaryCorrelations.LocalExpansion.dilationSummand_bounded line 220
  24. lemma OAI.OrdinaryCorrelations.LocalExpansion.dilationSummand_multiplicative line 232
  25. lemma OAI.OrdinaryCorrelations.LocalExpansion.dilationSummand_one line 235
  26. lemma OAI.OrdinaryCorrelations.LocalExpansion.dilationSummand_primePow line 238
  27. theorem OAI.OrdinaryCorrelations.LocalExpansion.dilationSummand_nonpretentious line 248