OAI/Combinatorics/EditApproximation/Geometry/AlignedStates.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Actual optimal child states

The alignment split is converted to bounded target endpoint states at the actual balanced source children. Its sum is exactly the parent edit distance; its target endpoints are shared.

  1. theorem OAI.EditApproximation.zipWith_sum_ofFn line 19
  2. theorem OAI.EditApproximation.optimal_balanced_child_states line 30