OAI/Combinatorics/EditApproximation/Geometry/SharedActions.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact connection cancellation for shared-endpoint finite actions.

  1. theorem OAI.EditApproximation.connectionBudget_ofFn_zero line 10
  2. theorem OAI.EditApproximation.endpointActionConnection_zero line 31
  3. theorem OAI.EditApproximation.round_shared_action line 49
  4. theorem OAI.EditApproximation.zero_connection_target_eq line 64
  5. theorem OAI.EditApproximation.zero_connection_gap_sum line 73
  6. theorem OAI.EditApproximation.zero_connection_cost_sum_lower line 94