OAI/NumberTheory/Ostmann/Construction/SeparatedMatchingCount.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.sumSide line 10
2. def OAI.Ostmann.sumSideLeftEquiv line 12
3. def OAI.Ostmann.sumSideRightEquiv line 21
4. def OAI.Ostmann.separatedMatchingLeft line 30
5. def OAI.Ostmann.separatedMatchingRight line 34
6. theorem OAI.Ostmann.separatedMatching_pair_injective line 38
7. theorem OAI.Ostmann.bad_separated_matching_count line 58

   Source documentation

   Nonbulk slots are still labeled. Their complete permutation cost is a fixed factorial; all growing bulk multiplicity uses the sharp bad count.

   theorem bad_separated_matching_count {r m : ℕ} {N : Type*} [Fintype N] :
       Fintype.card {e : PartitionMatching (@sumSide (Fin r × Fin m) N) (@sumSide (Fin r × Fin m) N) //
         BadBulkArrangement (separatedMatchingLeft e)} ≤
         Fintype.card {e : Equiv.Perm (Fin r × Fin m) // BadBulkArrangement e} *
           (Fintype.card N).factorial := by
   …

   Mentions: OAI.Ostmann.PartitionMatching, OAI.Ostmann.sumSide, OAI.Ostmann.BadBulkArrangement, OAI.Ostmann.separatedMatchingLeft

8. theorem OAI.Ostmann.bad_separated_matching_bound line 79