OAI/Combinatorics/EditApproximation/Geometry/ActionLower.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Preservation of the two action lower bounds

The action invariant follows from actual edit and shift connection inequalities, rather than an assumed lower-bound-preserving oracle.

  1. theorem OAI.EditApproximation.list_sum_map_le line 16
  2. theorem OAI.EditApproximation.list_sum_map_div line 24
  3. theorem OAI.EditApproximation.actual_action_lower line 30