OAI/NumberTheory/DirichletL/Eisenstein/CorrespondenceTests.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.cubeAverageMatrix_translate_lattice line 84
  2. lemma OAI.CubicEisenstein.cubeAverage_period_three line 93
  3. lemma OAI.CubicEisenstein.cubicSource_period_three line 131
  4. lemma OAI.CubicEisenstein.cubicSource_period_one line 139
  5. lemma OAI.CubicEisenstein.cubicSource_period_finTwo line 145
  6. lemma OAI.CubicEisenstein.cubicSource_cube_period_finTwo line 155
  7. theorem OAI.CubicEisenstein.cubeSource_summand_average line 168
  8. theorem OAI.CubicEisenstein.cubeSource_average_zero line 187
  9. theorem OAI.CubicEisenstein.cubeSource_primary_upper_average line 204
  10. theorem OAI.CubicEisenstein.cubeSource_levelTwo_upper_average line 248
  11. theorem OAI.CubicEisenstein.cubeSource_average_all_cusps line 271
  12. theorem OAI.CubicEisenstein.cubeSource_difference_average_zero line 288
  13. lemma OAI.CubicEisenstein.integralCoverFiberPoint_continuous line 325
  14. lemma OAI.CubicEisenstein.integralCoverMap_fiber line 334
  15. lemma OAI.CubicEisenstein.integralCoverMap_preimage_image line 354
  16. theorem OAI.CubicEisenstein.integralCoverMap_isClosedMap line 369
  17. theorem OAI.CubicEisenstein.integralCoverMap_isProperMap line 378
  18. theorem OAI.CubicEisenstein.integralCoverMap_compact_preimage line 390
  19. lemma OAI.CubicEisenstein.cubeCuspTriangular_norm_sq_pos line 407
  20. def OAI.CubicEisenstein.cubeReducedRemainder line 412
  21. lemma OAI.CubicEisenstein.cubeSource_remainder_summand line 418
  22. lemma OAI.CubicEisenstein.cubeSource_leading_sum line 429
  23. theorem OAI.CubicEisenstein.cubeSource_difference_eq_remainders line 461
  24. lemma OAI.CubicEisenstein.cubePrime_norm_ge_one line 504
  25. lemma OAI.CubicEisenstein.cubeReducedRemainder_bound line 512
  26. lemma OAI.CubicEisenstein.cube_normalized_sum_bound line 550
  27. theorem OAI.CubicEisenstein.cubeSource_difference_decay_from_representatives line 571
  28. lemma OAI.CubicEisenstein.integralCoverMap_hasCompactSupport line 610
  29. lemma OAI.CubicEisenstein.integralCoverTraceFunction_hasCompactSupport line 619
  30. def OAI.CubicEisenstein.kernelCorrespondenceFunction line 638
  31. lemma OAI.CubicEisenstein.kernelCorrespondenceFunction_lift line 643
  32. lemma OAI.CubicEisenstein.kernelCorrespondenceFunction_hasCompactSupport line 660
  33. lemma OAI.CubicEisenstein.kernelCorrespondenceFunction_contMDiff line 667
  34. def OAI.CubicEisenstein.kernelCorrespondenceTest line 679