OAI/NumberTheory/DirichletL/Eisenstein/ResidualFourierSeries.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.cuspFrequency_norm_lower line 85
  2. def OAI.CubicEisenstein.cubicBesselUpperAway line 95
  3. lemma OAI.CubicEisenstein.cubicBesselUpperAway_pos line 98
  4. lemma OAI.CubicEisenstein.schlafliBesselK_cubic_upper_away line 102
  5. def OAI.CubicEisenstein.cubicResidualNonzeroTerm line 117
  6. lemma OAI.CubicEisenstein.cubicResidualNonzeroTerm_bessel line 121
  7. lemma OAI.CubicEisenstein.cubicResidualNonzeroTerm_continuousOn line 139
  8. lemma OAI.CubicEisenstein.cubicResidualNonzeroTerm_slab_bound line 158
  9. lemma OAI.CubicEisenstein.cubicResidualNonzeroTerm_summable line 199
  10. def OAI.CubicEisenstein.cubicResidualNonzeroSeries line 206
  11. lemma OAI.CubicEisenstein.cubicResidualNonzeroSeries_continuousOn_slab line 208
  12. lemma OAI.CubicEisenstein.cubicResidualNonzeroSeries_continuousOn line 217
  13. lemma OAI.CubicEisenstein.cubicResidualNonzeroSeries_uniform line 226
  14. lemma OAI.CubicEisenstein.cubicResidualNonzeroSeries_bessel line 233
  15. def OAI.CubicEisenstein.cubicResidualNonzeroFunction line 243
  16. lemma OAI.CubicEisenstein.cubicResidualNonzeroFunction_continuous line 246
  17. lemma OAI.CubicEisenstein.cubicResidualNonzeroSeries_period line 255
  18. def OAI.CubicEisenstein.cubicResidualModeAmplitude line 273
  19. lemma OAI.CubicEisenstein.cubicResidualNonzeroTerm_eq_amplitude line 277
  20. lemma OAI.CubicEisenstein.integral_cusp_character_product line 283
  21. lemma OAI.CubicEisenstein.cubicResidualNonzeroSeries_fourier line 296
  22. lemma OAI.CubicEisenstein.cubicResidualNonzeroFunction_heightFourier line 357
  23. lemma OAI.CubicEisenstein.cubicResidualNonzeroFunction_zero_heightFourier line 381
  24. lemma OAI.CubicEisenstein.cubicResidualNonzeroFunction_nonzero_heightFourier line 387
  25. lemma OAI.CubicEisenstein.cubicEisensteinResidue_nonzero_height_test_eq line 400
  26. lemma OAI.CubicEisenstein.ae_eq_of_boundedContinuous_height_tests line 413
  27. lemma OAI.CubicEisenstein.interval_ae_eq_of_boundedContinuous_height_tests line 428
  28. def OAI.CubicEisenstein.compactHeightMellin line 440
  29. lemma OAI.CubicEisenstein.compactHeightMellin_integrable line 443
  30. theorem OAI.CubicEisenstein.compactHeightMellin_differentiable line 452
  31. lemma OAI.CubicEisenstein.compactHeightMellin_analyticAt line 490
  32. def OAI.CubicEisenstein.cuspHeightConstantAverage line 500
  33. lemma OAI.CubicEisenstein.hyperbolicEisenstein_cusp_height_fourier_zero line 504
  34. lemma OAI.CubicEisenstein.kernelCuspHeightFourierFamily_zero_initial line 549
  35. def OAI.CubicEisenstein.weightedOutgoingConstant line 555
  36. def OAI.CubicEisenstein.baseOutgoingConstant line 560
  37. lemma OAI.CubicEisenstein.weightedOutgoingConstant_analyticAt line 564
  38. lemma OAI.CubicEisenstein.baseOutgoingConstant_analyticAt line 571
  39. lemma OAI.CubicEisenstein.cuspScatterHeightFactor_analyticAt line 581
  40. lemma OAI.CubicEisenstein.weightedOutgoingConstant_cross_identity line 588