OAI/NumberTheory/DirichletL/GaussSum/GaussianDualLimit.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ActualEisensteinCubic.principal_absNorm_pow line 20
  2. theorem OAI.ActualEisensteinCubic.sixth_power_rows_within_norm_cutoff line 26
  3. def OAI.OscillatoryDeterminant.q line 59
  4. def OAI.OscillatoryDeterminant.A line 61
  5. def OAI.OscillatoryDeterminant.B line 62
  6. def OAI.OscillatoryDeterminant.D line 63
  7. theorem OAI.OscillatoryDeterminant.determinant line 65
  8. theorem OAI.ActualEisensteinCubic.breveE_bilinear_coordinates line 81
  9. theorem OAI.ActualEisensteinCubic.breveE_standard_dual_frequency line 92
  10. def OAI.EisensteinFiberShift.Q line 106
  11. def OAI.EisensteinFiberShift.q line 107
  12. def OAI.EisensteinFiberShift.shiftX line 108
  13. def OAI.EisensteinFiberShift.shiftY line 109
  14. theorem OAI.EisensteinFiberShift.exact_shift line 111
  15. def OAI.ShortDraftLatticeCount.rowNormBall line 125
  16. theorem OAI.ShortDraftLatticeCount.mem_rowNormBall_of_qNat_le line 130
  17. theorem OAI.ShortDraftLatticeCount.mem_rowNormBall_of_absNorm_le line 154
  18. theorem OAI.EisensteinGaussianPrefactor.sqrt_product line 163
  19. theorem OAI.EisensteinGaussianPrefactor.eta_times_prefactor line 176
  20. theorem OAI.ActualEisensteinCubic.sixth_power_rows_in_rowNormBall line 201
  21. theorem OAI.ActualEisensteinCubic.actual_oscillatory_gaussian_coordinate line 218
  22. theorem OAI.EisensteinGaussianPrefactor.complex_eta_times_prefactor line 249
  23. theorem OAI.ActualEisensteinCubic.finite_actual_prime_extraction_dyadic_ball line 279
  24. def OAI.OscillatoryDeterminant.r line 316
  25. theorem OAI.OscillatoryDeterminant.inverse_quadratic line 318
  26. theorem OAI.cheby_small_log line 340
  27. theorem OAI.rational_prime_three_interval_real_count line 353
  28. theorem OAI.rational_prime_three_interval_count line 428
  29. theorem OAI.RankTwoLimit.eisQ_nonneg line 470
  30. theorem OAI.RankTwoLimit.eisQ_pos line 474
  31. theorem OAI.RankTwoLimit.eisGauss_norm line 487
  32. def OAI.RankTwoLimit.dualTerm line 492
  33. def OAI.RankTwoLimit.limitTerm line 495
  34. theorem OAI.RankTwoLimit.dualTerm_tendsto line 498
  35. theorem OAI.RankTwoLimit.dual_sum_tendsto_one line 538
  36. theorem OAI.RankTwoLimit.dual_sum_tendsto_one_small_t line 566