OAI/NumberTheory/DirichletL/Eisenstein/QuotientTopology.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CubicEisenstein.complexSLTopology line 81
  2. lemma OAI.CubicEisenstein.continuous_complexSL_coe line 84
  3. lemma OAI.CubicEisenstein.continuous_complexSL_mul line 88
  4. lemma OAI.CubicEisenstein.continuous_coordinateSection line 95
  5. lemma OAI.CubicEisenstein.continuous_hyperbolicProjection line 112
  6. lemma OAI.CubicEisenstein.continuous_upperCoordinates line 116
  7. lemma OAI.CubicEisenstein.continuous_translatedUpperCoordinates line 120
  8. def OAI.CubicEisenstein.integralOrbitRel line 125
  9. abbrev OAI.CubicEisenstein.IntegralOrbitQuotient line 138
  10. def OAI.CubicEisenstein.integralOrbitProjection line 140
  11. lemma OAI.CubicEisenstein.continuous_integralOrbitProjection line 143
  12. lemma OAI.CubicEisenstein.integralOrbitProjection_eq line 146
  13. def OAI.CubicEisenstein.truncatedFordLift line 157
  14. lemma OAI.CubicEisenstein.continuous_truncatedFordLift line 160
  15. def OAI.CubicEisenstein.fordOrbitChart line 163
  16. lemma OAI.CubicEisenstein.continuous_fordOrbitChart line 167
  17. def OAI.CubicEisenstein.compactFordCore line 172
  18. lemma OAI.CubicEisenstein.compactFordCore_isCompact line 176
  19. def OAI.CubicEisenstein.fordCuspTail line 184
  20. theorem OAI.CubicEisenstein.finiteIndex_compact_core_cusp_cover line 189
  21. theorem OAI.CubicEisenstein.levelThree_compact_core_cusp_cover line 215
  22. theorem OAI.CubicEisenstein.globalKubotaKernel_compact_core_cusp_cover line 222
  23. def OAI.SecondPassArithmetic.globalSecondRecover line 252
  24. theorem OAI.SecondPassArithmetic.globalSecondRecover_apply line 255
  25. def OAI.SecondPassArithmetic.globalSecondSource line 266
  26. theorem OAI.SecondPassArithmetic.globalSecondSource_eq_tupleSource line 273
  27. theorem OAI.SecondPassArithmetic.globalSecondSource_uniform_transfer line 293
  28. def OAI.SecondPassArithmetic.globalSecondRawPool line 364
  29. def OAI.SecondPassArithmetic.globalSecondRawMask line 367
  30. def OAI.SecondPassArithmetic.globalSecondRawSource line 372
  31. theorem OAI.SecondPassArithmetic.globalSecondRawSource_eq line 380
  32. theorem OAI.SecondPassArithmetic.globalSecondRawSource_uniform_transfer line 406
  33. def OAI.SecondPassArithmetic.CubeCoordinates.sideDivisor line 440
  34. def OAI.SecondPassArithmetic.globalCubeJNorm line 447
  35. def OAI.SecondPassArithmetic.globalCubeActiveRoot line 451
  36. def OAI.SecondPassArithmetic.globalFirstColumnScale line 455
  37. def OAI.SecondPassArithmetic.globalFirstRowScale line 458
  38. def OAI.SecondPassArithmetic.globalSecondDelta line 462
  39. def OAI.SecondPassArithmetic.globalNominalChildRow line 466
  40. theorem OAI.SecondPassArithmetic.globalCubeJNorm_pos line 471
  41. theorem OAI.SecondPassArithmetic.globalCubeActiveRoot_pos line 476
  42. theorem OAI.SecondPassArithmetic.globalFirstColumnScale_pos line 486
  43. theorem OAI.SecondPassArithmetic.globalSecondDelta_ge line 492
  44. theorem OAI.SecondPassArithmetic.globalSecondDelta_pos line 504
  45. theorem OAI.SecondPassArithmetic.globalBaseLabel_norm line 512
  46. theorem OAI.SecondPassArithmetic.globalSecond_radial_ratio line 520
  47. theorem OAI.SecondPassArithmetic.globalSecond_child_mass line 538
  48. theorem OAI.SecondPassArithmetic.globalSecond_complete_cost line 556
  49. theorem OAI.SecondPassArithmetic.globalNominalChildRow_pos line 576
  50. theorem OAI.SecondPassArithmetic.globalNominalChildRow_bound line 584
  51. def OAI.SecondPassArithmetic.globalChildMass line 608
  52. theorem OAI.SecondPassArithmetic.globalChildMass_bound line 616
  53. theorem OAI.SecondPassArithmetic.globalChildRow_bound line 633
  54. theorem OAI.SecondPassArithmetic.globalSecondMask_bound line 650
  55. theorem OAI.SecondPassArithmetic.globalSecond_halving line 682
  56. theorem OAI.SecondPassArithmetic.ceil_strict_of_half line 704
  57. theorem OAI.SecondPassArithmetic.globalSecond_rank_decreases line 715