OAI/NumberTheory/DirichletL/Poisson/OscillatoryGaussian.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.OscSpecial.oscillatory_gaussian_poisson line 22
  2. def OAI.OscSpecial.r line 39
  3. theorem OAI.OscSpecial.r_pos line 41
  4. theorem OAI.OscSpecial.inverseForm_explicit line 46
  5. theorem OAI.OscSpecial.dualGaussian_explicit line 75
  6. theorem OAI.ActualEisensteinCubic.dual_quadratic_trace_coeff line 104
  7. theorem OAI.ActualEisensteinCubic.coords_neg_second line 114
  8. theorem OAI.ActualEisensteinCubic.breveE_dual_quadratic_real_scale line 130
  9. theorem OAI.ActualEisensteinCubic.original_abel_gamma_limit line 159
  10. theorem OAI.ActualEisensteinCubic.actual_oscillatory_binary_coordinate line 204
  11. theorem OAI.ActualEisensteinCubic.actual_oscillatory_sum_eq_binary line 230
  12. def OAI.ActualEisensteinCubic.dualFrequencyEquiv line 270
  13. theorem OAI.ActualEisensteinCubic.dualFrequencyEquiv_norm_sq line 287
  14. theorem OAI.ActualEisensteinCubic.dualFrequencyEquiv_trace_phase line 294
  15. def OAI.GaussianMoment.realGauss line 311
  16. theorem OAI.GaussianMoment.realGauss_nonneg line 314
  17. theorem OAI.GaussianMoment.realGauss_summable line 317
  18. theorem OAI.GaussianMoment.realGauss_cast line 326
  19. theorem OAI.GaussianMoment.real_gaussian_mass line 334
  20. theorem OAI.ActualEisensteinCubic.dual_gaussian_is_actual_trace_phase line 372
  21. theorem OAI.ActualEisensteinCubic.actual_oscillatory_poisson line 405
  22. theorem OAI.OscSpecial.R_eq_four_r_div_q line 458
  23. theorem OAI.OscSpecial.sqrt_R_eq line 464
  24. theorem OAI.OscSpecial.prefactor_eq_real_sqrt line 473
  25. theorem OAI.OscSpecial.prefactor_tendsto line 492
  26. theorem OAI.GaussianMoment.eisQ_nonneg line 527
  27. theorem OAI.GaussianMoment.moment_term_bound line 531
  28. theorem OAI.GaussianMoment.moment_summable line 538
  29. theorem OAI.GaussianMoment.moment_tsum_bound line 547
  30. theorem OAI.GaussianMoment.moment_tsum_nonneg line 558
  31. theorem OAI.GaussianMoment.half_tendsto_within line 562
  32. theorem OAI.GaussianMoment.t_tendsto_zero line 572
  33. theorem OAI.GaussianMoment.scaled_half_mass_tendsto line 576
  34. theorem OAI.GaussianMoment.scaled_moment_vanishes line 583