OAI/Geometry/Cannon/Actions/Height.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CannonH3.Height line 16
  2. abbrev OAI.CannonH3.Half line 17
  3. def OAI.CannonH3.coords line 19
  4. def OAI.CannonH3.distArg line 42
  5. lemma OAI.CannonH3.dist_coords line 45
  6. def OAI.CannonH3.lift line 59
  7. def OAI.CannonH3.heightScale line 65
  8. def OAI.CannonH3.complexAffine line 73
  9. def OAI.CannonH3.affine line 81
  10. lemma OAI.CannonH3.affine_preserves line 84
  11. def OAI.CannonH3.affineIsom line 94
  12. def OAI.CannonH3.q line 96
  13. lemma OAI.CannonH3.q_pos line 97
  14. def OAI.CannonH3.inversionFun line 102
  15. lemma OAI.CannonH3.inversion_q line 105
  16. lemma OAI.CannonH3.inversion_involutive line 113
  17. lemma OAI.CannonH3.continuous_q line 124
  18. lemma OAI.CannonH3.continuous_inversion line 128
  19. def OAI.CannonH3.inversion line 134
  20. lemma OAI.CannonH3.inversion_preserves line 144
  21. def OAI.CannonH3.inversionIsom line 173
  22. abbrev OAI.CannonH3.Boundary line 184
  23. def OAI.CannonH3.potential line 186
  24. lemma OAI.CannonH3.potential_infty line 189
  25. lemma OAI.CannonH3.potential_coe line 190
  26. lemma OAI.CannonH3.potential_pos line 193
  27. def OAI.CannonH3.Compatible line 201
  28. def OAI.CannonH3.quadratic line 205
  29. lemma OAI.CannonH3.quadratic_pos line 206
  30. lemma OAI.CannonH3.height_relation line 210
  31. lemma OAI.CannonH3.quadratic_relation line 221
  32. lemma OAI.CannonH3.quadratic_re line 240
  33. lemma OAI.CannonH3.quadratic_im line 247
  34. lemma OAI.CannonH3.product_quadratic_coefficients line 255
  35. def OAI.CannonH3.basepoint line 271
  36. lemma OAI.CannonH3.basepoint_fixed line 273
  37. lemma OAI.CannonH3.compatible_identity_unique line 301
  38. lemma OAI.CannonH3.compatible_one line 336
  39. lemma OAI.CannonH3.compatible_mul line 337
  40. lemma OAI.CannonH3.compatible_inv line 347
  41. def OAI.CannonH3.paired line 353
  42. def OAI.CannonH3.boundaryProjection line 368
  43. lemma OAI.CannonH3.boundaryProjection_injective line 373
  44. def OAI.CannonH3.boundaryGroup line 383
  45. def OAI.CannonH3.pairedH3 line 385
  46. def OAI.CannonH3.extensionHom line 401
  47. lemma OAI.CannonH3.extensionHom_compatible line 404
  48. def OAI.CannonH3.boundaryAffine line 422
  49. lemma OAI.CannonH3.affine_potential line 425
  50. lemma OAI.CannonH3.affine_compatible line 437
  51. lemma OAI.CannonH3.inversion_potential line 446
  52. lemma OAI.CannonH3.inversion_compatible line 492
  53. lemma OAI.CannonH3.affine_mem_boundaryGroup line 504
  54. lemma OAI.CannonH3.inversion_mem_boundaryGroup line 515
  55. lemma OAI.CannonH3.biholomorphic_mem_boundaryGroup line 518
  56. def OAI.CannonH3.reflection line 523
  57. def OAI.CannonH3.boundaryReflection line 525
  58. lemma OAI.CannonH3.reflection_potential line 527
  59. lemma OAI.CannonH3.reflection_compatible line 535
  60. lemma OAI.CannonH3.reflection_distArg line 538
  61. lemma OAI.CannonH3.reflection_mem_boundaryGroup line 542
  62. lemma OAI.CannonH3.boundaryReflection_sq line 545
  63. theorem OAI.CannonH3.conformal_or_anticonformal_mem line 552
  64. def OAI.CannonH3.conformalActionExtension line 561
  65. lemma OAI.CannonH3.conformalActionExtension_compatible line 567
  66. lemma OAI.CannonH3.compatible_unique line 576
  67. def OAI.CannonH3.interior line 582
  68. lemma OAI.CannonH3.interior_compatible line 584
  69. lemma OAI.CannonH3.interior_one line 586
  70. lemma OAI.CannonH3.interior_mul line 587
  71. lemma OAI.CannonH3.interior_affine line 589
  72. lemma OAI.CannonH3.interior_inversion line 601
  73. lemma OAI.CannonH3.interior_reflection line 603