OAI/NumberTheory/DirichletL/Eisenstein/SmoothCuspCutoffs.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.cuspTransition line 79
  2. lemma OAI.CubicEisenstein.cuspTransition_contDiff line 81
  3. lemma OAI.CubicEisenstein.cuspTransition_zero line 85
  4. lemma OAI.CubicEisenstein.cuspTransition_one line 87
  5. lemma OAI.CubicEisenstein.cuspTransition_derivatives line 90
  6. def OAI.CubicEisenstein.positiveHeightPower line 102
  7. lemma OAI.CubicEisenstein.positiveHeightPower_eq_cpow line 103
  8. lemma OAI.CubicEisenstein.positiveHeightPower_hasDerivAt line 107
  9. lemma OAI.CubicEisenstein.positiveHeightPower_hasDerivAt_deriv line 113
  10. def OAI.CubicEisenstein.cuspSeedProfile line 126
  11. lemma OAI.CubicEisenstein.cuspSeedProfile_zero line 129
  12. lemma OAI.CubicEisenstein.cuspSeedProfile_incoming line 131
  13. lemma OAI.CubicEisenstein.cuspSeedProfile_hasDerivAt line 135
  14. lemma OAI.CubicEisenstein.cuspSeedProfile_hasDerivAt_deriv line 142
  15. def OAI.CubicEisenstein.cuspSeedDefectProfile line 162
  16. lemma OAI.CubicEisenstein.cuspSeedProfile_laplace_defect line 166
  17. lemma OAI.CubicEisenstein.cuspSeedDefectProfile_zero line 175
  18. lemma OAI.CubicEisenstein.cuspSeedDefectProfile_hasCompactSupport line 180
  19. def OAI.CubicEisenstein.rowHeight line 188
  20. lemma OAI.CubicEisenstein.rowHeight_pos line 192
  21. lemma OAI.CubicEisenstein.rowHeight_eq_transformedHeight line 194
  22. lemma OAI.CubicEisenstein.cosetHeight_upperPoint_rowHeight line 198
  23. lemma OAI.CubicEisenstein.rowHeight_contDiffAt line 204
  24. lemma OAI.CubicEisenstein.rowSmoothPower_eq_height line 214
  25. lemma OAI.CubicEisenstein.norm_smoothSummand_three line 218
  26. lemma OAI.CubicEisenstein.locally_finite_high_rows line 225
  27. def OAI.CubicEisenstein.heightPoincareField line 243
  28. lemma OAI.CubicEisenstein.heightPoincareField_locally_finite line 246
  29. lemma OAI.CubicEisenstein.heightPoincareField_contDiffAt line 257
  30. lemma OAI.CubicEisenstein.heightPoincareField_eq_cuspCorrection line 267
  31. lemma OAI.CubicEisenstein.positiveHeightPower_contDiffAt line 281
  32. lemma OAI.CubicEisenstein.cuspSeedProfile_contDiffAt line 289
  33. lemma OAI.CubicEisenstein.cuspSeedDefectProfile_contDiffAt line 294
  34. lemma OAI.CubicEisenstein.cuspSeedDefectProfile_continuous line 306
  35. lemma OAI.CubicEisenstein.cuspSeedDefectProfile_integrable line 317
  36. def OAI.CubicEisenstein.smoothCuspSeed line 322
  37. def OAI.CubicEisenstein.smoothCuspSeedDefect line 325
  38. lemma OAI.CubicEisenstein.smoothCuspSeed_automorphy line 328
  39. lemma OAI.CubicEisenstein.smoothCuspSeedDefect_automorphy line 331
  40. lemma OAI.CubicEisenstein.smoothCuspSeed_coordinate line 335
  41. lemma OAI.CubicEisenstein.smoothCuspSeedDefect_coordinate line 341
  42. lemma OAI.CubicEisenstein.smoothCuspSeed_contDiffAt line 348
  43. lemma OAI.CubicEisenstein.smoothCuspSeedDefect_contDiffAt line 353
  44. lemma OAI.CubicEisenstein.cuspCutoffCorrection_upperPoint line 360
  45. lemma OAI.CubicEisenstein.smoothCuspSeed_incoming line 367
  46. lemma OAI.CubicEisenstein.smoothCuspSeedDefect_support line 373
  47. def OAI.CubicEisenstein.rowLogHeight line 394
  48. lemma OAI.CubicEisenstein.exp_rowLogHeight line 398
  49. lemma OAI.CubicEisenstein.hasDerivAt_deriv_log_ratio line 403
  50. lemma OAI.CubicEisenstein.rowLogHeight_hasDerivAt line 415
  51. lemma OAI.CubicEisenstein.rowLogHeight_hasDerivAt_deriv line 434
  52. lemma OAI.CubicEisenstein.complex_profile_second_chain line 471
  53. lemma OAI.CubicEisenstein.positiveProfile_differentiable line 486
  54. lemma OAI.CubicEisenstein.positiveProfile_exp_derivatives line 492
  55. lemma OAI.CubicEisenstein.rowProfile_axis_derivatives line 508
  56. lemma OAI.CubicEisenstein.rowLog_eikonal line 551
  57. lemma OAI.CubicEisenstein.rowLog_laplacian line 555
  58. theorem OAI.CubicEisenstein.rowProfile_laplacian line 560
  59. lemma OAI.CubicEisenstein.axisLaplacian_congr_eventuallyEq line 580
  60. lemma OAI.CubicEisenstein.axisLaplacian_const_mul line 594
  61. lemma OAI.CubicEisenstein.axisLaplacian_finset_sum line 602