OAI/Combinatorics/HadwigerCounterexample/ConditionalCellEntropy.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.plan_add_disjoint line 14
2. theorem OAI.HadwigerCounterexample.plan_new_disjoint line 23
3. def OAI.HadwigerCounterexample.kslots line 28
4. def OAI.HadwigerCounterexample.kmax line 30
5. theorem OAI.HadwigerCounterexample.slots_budget line 31
6. instance OAI.HadwigerCounterexample.instFKeys line 37
7. theorem OAI.HadwigerCounterexample.dim_keys line 40
8. theorem OAI.HadwigerCounterexample.Volley.key_slots line 63
9. theorem OAI.HadwigerCounterexample.Volley.key_pin line 90

   Source documentation

   chosen reference x fixes the pin made of a and all key directions for every y in the same pin which agrees on query key.

   theorem key_pin (t : Tagging p I) {a : Pin p n N} {x y : UnitType p n N}
       (hx : a.agree x) (hy : a.agree y) (h : v.keys t x=v.keys t y) :
       (Pin.make (v.frozen a.sp t) x).agree y := by
   …

   Mentions: OAI.HadwigerCounterexample.Tagging, OAI.HadwigerCounterexample.Pin, OAI.HadwigerCounterexample.UnitType, OAI.HadwigerCounterexample.Pin.make

10. def OAI.HadwigerCounterexample.tau line 108
11. def OAI.HadwigerCounterexample.hit line 109
12. theorem OAI.HadwigerCounterexample.in_clear line 111