OAI/RepresentationTheory/RestrictedTilting/PlaneCharts.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Two plane sections, transition matrices and associated charts.

  1. def OAI.FiberFunctorProof.planeXSection line 17
  2. def OAI.FiberFunctorProof.planeYSection line 21
  3. def OAI.FiberFunctorProof.planeChartCoordinate line 25
  4. def OAI.FiberFunctorProof.planeChartInverse line 28
  5. lemma OAI.FiberFunctorProof.planeChartEvaluation_coordinate line 32
  6. lemma OAI.FiberFunctorProof.planeChartEvaluation_inverse line 38
  7. def OAI.FiberFunctorProof.planeXPolynomialChart line 47
  8. def OAI.FiberFunctorProof.planeYPolynomialChart line 53
  9. lemma OAI.FiberFunctorProof.planeXPolynomialChart_evaluation line 60
  10. lemma OAI.FiberFunctorProof.planeYPolynomialChart_evaluation line 77
  11. def OAI.FiberFunctorProof.regularXChartValue line 93
  12. lemma OAI.FiberFunctorProof.regularXChartValue_evaluation line 97
  13. def OAI.FiberFunctorProof.regularXChart line 102
  14. def OAI.FiberFunctorProof.regularYChartValue line 132
  15. lemma OAI.FiberFunctorProof.regularYChartValue_evaluation line 136
  16. def OAI.FiberFunctorProof.regularYChart line 141
  17. lemma OAI.FiberFunctorProof.planeSections_transition line 179
  18. lemma OAI.FiberFunctorProof.sl2_xSection_decomposition line 191
  19. def OAI.FiberFunctorProof.associatedXChart line 208
  20. def OAI.FiberFunctorProof.associatedYChart line 214
  21. lemma OAI.FiberFunctorProof.associatedXChart_evaluation line 221
  22. lemma OAI.FiberFunctorProof.associatedYChart_evaluation line 229
  23. lemma OAI.FiberFunctorProof.associatedCharts_transition line 237
  24. lemma OAI.FiberFunctorProof.associatedXChart_injective line 246