OAI/NumberTheory/DirichletL/Eisenstein/SquarefreeCoefficients.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.primaryGenerator_squarefree_support line 86
  2. lemma OAI.CubicEisenstein.primaryPrime_isPrime_of_mem line 98
  3. lemma OAI.CubicEisenstein.primaryPrime_support_coprime line 107
  4. def OAI.CubicEisenstein.infinityCoefficientScalar line 118
  5. theorem OAI.CubicEisenstein.infinityCoefficient_squarefree line 120
  6. theorem OAI.CubicEisenstein.infinityCoefficient_squarefree_cube line 134
  7. theorem OAI.CubicEisenstein.sourceArithmeticResidue_valuation_ne_two line 149
  8. def OAI.CubicEisenstein.thetaSquarefreePart line 186
  9. def OAI.CubicEisenstein.thetaCubePart line 189
  10. lemma OAI.CubicEisenstein.thetaSquarefreePart_squarefree line 192
  11. lemma OAI.CubicEisenstein.thetaParts_mul_cube line 196
  12. theorem OAI.CubicEisenstein.sourceArithmeticResidue_squarefree_cube_support line 216
  13. theorem OAI.CubicEisenstein.sourceFourier_squarefree_cube_support line 237
  14. theorem OAI.CubicEisenstein.sourceFourier_primary_zero_of_base_zero line 246
  15. lemma OAI.CubicEisenstein.unramifiedGaussResidue_eq_of_initial_eq line 271
  16. theorem OAI.CubicEisenstein.unramifiedGaussResidue_neg line 280
  17. theorem OAI.CubicEisenstein.unramifiedGaussResidue_lambda_pow line 284
  18. theorem OAI.CubicEisenstein.unramifiedGaussResidue_lambda_cube line 289
  19. theorem OAI.CubicEisenstein.unramifiedGaussResidue_nine_family line 293
  20. def OAI.CubicEisenstein.ramifiedResidueFamilyMass line 310
  21. lemma OAI.CubicEisenstein.ramifiedResidueFamilyMass_nonneg line 313
  22. lemma OAI.CubicEisenstein.unramifiedGaussResidue_family_norm_le line 316
  23. lemma OAI.CubicEisenstein.unramifiedGaussResidue_nine_norm_le line 323
  24. theorem OAI.CubicEisenstein.unramifiedGaussResidue_unit_lambda_family line 329
  25. lemma OAI.CubicEisenstein.unramifiedGaussResidue_unit_lambda_norm_le line 338
  26. lemma OAI.CubicEisenstein.ramifiedResidueFamilyMass_unit_lambda_le line 344
  27. theorem OAI.CubicEisenstein.sourceArithmeticResidue_family_bound line 359
  28. def OAI.CubicEisenstein.ramifiedDecayRatio line 403
  29. lemma OAI.CubicEisenstein.ramifiedDecayRatio_pos line 405
  30. lemma OAI.CubicEisenstein.ramifiedDecayRatio_lt_one line 408
  31. lemma OAI.CubicEisenstein.explicitRamifiedCoefficient_norm_le line 411
  32. lemma OAI.CubicEisenstein.ramifiedWeight_norm_scalar line 419
  33. lemma OAI.CubicEisenstein.principalRamifiedWeight_norm_le line 442
  34. theorem OAI.CubicEisenstein.principalRamifiedWeight_sum_norm_le line 451
  35. def OAI.CubicEisenstein.ramifiedSourceFamilyConstant line 485
  36. lemma OAI.CubicEisenstein.ramifiedSourceFamilyConstant_nonneg line 488
  37. theorem OAI.CubicEisenstein.sourceArithmeticResidue_nine_family_bound line 493
  38. theorem OAI.CubicEisenstein.sourceArithmeticResidue_unit_lambda_bound line 508
  39. def OAI.CubicEisenstein.extraPeriodWitness line 524
  40. def OAI.CubicEisenstein.rationalLowerMinusThree line 536
  41. lemma OAI.CubicEisenstein.extraPeriodWitness_factor line 538
  42. lemma OAI.CubicEisenstein.extraPeriodWitness_character line 552
  43. lemma OAI.CubicEisenstein.extraPeriodWitness_character_ne_one line 576
  44. theorem OAI.CubicEisenstein.cubicSource_not_eisenstein_periodic line 581