OAI/NumberTheory/Ostmann/Construction/ScheduledTemplateBounds.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.copyScheduleVertex_card line 11
2. theorem OAI.Ostmann.copyScheduleAtoms_zero_card line 22
3. theorem OAI.Ostmann.copyScheduleH_card_le line 28
4. def OAI.Ostmann.scheduledTemplateWordBound line 33
5. theorem OAI.Ostmann.scheduledTemplateWordBound_pos line 36
6. theorem OAI.Ostmann.scheduledWordTemplate_size line 43

   Source documentation

   For fixed depth the word-size parameter is linear in the original number of atoms. All formula bounds therefore stay polynomial in that number.

   theorem scheduledWordTemplate_size {I σ : Type*} [Fintype I]
       (role : I → CopyScheduleRole) (address : ℕ → List Bool → σ)
       (childBound pivotBound : ℕ → ℕ) (n : ℕ)
       (path : List Bool) (current : CopyScheduleAtoms role n → σ) :
       (scheduledWordTemplate role address childBound pivotBound n path current).WordsBounded
         (scheduledTemplateWordBound I n) := by
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.CopyScheduleAtoms, OAI.Ostmann.scheduledWordTemplate, OAI.Ostmann.scheduledTemplateWordBound