OAI/NumberTheory/DirichletL/Eisenstein/CorrespondenceEnergy.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.kernelTestField_comp_contDiffAt line 86
  2. lemma OAI.CubicEisenstein.coverGradientAt_lift_continuous line 93
  3. def OAI.CubicEisenstein.kernelCorrespondencePairLift line 105
  4. lemma OAI.CubicEisenstein.kernelCorrespondencePairLift_continuous line 110
  5. lemma OAI.CubicEisenstein.kernelCorrespondencePairLift_invariant line 122
  6. def OAI.CubicEisenstein.kernelCorrespondencePair line 146
  7. lemma OAI.CubicEisenstein.kernelCorrespondencePair_projection line 152
  8. lemma OAI.CubicEisenstein.kernelCorrespondencePair_measurable line 157
  9. lemma OAI.CubicEisenstein.kernelCorrespondencePair_norm_le line 162
  10. lemma OAI.CubicEisenstein.kernelCorrespondencePair_integrable line 179
  11. lemma OAI.CubicEisenstein.kernelCorrespondencePairLift_kernel line 196
  12. lemma OAI.CubicEisenstein.kernelTestField_comp_inverse line 213
  13. lemma OAI.CubicEisenstein.kernelCorrespondencePair_trace line 224
  14. lemma OAI.CubicEisenstein.kernelCorrespondenceForm_integral line 254
  15. lemma OAI.CubicEisenstein.kernelCorrespondencePair_conjugate line 264
  16. theorem OAI.CubicEisenstein.kernelCorrespondenceForm_adjoint line 288
  17. lemma OAI.CubicEisenstein.kernelCorrespondenceEnergy_pairing_core line 329
  18. theorem OAI.CubicEisenstein.kernelCorrespondenceEnergy_pairing line 340
  19. lemma OAI.CubicEisenstein.kernelCorrespondenceEnergy_pairing_left line 355
  20. lemma OAI.CubicEisenstein.kernelCorrespondenceL2_pairing_left line 362
  21. theorem OAI.CubicEisenstein.kernelCorrespondence_variationalSolution line 369
  22. theorem OAI.CubicEisenstein.kernelCorrespondence_variationalResolvent line 379
  23. theorem OAI.CubicEisenstein.kernelCorrespondence_operatorGraph line 386
  24. theorem OAI.CubicEisenstein.kernelCorrespondence_eigenvector line 393
  25. lemma OAI.CubicEisenstein.cuspFrequency_mul_right line 410
  26. lemma OAI.CubicEisenstein.cusp_character_continuous line 415
  27. lemma OAI.CubicEisenstein.cusp_character_fractional_period line 421
  28. lemma OAI.CubicEisenstein.period_fourier_fractional_translation line 434
  29. lemma OAI.CubicEisenstein.cube_upperPoint_continuous line 456
  30. theorem OAI.CubicEisenstein.cubeAverage_fourier line 463
  31. theorem OAI.CubicEisenstein.cubeSource_fourier line 546
  32. lemma OAI.CubicEisenstein.cubeSource_amplitude_of_eigenrelation line 555
  33. lemma OAI.CubicEisenstein.schlafliBesselK_cubic_ne_zero line 577
  34. theorem OAI.CubicEisenstein.sourceResidualFourierCoefficient_cube_of_eigenrelation line 584