OAI/NumberTheory/DirichletL/Eisenstein/InverseCuspCoordinates.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.inverseCuspCoordinates line 82
  2. lemma OAI.CubicEisenstein.inverseCuspCoordinates_height_pos line 85
  3. lemma OAI.CubicEisenstein.inverseCuspCoordinates_line line 90
  4. theorem OAI.CubicEisenstein.inverse_cusp_action line 95
  5. lemma OAI.CubicEisenstein.real_linear_horizontal_decompose line 146
  6. lemma OAI.CubicEisenstein.real_linear_wirtinger_swap line 155
  7. theorem OAI.CubicEisenstein.inverse_cusp_wirtingerBar line 167
  8. def OAI.CubicEisenstein.horizontalWirtingerZ line 190
  9. lemma OAI.CubicEisenstein.horizontalWirtingerZ_eq_fderiv line 194
  10. theorem OAI.CubicEisenstein.inverse_cusp_wirtinger_rule line 210
  11. theorem OAI.CubicEisenstein.cusp_mellin_reflection line 227
  12. theorem OAI.CubicEisenstein.cusp_mellin_reflection_of_identity line 241
  13. def OAI.CubicEisenstein.horizontalPhaseCLM line 259
  14. lemma OAI.CubicEisenstein.horizontalPhaseCLM_apply line 264
  15. lemma OAI.CubicEisenstein.brevePhase_hasFDerivAt line 269
  16. def OAI.CubicEisenstein.SubexponentialBesselCoefficients.amplitudeDeriv line 278
  17. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.amplitude_hasDerivAt line 284
  18. def OAI.CubicEisenstein.SubexponentialBesselCoefficients.termFDeriv line 300
  19. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.term_hasFDerivAt line 307
  20. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.weighted_bessel_bounds line 351
  21. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.amplitudeDeriv_norm_le line 394
  22. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.termFDeriv_norm_le line 410
  23. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.termFDeriv_slab_bound line 439
  24. lemma OAI.CubicEisenstein.summable_one_add_norm_exp_neg_cuspFrequency line 483
  25. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.termFDeriv_summable line 491
  26. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_hasFDerivAt line 499
  27. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_differentiableAt line 519
  28. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_cusp_eq line 522
  29. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_cusp_differentiableAt line 528
  30. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_split_differentiableAt line 540
  31. def OAI.CubicEisenstein.truncatedCuspProfile line 553
  32. lemma OAI.CubicEisenstein.truncatedCuspProfile_eventually_top line 556
  33. lemma OAI.CubicEisenstein.truncatedCuspProfile_eventually_zero line 561
  34. lemma OAI.CubicEisenstein.truncatedCuspProfile_locallyIntegrable line 567
  35. theorem OAI.CubicEisenstein.truncatedCuspProfile_mellin_entire line 583