OAI/NumberTheory/Ostmann/Construction/ScheduledBulkMatchingCount.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.scheduledPathEnumeration line 11
2. abbrev OAI.Ostmann.ScheduledNonbulkH line 14
3. def OAI.Ostmann.scheduledBulkCoordinates line 17
4. def OAI.Ostmann.scheduledSplitHCoordinates line 23
5. def OAI.Ostmann.scheduledBulkLabel line 29
6. theorem OAI.Ostmann.scheduledBulkLabel_coordinates line 33
7. def OAI.Ostmann.scheduledSeparatedMatching line 45
8. theorem OAI.Ostmann.scheduledSeparatedMatching_injective line 61
9. def OAI.Ostmann.BadScheduledMatching line 73

   Source documentation

   This predicate uses the actual leaf coordinates of each bulk prime.

   def BadScheduledMatching {I : Type*} (role : I → CopyScheduleRole)
       (n m : ℕ) (word : Fin m ≃ {i : I // role i = .word})
       (e : PartitionMatching (scheduledBulkLabel role n) (scheduledBulkLabel role n)) : Prop :=
   …

   Mentions: OAI.Ostmann.CopyScheduleRole, OAI.Ostmann.PartitionMatching, OAI.Ostmann.scheduledBulkLabel

10. theorem OAI.Ostmann.bad_scheduled_matching_bound line 78
11. def OAI.Ostmann.scheduledBadMatchingSet line 97
12. theorem OAI.Ostmann.scheduledBadMatchingSet_card_bound line 103