OAI/NumberTheory/DirichletL/Reciprocity/CubeCorrespondence.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicKubota.cubeDiagonal line 84
  2. def OAI.CubicKubota.cubeCorrespondence line 86
  3. def OAI.CubicKubota.cubeCorrespondenceLeft line 116
  4. def OAI.CubicKubota.cubeCorrespondenceRight line 119
  5. lemma OAI.CubicKubota.cubeCorrespondence_entries line 122
  6. lemma OAI.CubicKubota.cubeCorrespondenceLeft_injective line 139
  7. lemma OAI.CubicKubota.cubeCorrespondenceRight_injective line 156
  8. lemma OAI.CubicKubota.cubeCorrespondence_value line 173
  9. lemma OAI.CubicKubota.cubeCorrespondence_character line 196
  10. def OAI.CubicKubota.cubePrincipalLevel line 207
  11. lemma OAI.CubicKubota.cubePrincipalLevel_entry line 211
  12. lemma OAI.CubicKubota.cubePrincipalLevel_finiteIndex line 223
  13. lemma OAI.CubicKubota.cubePrincipalLevel_left_mate line 230
  14. lemma OAI.CubicKubota.cubePrincipalLevel_right_mate line 264
  15. lemma OAI.CubicKubota.cubePrincipalLevel_le_left_range line 299
  16. lemma OAI.CubicKubota.cubePrincipalLevel_le_right_range line 305
  17. lemma OAI.CubicKubota.cubeCorrespondence_finite_covers line 311
  18. def OAI.CubicKubota.cubeKernelCorrespondence line 327
  19. def OAI.CubicKubota.cubeKernelLeft line 330
  20. lemma OAI.CubicKubota.cubeKernel_right_mem line 335
  21. def OAI.CubicKubota.cubeKernelRight line 341
  22. lemma OAI.CubicKubota.cubeKernelLeft_range line 347
  23. lemma OAI.CubicKubota.cubeKernelRight_range line 361
  24. lemma OAI.CubicKubota.cubeKernel_finite_covers line 375
  25. def OAI.CubicKubota.cubeKernelLeftGlobal line 395
  26. def OAI.CubicKubota.cubeKernelRightGlobal line 398
  27. lemma OAI.CubicKubota.cubeKernelLeftGlobal_le line 402
  28. lemma OAI.CubicKubota.cubeKernelRightGlobal_le line 407
  29. lemma OAI.CubicKubota.finiteIndex_subtype_image line 412
  30. lemma OAI.CubicKubota.cubeKernelGlobal_finite_covers line 419
  31. lemma OAI.CubicKubota.cubeKernelGlobal_intertwining line 436
  32. lemma OAI.CubicKubota.cubeArchimedean_correspondence line 445
  33. def OAI.CubicEisenstein.cuspBarProfile line 502
  34. def OAI.CubicEisenstein.cuspZProfile line 505
  35. lemma OAI.CubicEisenstein.cuspBarProfile_positive line 508
  36. lemma OAI.CubicEisenstein.cuspZProfile_positive line 512
  37. lemma OAI.CubicEisenstein.horizontalWirtingerZ_star line 516
  38. def OAI.CubicEisenstein.SubexponentialBesselCoefficients.directionalSeries line 525
  39. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.directionalSeries_continuousOn_slab line 528
  40. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.directionalSeries_continuousOn line 540
  41. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.cuspBarProfile_full_eq line 550
  42. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.cuspZProfile_full_eq line 560
  43. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.cuspBarProfile_continuousOn line 570
  44. lemma OAI.CubicEisenstein.SubexponentialBesselCoefficients.cuspZProfile_continuousOn line 579
  45. lemma OAI.CubicEisenstein.cuspBarProfile_source_continuousOn line 590
  46. lemma OAI.CubicEisenstein.cuspZProfile_source_continuousOn line 595
  47. lemma OAI.CubicEisenstein.cuspBarProfile_conjugate_eq line 600
  48. lemma OAI.CubicEisenstein.cuspZProfile_conjugate_eq line 605
  49. lemma OAI.CubicEisenstein.cuspBarProfile_conjugate_continuousOn line 610
  50. lemma OAI.CubicEisenstein.cuspZProfile_conjugate_continuousOn line 615
  51. lemma OAI.CubicEisenstein.cuspBarProfile_source_isBigO line 620
  52. lemma OAI.CubicEisenstein.cuspZProfile_source_isBigO line 630
  53. lemma OAI.CubicEisenstein.cuspBarProfile_conjugate_isBigO line 640
  54. lemma OAI.CubicEisenstein.cuspZProfile_conjugate_isBigO line 648