OAI/NumberTheory/DirichletL/GaussSum/QuadraticNormalization.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ActualEisensteinCubic.quadraticGammaO line 22
  2. theorem OAI.ActualEisensteinCubic.quadraticGammaO_traceLambda line 29
  3. theorem OAI.ActualEisensteinCubic.quadraticGammaO_negTraceLambda line 33
  4. theorem OAI.ActualEisensteinCubic.quadraticGammaO_rational line 37
  5. theorem OAI.ActualEisensteinCubic.quadraticGammaO_rational_odd line 41
  6. theorem OAI.PowerExtraction.from_mean_square_and_prime_rows_with_constant line 51
  7. theorem OAI.PowerExtraction.from_finite_sixth_power_rows_with_constant line 107
  8. theorem OAI.ActualEisensteinCubic.finite_actual_prime_extraction_with_constant line 141
  9. theorem OAI.PowerExtraction.dyadic_prime_error_bound line 202
  10. theorem OAI.ActualEisensteinCubic.cubicChar_unit_eq_one_of_card_mod_nine line 242
  11. theorem OAI.ActualEisensteinCubic.cubicChar_omega_agree_of_card_mod_nine line 277
  12. theorem OAI.ActualEisensteinCubic.cubicChar_units_agree_of_card_mod_nine line 290
  13. theorem OAI.ActualEisensteinCubic.eisenstein_coord_norm_zero line 330
  14. theorem OAI.ActualEisensteinCubic.quadraticTraceModChar_coordinate line 339
  15. theorem OAI.GaussianAbelPartition.tsum_by_finite_fibers line 365
  16. theorem OAI.GaussianAbelPartition.tsum_periodic_weighted_partition line 372
  17. theorem OAI.GaussianAbelPartition.actual_quadratic_gaussian_partition line 392
  18. theorem OAI.ActualEisensteinCubic.finite_actual_prime_extraction_dyadic line 417
  19. def OAI.GaussianFiberEquiv.fiberMap line 457
  20. theorem OAI.GaussianFiberEquiv.fiberMap_injective line 467
  21. theorem OAI.GaussianFiberEquiv.fiberMap_surjective line 476
  22. def OAI.GaussianFiberEquiv.fiberEquiv line 492
  23. theorem OAI.GaussianFiberEquiv.fiber_tsum line 499
  24. theorem OAI.RankTwoPoisson.schwartz_int_summable line 515
  25. theorem OAI.RankTwoPoisson.schwartz_int_norm_summable line 520
  26. theorem OAI.RankTwoPoisson.schwartz_int_poisson line 524
  27. theorem OAI.RankTwoPoisson.tensor_poisson line 529
  28. theorem OAI.RankTwoPoisson.gauss_int_summable line 545
  29. def OAI.RankTwoPoisson.cg line 553
  30. theorem OAI.RankTwoPoisson.cg_summable line 556
  31. theorem OAI.RankTwoPoisson.cg_poisson line 559
  32. theorem OAI.RankTwoPoisson.diagonal_gaussian_poisson line 565
  33. theorem OAI.RankTwoPoisson.real_gauss_summable line 583
  34. def OAI.RankTwoPoisson.eisQ line 589
  35. def OAI.RankTwoPoisson.eisGauss line 592
  36. theorem OAI.RankTwoPoisson.eisQ_lower line 595
  37. theorem OAI.RankTwoPoisson.eis_gauss_summable line 600
  38. def OAI.RankTwoPoisson.phase line 620
  39. def OAI.RankTwoPoisson.g1 line 623
  40. theorem OAI.RankTwoPoisson.phase_norm line 626
  41. theorem OAI.RankTwoPoisson.g1_summable line 629
  42. theorem OAI.RankTwoPoisson.eisGauss_split line 641
  43. theorem OAI.RankTwoPoisson.eis_exponent_identity line 652
  44. theorem OAI.RankTwoPoisson.first_transform_term line 666
  45. theorem OAI.RankTwoPoisson.first_poisson_slice line 681
  46. def OAI.RankTwoPoisson.dualTerm line 711
  47. theorem OAI.RankTwoPoisson.second_transform_term line 716
  48. theorem OAI.RankTwoPoisson.second_poisson_slice line 726
  49. theorem OAI.RankTwoPoisson.eisenstein_gaussian_poisson_iterated line 771
  50. theorem OAI.RankTwoPoisson.dualTerm_eq_eisGauss line 813
  51. theorem OAI.RankTwoPoisson.dualTerm_summable line 823
  52. theorem OAI.RankTwoPoisson.eisenstein_gaussian_poisson line 834