OAI/Combinatorics/EditApproximation/Binary/BinaryLocalWarmupWork.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The warmup branch constructs its actual local representative/action lists and evaluates their finite Bellman minimum with counted arithmetic.

  1. def OAI.EditApproximation.BinaryFraction.localWarmupWordBudget line 12
  2. def OAI.EditApproximation.BinaryFraction.localWarmupBitBudget line 16
  3. theorem OAI.EditApproximation.BinaryFraction.wideWork_mono line 23
  4. theorem OAI.EditApproximation.BinaryFraction.bellmanWork_mono line 29
  5. theorem OAI.EditApproximation.BinaryFraction.endpointDistance_uniform line 34

    Also declared: OAI/Combinatorics/EditApproximation/Binary/BinaryPhysicalContinuationWork.lean:20 (same declaration text).

  6. theorem OAI.EditApproximation.BinaryFraction.warmupCoefficient_bounds line 44
  7. theorem OAI.EditApproximation.BinaryFraction.warmupBellman_bounds line 54
  8. theorem OAI.EditApproximation.BinaryFraction.warmupWide_bounds line 80
  9. theorem OAI.EditApproximation.BinaryFraction.localWarmupKernelWithWork_bounds line 107