OAI/NumberTheory/Ostmann/Tree/PartitionMatching.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.PartitionMatching line 13
2. instance OAI.Ostmann.(instance at line 16) line 16
3. def OAI.Ostmann.PartitionMatching.restrict line 20
4. theorem OAI.Ostmann.PartitionMatching.restrict_injective line 28
5. theorem OAI.Ostmann.card_partitionMatching_le line 39

   Source documentation

   Each label can be matched independently; an upper bound suffices even without constructing the inverse assembly map.

   theorem card_partitionMatching_le {A B C : Type*}
       [Fintype A] [Fintype B] [Fintype C] (f : A → C) (g : B → C)
       (hcard : ∀ c, Fintype.card {a : A // f a = c} =
         Fintype.card {b : B // g b = c}) :
       Fintype.card (PartitionMatching f g) ≤
         ∏ c, (Fintype.card {a : A // f a = c}).factorial := by
   …

   Mentions: OAI.Ostmann.PartitionMatching

6. def OAI.Ostmann.slotFiberEquiv line 55
7. theorem OAI.Ostmann.card_slotFiber line 62
8. theorem OAI.Ostmann.card_slotMatching_le line 71

   Source documentation

   Slots and sampled variables remain labeled, so every arrangement is an actual permutation of all rm positions.

   theorem card_slotMatching_le {L C : Type*} [Fintype L] [Fintype C]
       (f g : L → C) (m : ℕ)
       (hcard : ∀ c, Fintype.card {l : L // f l = c} =
         Fintype.card {l : L // g l = c}) :
       Fintype.card (PartitionMatching (fun x : L × Fin m => f x.1)
         (fun x : L × Fin m => g x.1)) ≤
         ∏ c, (Fintype.card {l : L // f l = c} * m).factorial := by
   …

   Mentions: OAI.Ostmann.PartitionMatching