OAI/NumberTheory/Ostmann/Characters/AnchorMatchingCount.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.card_anchor_slot_fiber_le line 13
2. theorem OAI.Ostmann.card_anchor_matching_le line 25

   Source documentation

   Each of the 2^n * m labeled bulk slots has at most 2*m possible counterparts. Injectivity of the matching can only reduce the count.

   theorem card_anchor_matching_le {n m : ℕ} (α : Fin n → ℤ)
       (hα : ∀ j, α j = 1 ∨ α j = -1) :
       Fintype.card (PartitionMatching
         (fun x : (Fin n → Bool) × Fin m => finiteAnchorCode α x.1)
         (fun x : (Fin n → Bool) × Fin m => finiteAnchorCode α x.1)) ≤
         (2 * m) ^ (2 ^ n * m) := by
   …

   Mentions: OAI.Ostmann.PartitionMatching, OAI.Ostmann.finiteAnchorCode