OAI/NumberTheory/Ostmann/Tree/ArrangementGraph.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.arrangementGraph line 12
2. instance OAI.Ostmann.(instance at line 21) line 21
3. def OAI.Ostmann.arrangementLeft line 25
4. def OAI.Ostmann.arrangementRight line 29
5. theorem OAI.Ostmann.arrangement_components_match line 33
6. def OAI.Ostmann.arrangementMatching line 40
7. theorem OAI.Ostmann.arrangementLeft_surjective line 46
8. theorem OAI.Ostmann.arrangementRight_surjective line 59
9. theorem OAI.Ostmann.arrangement_component_balance line 67

   Source documentation

   Counting the slots in a component from the two sides gives equal leaf counts, because every leaf has exactly m slots.

   theorem arrangement_component_balance {L : Type*} [Fintype L] {m : ℕ}
       (hm : 0 < m) (e : Equiv.Perm (L × Fin m))
       (c : (arrangementGraph m e).ConnectedComponent) :
       Fintype.card {l : L // arrangementLeft e l = c} =
         Fintype.card {l : L // arrangementRight e l = c} := by
   …

   Mentions: OAI.Ostmann.arrangementGraph, OAI.Ostmann.arrangementLeft, OAI.Ostmann.arrangementRight

10. theorem OAI.Ostmann.arrangement_component_count_le line 76