OAI/NumberTheory/DirichletL/Poisson/GaussianMoments.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.GaussianMoment.x_exp_neg_le line 21
  2. theorem OAI.GaussianMoment.gaussian_moment_term_bound line 36
  3. theorem OAI.ActualEisensteinCubic.rational_sixth_row_approx_two_factors line 56
  4. theorem OAI.ActualEisensteinCubic.rational_qNat line 109
  5. theorem OAI.ActualEisensteinCubic.rational_qNat_pow line 118
  6. theorem OAI.ActualEisensteinCubic.rational_sixth_injective line 131
  7. theorem OAI.ActualEisensteinCubic.rational_sixth_norm_interval line 138
  8. theorem OAI.ActualEisensteinCubic.rational_qNat_eq_one_iff line 147
  9. theorem OAI.ActualEisensteinCubic.rational_prime_factor_cases line 151
  10. theorem OAI.ActualEisensteinCubic.maximal_ideal_eq_span_of_mem line 196
  11. theorem OAI.ActualEisensteinCubic.rational_prime_ideal_cover line 204
  12. theorem OAI.ActualEisensteinCubic.rational_prime_sixth_row_approx line 230
  13. def OAI.RationalPrimeExtraction.selected line 275
  14. theorem OAI.RationalPrimeExtraction.lower_count_and_extract line 278
  15. theorem OAI.OscSpecial.real_quadratic_lower line 304
  16. theorem OAI.OscSpecial.schur_eq_real_det_div line 324
  17. theorem OAI.OscSpecial.determinant_real_components line 331
  18. theorem OAI.OscSpecial.first_real_coefficients line 351
  19. theorem OAI.OscSpecial.first_real_determinant line 366
  20. def OAI.OscSpecial.middleForm line 385
  21. theorem OAI.OscSpecial.middleForm_real line 390
  22. theorem OAI.OscSpecial.middleForm_exp line 397
  23. theorem OAI.OscSpecial.firstGaussian_summable line 406
  24. def OAI.OscSpecial.originalForm line 435
  25. theorem OAI.OscSpecial.originalForm_real line 438
  26. theorem OAI.OscSpecial.originalGaussian_summable line 444
  27. def OAI.OscSpecial.inverseForm line 464
  28. theorem OAI.OscSpecial.inverseForm_real line 468
  29. theorem OAI.OscSpecial.dualGaussian_inverseForm line 476
  30. theorem OAI.OscSpecial.dualGaussian_summable line 490
  31. theorem OAI.OscSpecial.binary_gaussian_poisson_real_det line 515
  32. def OAI.OscSpecial.q line 541
  33. def OAI.OscSpecial.A line 542
  34. def OAI.OscSpecial.B line 544
  35. def OAI.OscSpecial.D line 546
  36. def OAI.OscSpecial.R line 548
  37. theorem OAI.OscSpecial.coefficient_re line 550
  38. theorem OAI.OscSpecial.oscillatory_determinant line 554
  39. theorem OAI.OscSpecial.real_positive_definite line 569