OAI/NumberTheory/DirichletL/Poisson/BinaryGaussian.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RankTwoComplex.lattice_gaussian_summable_of_re_bound line 22
  2. def OAI.RankTwoComplex.schur line 45
  3. def OAI.RankTwoComplex.binaryGaussian line 47
  4. def OAI.RankTwoComplex.firstGaussian line 51
  5. def OAI.RankTwoComplex.dualGaussian line 56
  6. theorem OAI.RankTwoComplex.binary_split line 61
  7. theorem OAI.RankTwoComplex.first_exponent_identity line 71
  8. theorem OAI.RankTwoComplex.first_transform_term line 82
  9. theorem OAI.RankTwoComplex.first_poisson_slice line 90
  10. theorem OAI.RankTwoComplex.second_poisson_slice line 121
  11. theorem OAI.RankTwoComplex.binary_gaussian_poisson line 165
  12. def OAI.GaussianShiftedPartition.representative line 221
  13. theorem OAI.GaussianShiftedPartition.representative_spec line 224
  14. theorem OAI.GaussianShiftedPartition.actual_quadratic_shifted_partition line 228
  15. def OAI.RankTwoAffine.binaryGaussian line 257
  16. def OAI.RankTwoAffine.firstGaussian line 262
  17. def OAI.RankTwoAffine.dualGaussian line 268
  18. theorem OAI.RankTwoAffine.binary_split line 274
  19. theorem OAI.RankTwoAffine.first_exponent_identity line 285
  20. theorem OAI.RankTwoAffine.first_transform_term line 299
  21. theorem OAI.RankTwoAffine.first_poisson_slice line 308
  22. theorem OAI.RankTwoAffine.second_poisson_slice line 340
  23. theorem OAI.RankTwoAffine.affine_gaussian_poisson line 372
  24. theorem OAI.ActualEisensteinCubic.eisEmbedding_eval_norm_sq line 428
  25. theorem OAI.ActualEisensteinCubic.fiber_coordinates line 445
  26. theorem OAI.ActualEisensteinCubic.fiber_quadratic_expansion line 456
  27. theorem OAI.ActualEisensteinCubic.eisEmbedding_fiber_norm_sq line 468
  28. theorem OAI.ActualEisensteinCubic.coordinate_norm_pos_of_nonzero line 480
  29. def OAI.RankTwoEisShift.Q line 496
  30. def OAI.RankTwoEisShift.shifted line 498
  31. def OAI.RankTwoEisShift.A line 501
  32. def OAI.RankTwoEisShift.B line 502
  33. def OAI.RankTwoEisShift.D line 503
  34. def OAI.RankTwoEisShift.U line 504
  35. def OAI.RankTwoEisShift.V line 505
  36. def OAI.RankTwoEisShift.C line 506
  37. theorem OAI.RankTwoEisShift.shifted_eq_affine line 509
  38. theorem OAI.RankTwoEisShift.schur_eis line 518
  39. theorem OAI.RankTwoEisShift.schur_eis_pos line 526
  40. def OAI.RankTwoEisShift.dualPhase line 532
  41. theorem OAI.RankTwoEisShift.shifted_dual_term line 535
  42. theorem OAI.RankTwoEisShift.shifted_real_gauss_summable line 552
  43. def OAI.RankTwoEisShift.middlePhase line 571
  44. theorem OAI.RankTwoEisShift.middlePhase_norm line 574
  45. theorem OAI.RankTwoEisShift.shifted_middle_term line 578
  46. theorem OAI.RankTwoEisShift.middle_norm line 597
  47. theorem OAI.RankTwoEisShift.affine_middle_summable line 606
  48. theorem OAI.RankTwoEisShift.dualPhase_norm line 627
  49. theorem OAI.RankTwoEisShift.affine_dual_summable line 631
  50. theorem OAI.RankTwoEisShift.shifted_summable line 651
  51. theorem OAI.RankTwoEisShift.affine_original_summable line 687
  52. theorem OAI.RankTwoEisShift.shifted_eisenstein_gaussian_poisson line 699