OAI/Probability/LatticeSurface/Geometry/CapCoordinates.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExtremalEdges.bulkIndex line 24
  2. def OAI.ExtremalEdges.splitBulk line 42
  3. lemma OAI.ExtremalEdges.preserving_splitBulk line 47
  4. lemma OAI.ExtremalEdges.splitBulk_fst line 52
  5. lemma OAI.ExtremalEdges.splitBulk_snd line 58
  6. lemma OAI.ExtremalEdges.continuous_splitBulk line 64
  7. lemma OAI.ExtremalEdges.splitBulk_restore line 73
  8. def OAI.ExtremalEdges.targetHeight line 86
  9. lemma OAI.ExtremalEdges.continuous_targetHeight line 90
  10. def OAI.ExtremalEdges.gradientShift line 94
  11. lemma OAI.ExtremalEdges.preserving_gradientShift line 106
  12. def OAI.ExtremalEdges.gradientCoords line 113
  13. lemma OAI.ExtremalEdges.preserving_gradientCoords line 118
  14. lemma OAI.ExtremalEdges.continuous_gradientCoords line 123
  15. def OAI.ExtremalEdges.fromGradients line 130
  16. lemma OAI.ExtremalEdges.gradient_restore line 135
  17. lemma OAI.ExtremalEdges.fromGradients_zero line 145
  18. lemma OAI.ExtremalEdges.fromGradients_comb line 151
  19. lemma OAI.ExtremalEdges.fromGradients_neg line 159
  20. lemma OAI.ExtremalEdges.gradientCoords_difference line 165