OAI/NumberTheory/DirichletL/Eisenstein/CuspDilation.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.ramifiedTraceLambda line 84
  2. lemma OAI.CubicEisenstein.ramifiedEmbedding_traceLambda line 86
  3. lemma OAI.CubicEisenstein.breveE_embedding_third_eval line 90
  4. lemma OAI.CubicEisenstein.primary_add_three line 105
  5. lemma OAI.CubicEisenstein.symbol_omega_pow_primary_shift line 111
  6. def OAI.CubicEisenstein.ninthCuspFrequency line 143
  7. def OAI.CubicEisenstein.unitLowerGauss line 145
  8. lemma OAI.CubicEisenstein.unitLower_phase_identity line 152
  9. lemma OAI.CubicEisenstein.unitLowerGauss_factor line 181
  10. theorem OAI.CubicEisenstein.unitLowerGauss_eq_unramified line 206
  11. def OAI.CubicEisenstein.UnitCuspFrequency line 247
  12. lemma OAI.CubicEisenstein.unitCuspFrequency_lift line 250
  13. lemma OAI.CubicEisenstein.unitLowerGauss_eq_unramified_of_frequency line 258
  14. def OAI.CubicEisenstein.unitCuspArithmeticSeries line 267
  15. theorem OAI.CubicEisenstein.unitCuspArithmeticSeries_eq line 270
  16. lemma OAI.CubicEisenstein.cuspTransition_dilate line 294
  17. lemma OAI.CubicEisenstein.cuspTransition_dilate_deriv line 301
  18. lemma OAI.CubicEisenstein.cuspTransition_dilate_second line 308
  19. def OAI.CubicEisenstein.cuspBaseDefectFactor line 322
  20. lemma OAI.CubicEisenstein.cuspBaseDefectFactor_continuous line 326
  21. lemma OAI.CubicEisenstein.cuspBaseDefectFactor_compact line 333
  22. lemma OAI.CubicEisenstein.cuspSeedDefectProfile_dilate line 341
  23. theorem OAI.CubicEisenstein.cuspSeedDefectProfile_dilate_bound line 349
  24. theorem OAI.CubicEisenstein.smoothCuspSeedDefect_dilate_bound line 377
  25. lemma OAI.CubicEisenstein.movingDefect_product_bound line 386
  26. lemma OAI.CubicEisenstein.movingDefect_inner_bound line 412
  27. theorem OAI.CubicEisenstein.cubicEisensteinResidue_orthogonal_of_rapid_cusp_decay line 430
  28. lemma OAI.CubicEisenstein.coset_decay_of_cusp_chart_decay line 468
  29. theorem OAI.CubicEisenstein.cubicEisensteinResidue_orthogonal_of_cusp_chart_decay line 490
  30. lemma OAI.CubicKubota.exists_congruent_cusp_completion line 510
  31. lemma OAI.CubicKubota.cusp_completion_upper_factor line 545
  32. lemma OAI.CubicKubota.bounded_power_factor line 575
  33. lemma OAI.CubicKubota.cube_average_cusp_reduction line 589