OAI/Combinatorics/EditApproximation/Refinement/ComputedSeedWords.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.EditApproximation.scheduledSeedWordWithWork_value line 12

   Source documentation

   The actual dyadic incoming approximation factor used by a seed pass.

   theorem scheduledSeedWordWithWork_value (N pass : ℕ) :
       (scheduledSeedWordWithWork N pass).1.value = scheduledSeedFactor N pass := by
   …

   Mentions: OAI.EditApproximation.scheduledSeedWordWithWork, OAI.EditApproximation.scheduledSeedFactor

2. theorem OAI.EditApproximation.scheduledSeedWordWithWork_bounds line 17
3. theorem OAI.EditApproximation.scheduledSeedWordWithWork_range line 33