OAI/NumberTheory/DirichletL/Eisenstein/ResidualCuspDecay.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.residualCuspDecayRate line 84
  2. lemma OAI.CubicEisenstein.residualCuspDecayRate_pos line 86
  3. lemma OAI.CubicEisenstein.cubicResidualNonzeroTerm_cusp_bound line 92
  4. lemma OAI.CubicEisenstein.cubicResidualDirectionalTerm_cusp_majorant line 129
  5. lemma OAI.CubicEisenstein.cubicResidualDirectionalSeries_cusp_decay line 164
  6. theorem OAI.CubicEisenstein.cubicResidualFunction_wirtingerBar_cusp_decay line 189
  7. theorem OAI.ShortDraftCRT.exists_frequency_lift line 223
  8. theorem OAI.ShortDraftCRT.crossNum_congr_of_lift_dvd line 229
  9. theorem OAI.ShortDraftCRT.crossNum_fixed_sector_congr line 243
  10. theorem OAI.ShortDraftCRT.fixed_ray_completion_in_sector line 257
  11. theorem OAI.ShortDraftCRT.exists_sectorwise_completions line 284
  12. def OAI.ShortDraftCRT.LiftedRows line 318
  13. theorem OAI.ShortDraftCRT.exists_uniform_cusp_completions line 322
  14. theorem OAI.ShortDraftCRT.eisenstein_uniform_cusp_completions line 350
  15. theorem OAI.ShortDraftCusp.A3_principal_global line 380
  16. theorem OAI.ShortDraftCusp.A3_ramified_global line 386
  17. theorem OAI.ShortDraftCusp.A3_ramified_global_factor line 407
  18. theorem OAI.ShortDraftCusp.A3_unramified_global line 416
  19. theorem OAI.ShortDraftCusp.A3_unramified_global_factor line 441
  20. theorem OAI.ShortDraftCusp.A3_fixed_factor_congr line 447
  21. theorem OAI.ShortDraftCusp.A3_ramified_fixed_factor_congr line 459
  22. theorem OAI.ShortDraftCusp.A3_unramified_fixed_factor_congr line 474
  23. theorem OAI.ShortDraftCusp.norm_embedded_cubic_symbol line 478
  24. theorem OAI.ShortDraftCusp.norm_A3_principal_fixed_factor line 486
  25. theorem OAI.ShortDraftCusp.norm_A3_ramified_fixed_factor line 493
  26. theorem OAI.ShortDraftCusp.norm_A3_unramified_fixed_factor line 507
  27. lemma OAI.CubicEisenstein.cubicUnitGaussSum_norm_le line 522
  28. theorem OAI.CubicEisenstein.unramifiedCubicGaussSeries_summable_norm line 546
  29. abbrev OAI.CubicEisenstein.PrimeDeletedIdeal line 561
  30. def OAI.CubicEisenstein.unramifiedPrimeDeletedSeries line 563
  31. lemma OAI.CubicEisenstein.primaryGenerator_pow line 567
  32. lemma OAI.CubicEisenstein.gaussPrimeIdeal_prime line 571
  33. def OAI.CubicEisenstein.gaussPrimeFactorMap line 575
  34. lemma OAI.CubicEisenstein.gaussPrimeFactorMap_bijective line 581
  35. def OAI.CubicEisenstein.gaussPrimeFactorEquiv line 608
  36. lemma OAI.CubicEisenstein.primeDeleted_generator_coprime line 613
  37. lemma OAI.CubicEisenstein.primary_pow_congruence line 622
  38. lemma OAI.CubicEisenstein.gaussPrimeFactor_term line 626
  39. theorem OAI.CubicEisenstein.unramifiedCubicGaussSeries_prime_reindex line 645
  40. lemma OAI.CubicEisenstein.unramifiedPrimeDeletedSeries_cube_shift line 669