OAI/NumberTheory/DirichletL/Eisenstein/CorrespondenceAdjoint.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.integralConjugatePullback_inverse_left line 84
  2. lemma OAI.CubicEisenstein.integralConjugatePullback_pairing line 99
  3. theorem OAI.CubicEisenstein.kernelCorrespondenceL2_pairing line 112
  4. theorem OAI.CubicEisenstein.kernelCorrespondenceL2_adjoint line 127
  5. lemma OAI.CubicEisenstein.continuous_period_integral line 148
  6. def OAI.CubicEisenstein.continuousCuspSlice line 167
  7. lemma OAI.CubicEisenstein.continuousCuspSlice_integrable line 170
  8. lemma OAI.CubicEisenstein.continuousCuspSlice_continuousOn line 189
  9. lemma OAI.CubicEisenstein.continuousCuspSlice_test line 212
  10. theorem OAI.CubicEisenstein.continuousCuspSlice_eq_of_tests line 234
  11. theorem OAI.CubicEisenstein.ramifiedSource_fourier_all_heights line 255
  12. lemma OAI.CubicEisenstein.continuous_period_fourier_bound line 299
  13. theorem OAI.CubicEisenstein.continuous_fourier_bessel_subexponential line 313
  14. theorem OAI.CubicEisenstein.continuous_periodic_eq_bessel line 355
  15. lemma OAI.CubicEisenstein.ninthCuspFrequency_three line 379
  16. lemma OAI.CubicEisenstein.sourceFourierKernel_cubic_amplitude line 384
  17. lemma OAI.CubicEisenstein.ramified_kernel_scaled_bessel line 400
  18. def OAI.CubicEisenstein.ramifiedScaledRow line 420
  19. def OAI.CubicEisenstein.ramifiedBesselValue line 423
  20. lemma OAI.CubicEisenstein.ramifiedScaledRow_continuous line 429
  21. lemma OAI.CubicEisenstein.ramifiedScaledRow_periodic line 439
  22. lemma OAI.CubicEisenstein.ramifiedScaledRow_zero line 446
  23. lemma OAI.CubicEisenstein.ramifiedScaledRow_fourier line 454
  24. lemma OAI.CubicEisenstein.ramifiedBesselValue_subexponential line 476
  25. def OAI.CubicEisenstein.ramifiedBesselCoefficients line 483
  26. theorem OAI.CubicEisenstein.ramifiedScaledRow_eq_bessel line 487
  27. theorem OAI.CubicEisenstein.ramifiedSource_cubic_decay line 495
  28. def OAI.CubicEisenstein.ramifiedCuspBesselTerm line 517
  29. lemma OAI.CubicEisenstein.ramifiedCuspBesselTerm_eq line 522
  30. lemma OAI.CubicEisenstein.ramifiedSource_eq_series line 531
  31. theorem OAI.CubicEisenstein.ramifiedSource_bessel line 542
  32. theorem OAI.CubicEisenstein.ramifiedSource_bessel_normal line 548
  33. theorem OAI.CubicEisenstein.ramifiedSource_exponential_decay line 560
  34. lemma OAI.CubicEisenstein.coverGradientAt_add line 576
  35. lemma OAI.CubicEisenstein.coverGradientAt_sub line 584
  36. lemma OAI.CubicEisenstein.coverGradientAt_smul line 592
  37. def OAI.CubicEisenstein.coverDirichletPair line 600
  38. lemma OAI.CubicEisenstein.coverDirichletPair_polarization line 603
  39. lemma OAI.CubicEisenstein.coverDirichletPair_comp line 621
  40. lemma OAI.CubicEisenstein.coverDirichletPair_sum_right line 641
  41. lemma OAI.CubicEisenstein.coverDirichletPair_norm_le line 647
  42. lemma OAI.CubicEisenstein.kernelDirichletPairDensity_eq_cover line 655