OAI/NumberTheory/DirichletL/Eisenstein/FundamentalDomain.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.integralRowPair line 83
  2. lemma OAI.CubicEisenstein.integralRowPair_injective line 86
  3. lemma OAI.CubicEisenstein.matrixFrobenius_integral line 94
  4. lemma OAI.CubicEisenstein.integralRowEnergy_nonneg line 100
  5. theorem OAI.CubicEisenstein.integral_frobenius_sublevel_finite line 104
  6. theorem OAI.CubicEisenstein.integral_hyperbolic_sublevel_finite line 115
  7. theorem OAI.CubicEisenstein.subgroup_hyperbolic_sublevel_finite line 120
  8. theorem OAI.CubicEisenstein.subgroup_orbit_minimum line 125
  9. lemma OAI.CubicEisenstein.integralComplexMatrix_injective line 145
  10. lemma OAI.CubicEisenstein.levelThree_trace_divisible_nine line 152
  11. lemma OAI.CubicEisenstein.unitary_row_normSq line 166
  12. lemma OAI.CubicEisenstein.unitary_trace_norm_le_two line 175
  13. lemma OAI.CubicEisenstein.unitary_trace_two_eq_one line 186
  14. lemma OAI.CubicEisenstein.matrix_trace_conjugate line 212
  15. lemma OAI.CubicEisenstein.levelThree_unitary_conjugate_eq_one line 222
  16. theorem OAI.CubicEisenstein.levelThree_action_free line 256
  17. def OAI.CubicEisenstein.hyperbolicKeyCoordinates line 268
  18. def OAI.CubicEisenstein.hyperbolicOrderKey line 274
  19. lemma OAI.CubicEisenstein.hyperbolicOrderKey_injective line 276
  20. lemma OAI.CubicEisenstein.hyperbolicOrderKey_lt_of_frobenius line 291
  21. lemma OAI.CubicEisenstein.hyperbolicKeyCoordinates_continuous line 299
  22. lemma OAI.CubicEisenstein.hyperbolicOrderKey_lt_measurable line 303
  23. lemma OAI.CubicEisenstein.hyperbolicOrderKey_le_measurable line 321
  24. instance OAI.CubicEisenstein.integralSLCountable line 332
  25. instance OAI.CubicEisenstein.integralSubgroupHyperbolicAction line 337
  26. lemma OAI.CubicEisenstein.integralSubgroup_smul line 340
  27. def OAI.CubicEisenstein.hyperbolicFundamentalSet line 343
  28. lemma OAI.CubicEisenstein.hyperbolicFundamentalSet_measurable line 346
  29. lemma OAI.CubicEisenstein.exists_key_orbit_minimum line 355
  30. lemma OAI.CubicEisenstein.hyperbolicFundamentalSet_covers line 368
  31. lemma OAI.CubicEisenstein.hyperbolicFundamentalSet_orbit_unique line 374
  32. lemma OAI.CubicEisenstein.subgroup_action_free line 382
  33. theorem OAI.CubicEisenstein.hyperbolicFundamentalSet_isFundamentalDomain line 388
  34. lemma OAI.CubicEisenstein.globalKubotaKernel_le_levelThree line 400
  35. theorem OAI.CubicEisenstein.globalKubotaKernel_isFundamentalDomain line 404
  36. instance OAI.CubicEisenstein.integralSubgroupMeasurableAction line 416
  37. instance OAI.CubicEisenstein.integralSubgroupVolumeInvariant line 420
  38. lemma OAI.CubicEisenstein.measurable_integralOrbitProjection line 428
  39. def OAI.CubicEisenstein.integralQuotientVolume line 431
  40. lemma OAI.CubicEisenstein.quotient_projection_measurePreserving line 434
  41. theorem OAI.CubicEisenstein.integralQuotientVolume_independent line 439
  42. lemma OAI.CubicEisenstein.integralQuotientVolume_integral line 454
  43. lemma OAI.CubicEisenstein.hyperbolicEuclideanVolume_ne_zero line 460
  44. lemma OAI.CubicEisenstein.hyperbolicVolume_ne_zero line 476
  45. lemma OAI.CubicEisenstein.integralQuotientVolume_ne_zero line 479
  46. abbrev OAI.CubicEisenstein.KernelQuotientL2 line 489
  47. example OAI.CubicEisenstein.(example at line 490) line 490
  48. example OAI.CubicEisenstein.(example at line 491) line 491
  49. lemma OAI.CubicEisenstein.kernel_eisenstein_invariant line 493
  50. def OAI.CubicEisenstein.kernelQuotientEisenstein line 501
  51. lemma OAI.CubicEisenstein.kernelQuotientEisenstein_mk line 508
  52. lemma OAI.CubicEisenstein.kernel_seed_invariant line 512
  53. lemma OAI.CubicEisenstein.kernel_defect_invariant line 519
  54. def OAI.CubicEisenstein.kernelQuotientSeed line 526
  55. def OAI.CubicEisenstein.kernelQuotientDefect line 532
  56. def OAI.CompletedGauss.largeCubeCoefficient line 545
  57. theorem OAI.CompletedGauss.largeCubeCoefficient_zero line 549
  58. theorem OAI.CompletedGauss.largeCubeCoefficient_norm_le line 552
  59. theorem OAI.CompletedGauss.largeCubeCoefficient_support line 570
  60. theorem OAI.CompletedGauss.large_cube_convolution line 583
  61. theorem OAI.CompletedGauss.large_cube_inner_reopen line 635
  62. theorem OAI.CompletedGauss.large_cube_reopen line 660
  63. theorem OAI.CompletedGauss.completed_cube_inverse_split line 702
  64. theorem OAI.CompletedGauss.large_cube_block_progress line 734