OAI/NumberTheory/DirichletL/Reciprocity/KubotaCharacter.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicKubota.rationalEmbedding line 83
  2. def OAI.CubicKubota.levelThreeConjugate line 86
  3. lemma OAI.CubicKubota.levelThree_bottom_primary line 92
  4. lemma OAI.CubicKubota.value_inverse_formula line 95
  5. lemma OAI.CubicKubota.value_upper_formula line 102
  6. theorem OAI.CubicKubota.value_conjugate_S line 127
  7. theorem OAI.CubicKubota.complexCharacter_conjugate_S line 137
  8. theorem OAI.CubicJacobiGlobal.symbol_shift_by_self line 146
  9. theorem OAI.CubicKubota.value_conjugate_T line 168
  10. lemma OAI.CubicKubota.levelThreeConjugate_one line 178
  11. lemma OAI.CubicKubota.levelThreeConjugate_mul line 182
  12. def OAI.CubicKubota.characterConjugationStabilizer line 187
  13. theorem OAI.CubicKubota.value_conjugate_rational line 196
  14. theorem OAI.CubicKubota.complexCharacter_conjugate_rational line 209
  15. def OAI.CubicJacobiGlobal.rationalPrimary line 222
  16. lemma OAI.CubicJacobiGlobal.rationalPrimary_coord line 224
  17. lemma OAI.CubicJacobiGlobal.rationalPrimary_primary line 245
  18. lemma OAI.CubicJacobiGlobal.rationalPrimary_denominator line 250
  19. lemma OAI.CubicJacobiGlobal.rationalPrimary_numerator line 256
  20. lemma OAI.CubicJacobiGlobal.rational_symbol_mul line 263
  21. lemma OAI.CubicJacobiGlobal.rational_symbol_three line 269
  22. lemma OAI.CubicJacobiGlobal.rational_symbol_reciprocity line 286
  23. lemma OAI.CubicJacobiGlobal.rational_symbol_mod line 297
  24. theorem OAI.CubicJacobiGlobal.rational_symbol_eq_one line 304
  25. lemma OAI.CubicJacobiGlobal.primary_int_natAbs_not_three line 345
  26. theorem OAI.CubicJacobiGlobal.integer_symbol_eq_one line 359
  27. theorem OAI.CubicKubota.value_rational_intersection line 390
  28. theorem OAI.CubicKubota.complexCharacter_rational_intersection line 402
  29. def OAI.CubicKubota.levelTwo line 411
  30. lemma OAI.CubicKubota.levelThree_le_levelTwo line 423
  31. lemma OAI.CubicKubota.rational_mem_levelTwo line 427
  32. lemma OAI.CubicKubota.levelTwo_eq_sup line 430
  33. lemma OAI.CubicKubota.complexCharacter_product_well_defined line 440
  34. def OAI.CubicKubota.levelTwoLeft line 456
  35. def OAI.CubicKubota.levelTwoRight line 458
  36. lemma OAI.CubicKubota.levelTwo_product line 460
  37. def OAI.CubicKubota.levelTwoValue line 464
  38. lemma OAI.CubicKubota.levelTwoValue_of_product line 466
  39. def OAI.CubicKubota.levelTwoComplexCharacter line 471
  40. lemma OAI.CubicKubota.levelTwoComplexCharacter_restrict line 486
  41. lemma OAI.CubicKubota.levelTwoComplexCharacter_rational line 490
  42. lemma OAI.CubicKubota.levelTwoComplexCharacter_cube line 494
  43. lemma OAI.CubicKubota.norm_levelTwoComplexCharacter line 497
  44. theorem OAI.CubicKubota.globalKubotaKernel_conjugate line 509
  45. def OAI.CubicKubota.kernelInLevelTwo line 526
  46. instance OAI.CubicKubota.kernelInLevelTwo_normal line 528
  47. theorem OAI.CubicKubota.globalKubotaKernel_rational_conjugate_iff line 531
  48. def OAI.CubicEisenstein.cuspHeightCompact line 550
  49. lemma OAI.CubicEisenstein.cuspHeightCompact_isCompact line 553
  50. lemma OAI.CubicEisenstein.cuspPeriodStrip_subset_heightCompact line 558
  51. lemma OAI.CubicEisenstein.cuspPeriodStrip_measure_ne_top_of_pos line 566
  52. theorem OAI.CubicEisenstein.cuspPeriodStripFiniteVolume line 572
  53. lemma OAI.CubicEisenstein.cuspStrip_restrict_le_compact line 576
  54. abbrev OAI.CubicEisenstein.CuspHeightStripL2 line 582
  55. def OAI.CubicEisenstein.kernelCuspHeightPullback line 584
  56. lemma OAI.CubicEisenstein.kernelCuspHeightPullback_ae line 588
  57. lemma OAI.CubicEisenstein.kernelCuspHeight_quasiMeasurePreserving line 597
  58. def OAI.CubicEisenstein.cuspHeightQuotientCompact line 608
  59. lemma OAI.CubicEisenstein.cuspHeightQuotientCompact_isCompact line 611
  60. lemma OAI.CubicEisenstein.cuspPeriodStrip_image_subset line 615
  61. def OAI.CubicEisenstein.positiveEuclideanStrip line 619
  62. lemma OAI.CubicEisenstein.positiveEuclideanStrip_measurable line 622
  63. lemma OAI.CubicEisenstein.positiveEuclideanStrip_positive line 625
  64. lemma OAI.CubicEisenstein.positiveEuclideanStrip_preimage line 630
  65. lemma OAI.CubicEisenstein.cuspPeriodStrip_integral_coordinates_of_pos line 637
  66. lemma OAI.CubicEisenstein.cuspCoordinateLift_weighted_integrable_of_pos line 670