OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/Phase.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.OrdinaryDirichletMeanSquare.phase line 17
  2. def OAI.OrdinaryDirichletMeanSquare.gaussian line 19
  3. def OAI.OrdinaryDirichletMeanSquare.polynomial line 21
  4. def OAI.OrdinaryDirichletMeanSquare.gaussianConstant line 24
  5. lemma OAI.OrdinaryDirichletMeanSquare.norm_phase line 26
  6. lemma OAI.OrdinaryDirichletMeanSquare.phase_mul_conj line 29
  7. lemma OAI.OrdinaryDirichletMeanSquare.gaussian_nonneg line 37
  8. lemma OAI.OrdinaryDirichletMeanSquare.gaussian_integrable line 39
  9. lemma OAI.OrdinaryDirichletMeanSquare.gaussian_phase_integrable line 43
  10. lemma OAI.OrdinaryDirichletMeanSquare.gaussian_phase_integral line 54
  11. lemma OAI.OrdinaryDirichletMeanSquare.norm_gaussian_phase_integral line 66
  12. lemma OAI.OrdinaryDirichletMeanSquare.gaussian_polynomial_integrable line 73
  13. lemma OAI.OrdinaryDirichletMeanSquare.gaussian_pair_integrable line 87
  14. lemma OAI.OrdinaryDirichletMeanSquare.gaussian_polynomial_expansion line 96
  15. lemma OAI.OrdinaryDirichletMeanSquare.gaussian_polynomial_energy line 129
  16. lemma OAI.OrdinaryDirichletMeanSquare.geometric_row line 153
  17. lemma OAI.OrdinaryDirichletMeanSquare.geometric_exponential_row line 188
  18. lemma OAI.OrdinaryDirichletMeanSquare.log_separation line 209
  19. lemma OAI.OrdinaryDirichletMeanSquare.dist_real line 224
  20. lemma OAI.OrdinaryDirichletMeanSquare.gaussian_kernel_le line 232
  21. lemma OAI.OrdinaryDirichletMeanSquare.log_gaussian_row line 238
  22. lemma OAI.OrdinaryDirichletMeanSquare.finite_schur line 265
  23. lemma OAI.OrdinaryDirichletMeanSquare.logarithmic_gaussian_energy line 298
  24. lemma OAI.OrdinaryDirichletMeanSquare.polynomial_rescale line 315
  25. lemma OAI.OrdinaryDirichletMeanSquare.logarithmic_scaled_integrable line 325
  26. lemma OAI.OrdinaryDirichletMeanSquare.logarithmic_scaled_energy line 332
  27. lemma OAI.OrdinaryDirichletMeanSquare.logarithmic_interval_energy line 347