OAI/NumberTheory/DirichletL/Eisenstein/HyperbolicVolume.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.linear_preserves_hyperbolicVolume line 77
  2. lemma OAI.CubicEisenstein.translation_preserves_hyperbolicVolume line 104
  3. def OAI.CubicEisenstein.euclideanMatrixOperator line 121
  4. lemma OAI.CubicEisenstein.euclideanMatrixOperator_apply line 124
  5. lemma OAI.CubicEisenstein.euclideanMatrixOperator_det line 127
  6. def OAI.CubicEisenstein.euclideanWeylReflection line 132
  7. lemma OAI.CubicEisenstein.euclideanWeylReflection_apply line 135
  8. lemma OAI.CubicEisenstein.euclideanWeylReflection_preserves_hyperbolicVolume line 140
  9. def OAI.CubicEisenstein.euclideanComplexDilation line 147
  10. lemma OAI.CubicEisenstein.euclideanComplexDilation_apply line 150
  11. lemma OAI.CubicEisenstein.euclideanComplexDilation_det line 156
  12. lemma OAI.CubicEisenstein.euclideanComplexDilation_preserves_hyperbolicVolume line 168
  13. instance OAI.CubicEisenstein.hyperbolicMeasurableSpace line 181
  14. instance OAI.CubicEisenstein.hyperbolicBorelSpace line 182
  15. lemma OAI.CubicEisenstein.continuous_hyperbolic_action line 184
  16. def OAI.CubicEisenstein.positiveCoordinateHeight line 189
  17. lemma OAI.CubicEisenstein.positiveCoordinateHeight_pos line 190
  18. def OAI.CubicEisenstein.euclideanToUpperCoordinates line 196
  19. def OAI.CubicEisenstein.euclideanToHyperbolic line 199
  20. lemma OAI.CubicEisenstein.euclideanToUpperCoordinates_measurable line 203
  21. lemma OAI.CubicEisenstein.euclideanToHyperbolic_measurable line 210
  22. lemma OAI.CubicEisenstein.euclideanToHyperbolic_positive line 213
  23. def OAI.CubicEisenstein.hyperbolicVolume line 218
  24. lemma OAI.CubicEisenstein.hyperbolicEuclideanVolume_ae_positive line 221
  25. lemma OAI.CubicEisenstein.hyperbolicVolume_map_of_coordinate_action line 226
  26. lemma OAI.CubicEisenstein.matrix_point_coordinates line 240
  27. def OAI.CubicEisenstein.matrixCross line 258
  28. lemma OAI.CubicEisenstein.matrixHorizontal_eq_cross_height line 260
  29. lemma OAI.CubicEisenstein.matrixCross_upperSection line 266
  30. lemma OAI.CubicEisenstein.mobius_denominator_pos line 282
  31. lemma OAI.CubicEisenstein.upperPoint_congr line 286
  32. theorem OAI.CubicEisenstein.mobius_upperPoint line 292
  33. def OAI.CubicEisenstein.complexTranslation line 309
  34. def OAI.CubicEisenstein.complexDiagonal line 310
  35. def OAI.CubicEisenstein.complexWeyl line 312
  36. lemma OAI.CubicEisenstein.complexTranslation_action line 314
  37. lemma OAI.CubicEisenstein.complexWeyl_action line 328
  38. lemma OAI.CubicEisenstein.complexDiagonal_action line 337
  39. lemma OAI.CubicEisenstein.complex_bruhat_nonzero line 359
  40. lemma OAI.CubicEisenstein.complex_bruhat_zero line 374
  41. def OAI.CubicEisenstein.euclideanHorizontalTranslation line 388
  42. lemma OAI.CubicEisenstein.complexTranslation_preserves_hyperbolicVolume line 390
  43. lemma OAI.CubicEisenstein.complexDiagonal_preserves_hyperbolicVolume line 402
  44. lemma OAI.CubicEisenstein.euclidean_complex_norm_sq line 416
  45. def OAI.CubicEisenstein.euclideanWeylAction line 421
  46. lemma OAI.CubicEisenstein.euclideanWeylAction_measurable line 424
  47. lemma OAI.CubicEisenstein.euclideanWeylAction_preserves_hyperbolicVolume line 427
  48. lemma OAI.CubicEisenstein.euclideanWeylAction_apply line 433
  49. lemma OAI.CubicEisenstein.complexWeyl_preserves_hyperbolicVolume line 440
  50. lemma OAI.CubicEisenstein.hyperbolicVolume_invariant_mul line 461
  51. theorem OAI.CubicEisenstein.hyperbolicVolume_invariant line 470
  52. def OAI.SecondPassArithmetic.globalBinTripleRange line 493
  53. def OAI.SecondPassArithmetic.globalBinFirstCoefficient line 496
  54. def OAI.SecondPassArithmetic.globalBinChildCharge line 499
  55. theorem OAI.SecondPassArithmetic.globalBinTripleRange_nonneg line 502
  56. theorem OAI.SecondPassArithmetic.globalBin_complete_cost line 510
  57. theorem OAI.SecondPassArithmetic.globalBin_mass_balance line 525
  58. theorem OAI.SecondPassArithmetic.globalBin_active_bounds line 540
  59. theorem OAI.SecondPassArithmetic.globalBin_first_coefficient_bound line 561
  60. theorem OAI.SecondPassArithmetic.globalBin_triple_bounds line 577
  61. theorem OAI.SecondPassArithmetic.globalBin_triple_count line 593