OAI/NumberTheory/DirichletL/Moments/CanonicalFirst.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.CenteredMomentCanonicalFirst.CommonIndex line 17
  2. instance OAI.SevenEighths.CenteredMomentCanonicalFirst.commonIndexMaximal line 18
  3. def OAI.SevenEighths.CenteredMomentCanonicalFirst.leftExponent line 22
  4. def OAI.SevenEighths.CenteredMomentCanonicalFirst.rightExponent line 23
  5. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.common_good line 25
  6. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.common_odd line 29
  7. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.leftExponent_pos line 33
  8. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.rightExponent_pos line 36
  9. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.commonPart_left_product line 39
  10. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.commonPart_right_product line 43
  11. abbrev OAI.SevenEighths.CenteredMomentCanonicalFirst.ActiveIndex line 49
  12. def OAI.SevenEighths.CenteredMomentCanonicalFirst.activePrime line 51
  13. instance OAI.SevenEighths.CenteredMomentCanonicalFirst.activePrimeMaximal line 52
  14. def OAI.SevenEighths.CenteredMomentCanonicalFirst.activeConductor line 55
  15. def OAI.SevenEighths.CenteredMomentCanonicalFirst.activeExponent line 56
  16. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.activeGood line 58
  17. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.activeCoprime line 61
  18. def OAI.SevenEighths.CenteredMomentCanonicalFirst.activeFunction line 65
  19. def OAI.SevenEighths.CenteredMomentCanonicalFirst.residualGenerator line 69
  20. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.residualGenerator_span line 71
  21. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.residualGenerator_supported line 75
  22. def OAI.SevenEighths.CenteredMomentCanonicalFirst.residualCharacter line 80
  23. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.residualCharacter_mk line 83
  24. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.original_pair_factor line 87
  25. def OAI.SevenEighths.CenteredMomentCanonicalFirst.reducedFirstSum line 102
  26. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.canonical_pair_reduced_poisson line 118
  27. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.activeConductor_span_dvd line 131
  28. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.residual_active_coprime line 143
  29. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.opposite_residual_active_coprime line 149
  30. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.residual_generators_coprime line 155
  31. theorem OAI.SevenEighths.CenteredMomentCanonicalFirst.canonical_tripleFourier_norm_le line 161