OAI/NumberTheory/DirichletL/Eisenstein/CubeResidueStrata.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_cusp_decay line 85
  2. theorem OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_cubic_decay line 120
  3. theorem OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_zero_cubic_decay line 141
  4. lemma OAI.CubicEisenstein.halfPrimary_lambda_dvd_three line 160
  5. lemma OAI.CubicEisenstein.halfPrimary_lambda_not_dvd_one line 163
  6. lemma OAI.CubicEisenstein.halfPrimary_omega_pow line 167
  7. lemma OAI.CubicEisenstein.halfPrimary_not_negative line 170
  8. abbrev OAI.CubicEisenstein.HalfPrimary line 178
  9. lemma OAI.CubicEisenstein.halfPrimary_ne_zero line 180
  10. lemma OAI.CubicEisenstein.halfPrimary_not_dvd line 185
  11. def OAI.CubicEisenstein.halfPrimaryFromAssociate line 190
  12. lemma OAI.CubicEisenstein.halfPrimaryFromAssociate_injective line 195
  13. lemma OAI.CubicEisenstein.halfPrimaryFromAssociate_surjective line 215
  14. def OAI.CubicEisenstein.halfPrimaryAssociateEquiv line 234
  15. lemma OAI.CubicEisenstein.halfPrimaryAssociateEquiv_apply line 238
  16. lemma OAI.CubicEisenstein.halfPrimary_tsum line 241
  17. def OAI.CubicEisenstein.unitCuspUpper line 250
  18. def OAI.CubicEisenstein.unitCuspDiagonal line 251
  19. theorem OAI.CubicEisenstein.rational_cusp_lower_factor line 254
  20. lemma OAI.CubicEisenstein.unitCuspUpper_section line 269
  21. lemma OAI.CubicEisenstein.unitCuspDiagonal_norm line 281
  22. abbrev OAI.CubicEisenstein.CubeResidueStrata line 295
  23. def OAI.CubicEisenstein.cubeResidueStratumMap line 297
  24. lemma OAI.CubicEisenstein.unit_rep_coprime line 300
  25. lemma OAI.CubicEisenstein.cube_strata_exponents line 305
  26. lemma OAI.CubicEisenstein.cubeResidueStratumMap_injective line 323
  27. lemma OAI.CubicEisenstein.cubeResidueStratumMap_surjective line 347
  28. def OAI.CubicEisenstein.cubeResidueStrataEquiv line 377
  29. def OAI.CubicEisenstein.cubeStratumSymbol line 387
  30. lemma OAI.CubicEisenstein.unit_stratum_symbol_gauss line 390
  31. lemma OAI.CubicEisenstein.cubeStratumSymbol_sum line 402
  32. lemma OAI.CubicEisenstein.cubeStrata_weighted_sum line 423
  33. lemma OAI.CubicKubota.comparison_mod_three line 438
  34. lemma OAI.CubicKubota.comparison_primary line 447
  35. lemma OAI.CubicKubota.comparison_levelTwo line 452
  36. lemma OAI.CubicKubota.levelTwo_cube_zero_phase line 457
  37. lemma OAI.CubicKubota.cube_exponent_zero_of_lower_divisible line 485
  38. lemma OAI.CubicEisenstein.cube_affine_coefficient_unit line 507
  39. def OAI.CubicEisenstein.cubeCuspAffineEquiv line 516
  40. lemma OAI.CubicEisenstein.cubeCuspAffineEquiv_apply line 530
  41. lemma OAI.CubicEisenstein.cubeCuspAffineEquiv_mk line 538
  42. structure OAI.CubicKubota.CubeCuspData line 552
  43. def OAI.CubicKubota.actualCubeCuspData line 559
  44. lemma OAI.CubicKubota.CubeCuspData.lower_eq line 571
  45. lemma OAI.CubicKubota.CubeCuspData.unit_top line 576
  46. def OAI.CubicKubota.CubeCuspData.stratum line 585
  47. lemma OAI.CubicKubota.CubeCuspData.stratum_map line 588
  48. lemma OAI.CubicKubota.CubeCuspData.comparison_phase line 601