OAI/Combinatorics/TriangleRemoval/Process/CompleteEdgePair.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpTerminalLeave.completeEdgePair line 15
  2. def OAI.SharpTerminalLeave.centeredEdgeVector line 22
  3. lemma OAI.SharpTerminalLeave.centeredEdgeVector_restrict line 25
  4. lemma OAI.SharpTerminalLeave.graphMatrixLift_apply line 33
  5. lemma OAI.SharpTerminalLeave.graph_centered_normalized_operator line 40
  6. lemma OAI.SharpTerminalLeave.graph_star_residual_sum line 56
  7. lemma OAI.SharpTerminalLeave.centered_edge_operator_drift line 66
  8. lemma OAI.SharpTerminalLeave.history_valid_all line 86
  9. def OAI.SharpTerminalLeave.prefixCenteredEdge line 93
  10. def OAI.SharpTerminalLeave.prefixEdgeRate line 97
  11. def OAI.SharpTerminalLeave.prefixEdgeScalar line 101
  12. def OAI.SharpTerminalLeave.prefixEdgeResidual line 105
  13. def OAI.SharpTerminalLeave.prefixEdgeForcing line 111
  14. lemma OAI.SharpTerminalLeave.prefixEdgeForcing_zero line 119
  15. lemma OAI.SharpTerminalLeave.prefix_centered_edge_recurrence line 124