OAI/Combinatorics/EditApproximation/Geometry/ActualActionValues.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Connection values at labeled physical children

Child table values retain their child labels even when two source substrings coincide. The edit and shift lower bounds are proved for the actual finite sum of these labeled values.

  1. def OAI.EditApproximation.endpointActionValue line 23
  2. theorem OAI.EditApproximation.actual_endpoint_action_lower line 27