OAI/NumberTheory/DirichletL/Eisenstein/PrimePowerGaussSums.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.cubicUnitGaussSum_one line 83
  2. lemma OAI.CubicEisenstein.cubicUnitGaussSum_frequency_dvd line 92
  3. lemma OAI.CubicEisenstein.cubicUnitGaussSum_prime_power_zero line 96
  4. lemma OAI.CubicEisenstein.cubicUnitGaussSum_prime_power_too_large line 105
  5. lemma OAI.CubicEisenstein.unramifiedPrimeDeletedSeries_pow_mod line 119
  6. theorem OAI.CubicEisenstein.unramifiedCubicGaussSeries_prime_finite line 134
  7. lemma OAI.CubicEisenstein.unramifiedCubicGaussSeries_prime_zero_power line 147
  8. lemma OAI.CubicEisenstein.unramifiedCubicGaussSeries_prime_one_power line 157
  9. lemma OAI.CubicEisenstein.unramifiedCubicGaussSeries_prime_three_power line 175
  10. theorem OAI.CubicEisenstein.unramifiedCubicGaussSeries_prime_recurrence line 213
  11. structure OAI.CubicEisenstein.SubexponentialBesselCoefficients line 236
  12. def OAI.CubicEisenstein.SubexponentialBesselCoefficients.term line 244
  13. def OAI.CubicEisenstein.SubexponentialBesselCoefficients.amplitude line 248
  14. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.term_bessel line 252
  15. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.term_eq_amplitude line 270
  16. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.term_continuousOn line 276
  17. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.slab_bound line 295
  18. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.summable line 333
  19. def OAI.CubicEisenstein.SubexponentialBesselCoefficients.series line 339
  20. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_continuousOn_slab line 341
  21. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_continuousOn line 350
  22. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_uniform line 358
  23. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_bessel line 365
  24. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_period line 369
  25. def OAI.CubicEisenstein.SubexponentialBesselCoefficients.function line 378
  26. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.function_continuous line 380
  27. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_fourier line 400
  28. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_height_continuous line 452
  29. def OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction line 460
  30. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_continuous line 463
  31. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_fourier line 471
  32. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_period line 492
  33. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_height_continuous line 498
  34. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_height_memLp line 504
  35. theorem OAI.ShortDraftCRT.inverse_residue_congr line 525
  36. theorem OAI.ShortDraftCRT.inverse_weight_residue_congr line 531
  37. theorem OAI.ShortDraftCRT.fixed_additive_sector line 539
  38. theorem OAI.ShortDraftCRT.strong_sector_additive_congruences line 550
  39. def OAI.CubicEisenstein.translatedHeightCompact line 566
  40. lemma OAI.CubicEisenstein.translatedHeightCompact_isCompact line 569
  41. def OAI.CubicEisenstein.translatedHeightFourier line 573
  42. lemma OAI.CubicEisenstein.translatedHeightFourier_integral line 577
  43. lemma OAI.CubicEisenstein.translatedHeightFourier_restrict line 588
  44. def OAI.CubicEisenstein.translatedHeightFamily line 605
  45. lemma OAI.CubicEisenstein.translatedHeightFamily_analyticAt line 611
  46. lemma OAI.CubicEisenstein.translatedHeightFamily_residue_limit line 619
  47. lemma OAI.CubicEisenstein.translatedHeightFamily_initial line 628