OAI/NumberTheory/DirichletL/GaussSum/FiniteTranslations.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CompletedGauss.positive_cpow_comp_continuous line 83
  2. theorem OAI.CompletedGauss.besselSmoothingIntegrand_reflected_integrable line 88
  3. def OAI.CubicEisenstein.finiteTranslationMultiplier line 165
  4. lemma OAI.CubicEisenstein.finiteTranslationMultiplier_norm line 169
  5. def OAI.CubicEisenstein.SubexponentialBesselCoefficients.finiteTranslate line 180
  6. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.term_horizontal_translate line 194
  7. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.finiteTranslate_term line 202
  8. theorem OAI.CubicEisenstein.SubexponentialBesselCoefficients.finiteTranslate_series line 219
  9. theorem OAI.CubicEisenstein.SubexponentialBesselCoefficients.finiteTranslate_fullFunction line 230
  10. theorem OAI.CubicEisenstein.cubicSource_finite_translation line 248
  11. def OAI.CubicEisenstein.finiteAdditiveFourierCoeff line 261
  12. lemma OAI.CubicEisenstein.finiteAdditiveFourier_inversion line 265
  13. lemma OAI.CubicEisenstein.finiteAdditiveFourierCoeff_norm line 291
  14. def OAI.CubicEisenstein.thetaFourierTranslation line 305
  15. lemma OAI.CubicEisenstein.thetaFourierTranslation_phase line 309
  16. lemma OAI.CubicEisenstein.thetaFourierTranslation_inversion line 326
  17. lemma OAI.CubicEisenstein.breveE_star line 340
  18. lemma OAI.CubicEisenstein.finiteTranslationMultiplier_star line 349
  19. lemma OAI.CubicEisenstein.finiteTranslate_term_multiplier line 358
  20. def OAI.CubicEisenstein.finiteConjugateSource line 369
  21. lemma OAI.CubicEisenstein.finiteConjugateSource_eq_bessel line 373
  22. theorem OAI.CubicEisenstein.finiteConjugateSource_wirtingerBar line 385
  23. def OAI.CubicEisenstein.traceTwistedConjugateSource line 407
  24. theorem OAI.CubicEisenstein.traceTwistedConjugateSource_wirtingerBar line 413
  25. theorem OAI.CubicEisenstein.traceTwistedConjugateSource_wirtingerBar_zero line 424
  26. def OAI.CubicEisenstein.fixedThetaTwist line 453
  27. lemma OAI.CubicEisenstein.fixedThetaTwist_primary line 456
  28. lemma OAI.CubicEisenstein.fixedThetaTwist_not_primary line 460
  29. lemma OAI.CubicEisenstein.paperLambda_symbol_cube line 464
  30. lemma OAI.CubicEisenstein.paperLambda_symbol_norm line 469
  31. lemma OAI.CubicEisenstein.fixedThetaTwist_norm_le_one line 474
  32. theorem OAI.CubicEisenstein.fixedThetaTwist_periodic line 482
  33. def OAI.CubicEisenstein.fixedThetaQuotient line 502
  34. lemma OAI.CubicEisenstein.fixedThetaQuotient_mk line 505
  35. lemma OAI.CubicEisenstein.fixedThetaQuotient_norm_le_one line 512
  36. lemma OAI.CubicEisenstein.paperLambda_symbol_squarefree_cube line 516
  37. theorem OAI.CubicEisenstein.fixedThetaTwist_infinity_coefficient line 522
  38. lemma OAI.CubicEisenstein.sourceFourier_primary_squarefree_cube_preimage line 551
  39. theorem OAI.CubicEisenstein.sourceFourier_tsum_primary_pairs line 566