OAI/Combinatorics/EditApproximation/Geometry/LocalSeedSequence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Mathematical values for the actual local seed passes. This complete function is a specification for the lazy program, not a table allocated by the implementation. Copy streams are kept distinct at every pass.

  1. def OAI.EditApproximation.localPassValue line 22
  2. def OAI.EditApproximation.localSeedSequence line 29
  3. theorem OAI.EditApproximation.localSeedSequence_zero line 36
  4. theorem OAI.EditApproximation.localSeedSequence_bounded line 40
  5. def OAI.EditApproximation.localRequestValue line 48
  6. theorem OAI.EditApproximation.localRequestValue_warmup line 57
  7. theorem OAI.EditApproximation.localRequestValue_refinement line 66