OAI/GroupTheory/ArtinCAT0/SectorCharts.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArtinCAT0.SixSector.rayLength line 10
  2. def OAI.ArtinCAT0.SixSector.chart line 11
  3. def OAI.ArtinCAT0.SixSector.axis line 13
  4. def OAI.ArtinCAT0.SixSector.circle line 14
  5. lemma OAI.ArtinCAT0.SixSector.chart_zero line 18
  6. lemma OAI.ArtinCAT0.SixSector.chart_axis1 line 20
  7. lemma OAI.ArtinCAT0.SixSector.chart_axis2 line 23
  8. lemma OAI.ArtinCAT0.SixSector.cosine_abs line 26
  9. lemma OAI.ArtinCAT0.SixSector.circle_zero line 30
  10. lemma OAI.ArtinCAT0.SixSector.circle_one line 32
  11. theorem OAI.ArtinCAT0.SixSector.chart_uniform line 36
  12. lemma OAI.ArtinCAT0.SixSector.circle_radius line 57
  13. lemma OAI.ArtinCAT0.SixSector.circle_lipschitz line 66
  14. lemma OAI.ArtinCAT0.SixSector.axis_radius line 81
  15. lemma OAI.ArtinCAT0.SixSector.circle_axis_chord line 85
  16. lemma OAI.ArtinCAT0.SixSector.axis_adjacent line 114
  17. lemma OAI.ArtinCAT0.SixSector.common_cosine line 131
  18. lemma OAI.ArtinCAT0.SixSector.circle_detour line 141
  19. lemma OAI.ArtinCAT0.WordDiagram.eval_surjective line 198
  20. def OAI.ArtinCAT0.WordDiagram.representative line 210
  21. lemma OAI.ArtinCAT0.WordDiagram.eval_representative line 211
  22. abbrev OAI.ArtinCAT0.WordDiagram.SmallSide line 217
  23. def OAI.ArtinCAT0.WordDiagram.smallSide line 218
  24. def OAI.ArtinCAT0.WordDiagram.smallFlip line 219
  25. lemma OAI.ArtinCAT0.WordDiagram.smallSide_flip line 222
  26. abbrev OAI.ArtinCAT0.WordDiagram.SmallLoop line 225
  27. instance OAI.ArtinCAT0.WordDiagram.(instance at line 227) line 227
  28. def OAI.ArtinCAT0.WordDiagram.loopSides line 229
  29. lemma OAI.ArtinCAT0.WordDiagram.loops_closed line 231
  30. lemma OAI.ArtinCAT0.WordDiagram.finite_short_elements line 238
  31. abbrev OAI.ArtinCAT0.WordDiagram.ShortElement line 244
  32. def OAI.ArtinCAT0.WordDiagram.shortElementFintype line 245
  33. lemma OAI.ArtinCAT0.WordDiagram.action_displacement line 250
  34. def OAI.ArtinCAT0.WordDiagram.chooseForward line 257
  35. lemma OAI.ArtinCAT0.WordDiagram.chooseForward_mate line 261
  36. def OAI.ArtinCAT0.WordDiagram.orientedSide line 271
  37. lemma OAI.ArtinCAT0.WordDiagram.orientedSide_mate line 279
  38. lemma OAI.ArtinCAT0.WordDiagram.orientedSide_value line 290
  39. def OAI.ArtinCAT0.WordDiagram.faceLoop line 297
  40. lemma OAI.ArtinCAT0.WordDiagram.faceLoop_start line 307
  41. lemma OAI.ArtinCAT0.WordDiagram.faceLoop_mate line 313
  42. theorem OAI.ArtinCAT0.WordDiagram.controlled_refinement line 331

    Source documentation

    The constants are chosen before the mesh: refinement has uniformly bounded metric displacement and uniformly bounded error in every mirror coordinate.

    theorem controlled_refinement (hG : GeometricAction TriangleGroup X) (y : X)
    (B : ℝ) (hB : 0≤B) :
    ∃ K H : ℕ, ∃ hK : 0<K, letI : NeZero K := ⟨by omega⟩;
…

    Mentions: OAI.ArtinCAT0.TriangleGroup

  43. lemma OAI.ArtinCAT0.SixSector.product_next line 400
  44. def OAI.ArtinCAT0.SixSector.ringCircle line 428
  45. lemma OAI.ArtinCAT0.SixSector.ringCircle_product line 432
  46. lemma OAI.ArtinCAT0.SixSector.angular_parameter line 436
  47. lemma OAI.ArtinCAT0.SixSector.ringCircle_radius line 447
  48. lemma OAI.ArtinCAT0.SixSector.circle_radial line 451
  49. lemma OAI.ArtinCAT0.SixSector.ringCircle_radial line 461
  50. lemma OAI.ArtinCAT0.SixSector.ringCircle_step line 465