OAI/NumberTheory/DirichletL/Eisenstein/ConjugateCuspProfiles.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CubicEisenstein.cuspBarProfile_conjugate_reflection line 84
  2. theorem OAI.CubicEisenstein.conjugateSource_principal_cusp_mellin_entire line 101
  3. theorem OAI.CubicEisenstein.conjugateSource_cusp_mellin_reflection line 124
  4. lemma OAI.CubicEisenstein.cubicBesselIntegralDeriv_continuousAt line 142
  5. lemma OAI.CubicEisenstein.schlafliBesselK_cubic_derivative_continuousAt line 164
  6. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.amplitudeDeriv_continuousAt line 178
  7. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.termFDeriv_continuousAt line 190
  8. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.seriesFDeriv_continuousOn_slab line 218
  9. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.series_contDiffAt_one line 228
  10. def OAI.CubicEisenstein.cuspSpatialInput line 245
  11. def OAI.CubicEisenstein.cuspSpatialOutput line 246
  12. lemma OAI.CubicEisenstein.cuspSpatialInput_contDiff line 248
  13. lemma OAI.CubicEisenstein.cuspSpatialOutput_contDiff line 259
  14. lemma OAI.CubicEisenstein.cuspSpatialInput_horizontal line 262
  15. lemma OAI.CubicEisenstein.cuspSpatialAction_lift line 265
  16. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_cusp_contDiffAt_one line 285
  17. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_translate_cusp_contDiffAt_one line 302
  18. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.fullFunction_translate_split_contDiffAt_one line 316
  19. lemma OAI.CubicEisenstein.cubicSourceResidualFunction_translate_split_contDiffAt_one line 324
  20. lemma OAI.CubicEisenstein.cubicSourceConjugateFunction_translate_split_contDiffAt_one line 330
  21. lemma OAI.CubicEisenstein.horizontalWirtingerBar_eq_fderiv line 336
  22. lemma OAI.CubicEisenstein.cuspBarProfile_continuousOn_of_contDiff line 352
  23. lemma OAI.CubicEisenstein.cuspZProfile_continuousOn_of_contDiff line 372
  24. lemma OAI.CubicEisenstein.cuspBarProfile_source_translate_continuousOn line 392
  25. lemma OAI.CubicEisenstein.cuspZProfile_source_translate_continuousOn line 397
  26. lemma OAI.CubicEisenstein.cuspBarProfile_conjugate_translate_continuousOn line 402
  27. lemma OAI.CubicEisenstein.cuspZProfile_conjugate_translate_continuousOn line 407
  28. lemma OAI.CubicEisenstein.ninth_trace_character_period line 421
  29. lemma OAI.CubicEisenstein.ramifiedSource_scaled_periodic10 line 428
  30. lemma OAI.CubicEisenstein.ramifiedSource_scaled_periodic19 line 440
  31. lemma OAI.CubicEisenstein.periodic_integral_zero_of_eigen_translation line 452
  32. theorem OAI.CubicEisenstein.ramifiedSource_zero_mode10 line 462
  33. theorem OAI.CubicEisenstein.ramifiedSource_zero_mode19 line 474
  34. abbrev OAI.CubicEisenstein.UnitLowerData line 499
  35. def OAI.CubicEisenstein.unitLowerToPrimitive line 501
  36. lemma OAI.CubicEisenstein.unitLowerToPrimitive_bijective line 513
  37. def OAI.CubicEisenstein.unitLowerEquiv line 547
  38. lemma OAI.CubicEisenstein.rowOperator_lowerCusp line 550
  39. lemma OAI.CubicEisenstein.unitLower_row_phase line 559
  40. def OAI.CubicEisenstein.unitLowerTerm line 573
  41. lemma OAI.CubicEisenstein.unitLower_summand line 578
  42. theorem OAI.CubicEisenstein.unitLowerEisenstein_eq_rows line 603