OAI/NumberTheory/DirichletL/Eisenstein/RamifiedTransform.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.lowRamifiedTransform line 88
  2. lemma OAI.CubicEisenstein.principalArithmeticResidue_low line 92
  3. lemma OAI.CubicEisenstein.sourceRayPhase_of_three_dvd line 114
  4. lemma OAI.CubicEisenstein.lowRamifiedFrequency_three_dvd line 123
  5. theorem OAI.CubicEisenstein.lowRamifiedTransform_actual line 127
  6. lemma OAI.CubicEisenstein.lowRamifiedTransform_sub line 137
  7. lemma OAI.CubicEisenstein.ramifiedRawWeight_frequency_cube line 143
  8. lemma OAI.CubicEisenstein.lowRamifiedTransform_cube_comp line 149
  9. theorem OAI.CubicEisenstein.lowRamifiedTransform_cube_difference line 162
  10. lemma OAI.CubicEisenstein.ramifiedFunction_reduce line 180
  11. lemma OAI.CubicEisenstein.ramifiedFunction_family_bound line 189
  12. lemma OAI.CubicEisenstein.ramifiedNine_eq line 197
  13. lemma OAI.CubicEisenstein.lowRamified_inner_family line 208
  14. lemma OAI.CubicEisenstein.lowRamifiedLeading line 217
  15. lemma OAI.CubicEisenstein.lowRamified_remainder_bound line 230
  16. theorem OAI.CubicEisenstein.lowRamifiedTransform_injective line 251
  17. lemma OAI.CubicEisenstein.exists_primary_unit_lambda_factor line 286
  18. theorem OAI.CubicEisenstein.unramifiedGaussResidue_prime_cube line 297
  19. lemma OAI.CubicEisenstein.unramifiedGaussResidue_prime_pow_mod line 329
  20. theorem OAI.CubicEisenstein.unramifiedGaussResidue_prime_square line 343
  21. theorem OAI.CubicEisenstein.unramifiedGaussResidue_prime_factor line 356
  22. theorem OAI.CubicEisenstein.unramifiedGaussResidue_prime_power_table line 392
  23. def OAI.CubicEisenstein.thetaFrequencyScale line 420
  24. def OAI.CubicEisenstein.thetaBesselScale line 421
  25. def OAI.CubicEisenstein.thetaDerivativeScalar line 422
  26. lemma OAI.CubicEisenstein.thetaFrequencyScale_ne_zero line 425
  27. lemma OAI.CubicEisenstein.thetaBesselScale_pos line 428
  28. lemma OAI.CubicEisenstein.thetaBesselScale_eq line 430
  29. lemma OAI.CubicEisenstein.thetaDerivativeScalar_ne_zero line 441
  30. lemma OAI.CubicEisenstein.cuspFrequency_eq_thetaFrequencyScale line 446
  31. lemma OAI.CubicEisenstein.completedCoefficient_mul_length line 451
  32. lemma OAI.CubicEisenstein.thetaPair_frequency_norm line 475
  33. lemma OAI.CubicEisenstein.thetaPair_derivative_coefficient line 487
  34. def OAI.CubicEisenstein.thetaTwistedSource line 511
  35. theorem OAI.CubicEisenstein.thetaTwistedSource_wirtingerBar_eq_completedBesselProfile line 515
  36. lemma OAI.CubicEisenstein.horizontalWirtingerBar_finite_sum line 573
  37. lemma OAI.CubicEisenstein.finiteConjugateSource_wirtingerBar_sum line 587
  38. def OAI.CubicEisenstein.thetaTwistedCuspProfile line 611
  39. theorem OAI.CubicEisenstein.thetaTwistedCuspProfile_eq_completedBesselProfile line 616