OAI/NumberTheory/DirichletL/Poisson/QuadraticProfiles.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EisensteinSchwartzPoisson.quadraticSquareProfileCLM line 78
  2. theorem OAI.EisensteinSchwartzPoisson.quadraticSquareProfileCLM_apply line 85
  3. def OAI.EisensteinSchwartzPoisson.realAxisProfileCLM line 91
  4. theorem OAI.EisensteinSchwartzPoisson.realAxisProfileCLM_apply line 96
  5. def OAI.EisensteinSchwartzPoisson.squareFrequencyScaleCLM line 102
  6. def OAI.EisensteinSchwartzPoisson.quadraticTransformedSquareProfileCLM line 106
  7. theorem OAI.EisensteinSchwartzPoisson.quadraticTransformedSquareProfileCLM_apply line 110
  8. theorem OAI.EisensteinSchwartzPoisson.two_profile_seminorm_control line 117
  9. theorem OAI.EisensteinSchwartzPoisson.quadratic_principal_difference_large_scale line 135
  10. theorem OAI.EisensteinSchwartzPoisson.paperRadialFourier_nonzero_sum_uniform line 173
  11. theorem OAI.EisensteinSchwartzPoisson.maskedPrincipalRemainder_uniform line 190
  12. theorem OAI.EisensteinSchwartzPoisson.quadratic_principal_difference_uniform line 224
  13. theorem OAI.EisensteinSchwartzPoisson.two_regime_decay line 251
  14. theorem OAI.EisensteinSchwartzPoisson.quadratic_principal_difference_decay line 275
  15. theorem OAI.FirstPassCubeLabels.supportRay_star line 324
  16. theorem OAI.FirstPassCubeLabels.supportRay_mul line 328
  17. theorem OAI.FirstPassCubeLabels.columnG_ray_expansion line 332
  18. def OAI.FirstPassCubeLabels.coreRayCharacter line 344
  19. def OAI.FirstPassCubeLabels.coreRayCoefficient line 347
  20. theorem OAI.FirstPassCubeLabels.core_phase_ray_expansion line 352
  21. theorem OAI.FirstPassCubeLabels.coreRayCoefficient_norm_le line 385
  22. theorem OAI.FirstPassCubeLabels.coreRayCoefficient_mass line 395
  23. def OAI.FirstPassCubeLabels.coreRayTwist line 409
  24. theorem OAI.FirstPassCubeLabels.coreRayTwist_prod line 414
  25. theorem OAI.FirstPassCubeLabels.twisted_core_product line 419
  26. theorem OAI.FirstPassCubeLabels.actual_first_kernel_uniform_energy_envelope line 432
  27. def OAI.FirstPassCubeLabels.dilatedCoreRow line 499
  28. theorem OAI.FirstPassCubeLabels.cubeCoreCoefficient_continuous line 503
  29. theorem OAI.FirstPassCubeLabels.norm_cubeCoreCoefficient line 510
  30. theorem OAI.FirstPassCubeLabels.dilatedCoreRow_continuous line 516
  31. theorem OAI.FirstPassCubeLabels.dilatedCoreRow_uniform_bound line 524
  32. theorem OAI.FirstPassCubeLabels.dilatedCoreRow_integrable line 542
  33. def OAI.FirstPassCubeLabels.firstRayIntegrand line 553
  34. theorem OAI.FirstPassCubeLabels.firstRayIntegrand_integrable line 566
  35. theorem OAI.FirstPassCubeLabels.first_ray_energy_integral line 585