OAI/Combinatorics/EditApproximation/Geometry/LocalInitialCones.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact local evaluation of the initial cones

The local implementation enumerates only the stated dyadic scale interval and the grid square about the query. Zero cones are never searched at a positive seed query. Equality with the global family is proved on a good seed; the local program is finite on every input table.

  1. theorem OAI.EditApproximation.rationalMinimum_le_fallback line 24
  2. theorem OAI.EditApproximation.rationalMinimum_attained line 30
  3. theorem OAI.EditApproximation.localTargetStates_on_grid line 40
  4. theorem OAI.EditApproximation.localInitialConeCenters_subset line 52
  5. theorem OAI.EditApproximation.localInitialConeTable_eq_global line 64