OAI/NumberTheory/DirichletL/Eisenstein/UnitNormalization.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CanonicalUnitEuler.good_prime_norm_mod_six line 83
  2. lemma OAI.CanonicalUnitEuler.unit_sixth_exponent_mul line 96
  3. lemma OAI.CanonicalUnitEuler.multiset_unit_norm line 109
  4. theorem OAI.CanonicalUnitEuler.idealRowHom_unit_norm line 130
  5. lemma OAI.CanonicalUnitEuler.ideal_norm_mod_six_of_good line 142
  6. theorem OAI.CanonicalUnitEuler.idealRowHom_unit_eq_of_norm_mod_thirty_six line 152
  7. theorem OAI.CanonicalUnitEuler.rowTwist_unit_norm line 166
  8. theorem OAI.CompletedGauss.normalized_cusp_coefficient line 184
  9. theorem OAI.CompletedGauss.normalized_reflection_weight line 209
  10. theorem OAI.CompletedGauss.normalized_cusp_coefficient_nat line 215
  11. theorem OAI.CompletedGauss.reflection_kernel_scale line 223
  12. theorem OAI.CompletedGauss.completed_branch_kernel_argument line 232
  13. theorem OAI.CanonicalRowCompletion.shortEnergy_scalar_normalization line 266
  14. theorem OAI.CanonicalRowCompletion.canonicalShortEnergy_normalized_uniform_twist line 303
  15. lemma OAI.CubicEisenstein.rowCoordinates_zero line 350
  16. lemma OAI.CubicEisenstein.rowCoordinates_norm_pos line 359
  17. lemma OAI.CubicEisenstein.rowCoordinates_le_horizontal line 365
  18. lemma OAI.CubicEisenstein.height_times_coordinate_bound line 384
  19. lemma OAI.CubicEisenstein.rowHeight_times_coordinates line 396
  20. lemma OAI.CubicEisenstein.positive_rpow_of_product_bound line 412
  21. def OAI.CubicEisenstein.cuspRemainderProfile line 420
  22. lemma OAI.CubicEisenstein.cuspRemainderProfile_norm_le line 423
  23. lemma OAI.CubicEisenstein.cuspRemainderProfile_zero line 438
  24. lemma OAI.CubicEisenstein.cuspRemainderProfile_norm_le_bound line 443
  25. lemma OAI.CubicEisenstein.integral_row_embedding_ne_zero line 457
  26. lemma OAI.CubicEisenstein.coprime_row_ne_zero line 465
  27. theorem OAI.CubicEisenstein.cuspRemainderProfile_row_bound line 471
  28. def OAI.CubicEisenstein.translatedCuspRow line 506
  29. lemma OAI.CubicEisenstein.translatedCuspRow_injective line 509
  30. lemma OAI.CubicEisenstein.integral_bottom_coprime line 517
  31. lemma OAI.CubicEisenstein.translatedCuspRow_coprime line 523
  32. lemma OAI.CubicEisenstein.cosetHeight_integral_chart line 531
  33. lemma OAI.CubicEisenstein.translated_remainder_majorant line 545
  34. lemma OAI.CubicEisenstein.cuspCutoffTerm_eq_seedProfile line 565
  35. lemma OAI.CubicEisenstein.cusp_seed_profile_summable line 574
  36. theorem OAI.CubicEisenstein.eisenstein_sub_seed_eq_series line 581
  37. def OAI.CubicEisenstein.eisensteinRemainderBound line 598
  38. lemma OAI.CubicEisenstein.eisensteinRemainderBound_nonneg line 601
  39. theorem OAI.CubicEisenstein.eisenstein_sub_seed_chart_bound line 606
  40. theorem OAI.CubicEisenstein.eisenstein_sub_seed_bounded line 629
  41. lemma OAI.CubicEisenstein.cuspRemainderProfile_measurable line 645
  42. lemma OAI.CubicEisenstein.eisenstein_sub_seed_measurable line 650
  43. theorem OAI.CubicEisenstein.kernel_eisenstein_sub_seed_memLp line 659