OAI/Combinatorics/EditApproximation/Geometry/SeedFactorSchedule.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The literal dyadic factor schedule stops at A<=F. Each active pass replaces A by 4A/F and uses the integer factor a=A/F.

  1. theorem OAI.EditApproximation.dyadicSeedExponent_active line 16
  2. theorem OAI.EditApproximation.dyadicSeedExponent_terminal line 29
  3. theorem OAI.EditApproximation.dyadicSeedPassCount_le line 38
  4. theorem OAI.EditApproximation.dyadicSeedPassCount_le_initial line 45
  5. theorem OAI.EditApproximation.dyadicSeedExponent_succ line 50
  6. theorem OAI.EditApproximation.dyadicSeedFactor_update line 54
  7. theorem OAI.EditApproximation.dyadicSeedFactor_integer line 66
  8. theorem OAI.EditApproximation.dyadicSeedFactor_bound line 80
  9. theorem OAI.EditApproximation.dyadicSeedFactor_terminal line 84
  10. theorem OAI.EditApproximation.dyadicSeedFactor_terminal_refinement line 89
  11. theorem OAI.EditApproximation.computedSeed_initial_factor line 100
  12. theorem OAI.EditApproximation.computedSeedPassCount_le_height line 106