OAI/Combinatorics/HadwigerCounterexample/FrozenProjections.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HadwigerCounterexample.Volley.frozen line 19

   Source documentation

   D + attack directions.

   def frozen (a : Plan p n) (t : Tagging p I) : Plan p n := a⊔v.keyPlan t

   Mentions: OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.Tagging

2. def OAI.HadwigerCounterexample.Volley.marked line 22

   Source documentation

   All labels at one endpoint.

   def marked (i : Bool) := (v.here i).image v.sel

3. theorem OAI.HadwigerCounterexample.Volley.marked_mem line 24
4. theorem OAI.HadwigerCounterexample.Volley.marked_card line 27
5. def OAI.HadwigerCounterexample.Volley.visitH line 32

   Source documentation

   project matrix of active key rays to one endpoint under attack

   def visitH (t : Tagging p I) (i : Bool) (e : Comp p.g) : Finset (visits p t e) :=
   …

   Mentions: OAI.HadwigerCounterexample.Tagging, OAI.HadwigerCounterexample.Comp, OAI.HadwigerCounterexample.Volley.visits

6. theorem OAI.HadwigerCounterexample.Volley.visitH_here line 35
7. theorem OAI.HadwigerCounterexample.Volley.visitH_card line 39
8. theorem OAI.HadwigerCounterexample.Volley.key_proj line 49
9. theorem OAI.HadwigerCounterexample.Volley.key_here_dim line 64
10. theorem OAI.HadwigerCounterexample.Volley.key_dim line 82
11. theorem OAI.HadwigerCounterexample.Volley.sPin_frozen line 87
12. theorem OAI.HadwigerCounterexample.Volley.hPin_frozen line 91
13. theorem OAI.HadwigerCounterexample.Volley.frozen_here_dim line 102
14. theorem OAI.HadwigerCounterexample.ip_annih line 110
15. theorem OAI.HadwigerCounterexample.orth_pair_sym line 123
16. theorem OAI.HadwigerCounterexample.purePair_sym line 129
17. theorem OAI.HadwigerCounterexample.pure_ip line 134
18. theorem OAI.HadwigerCounterexample.vanish_one line 144
19. theorem OAI.HadwigerCounterexample.orth_ip_frozen line 157

    Source documentation

    For an annihilator cut pair, testing a right or left primal functional on endpoint i annihilating projected pins-and-keys produces an entire vector in the opposite frozen space.

    theorem orth_ip_frozen {f b : Plan p n} {x : Xpair p n} {C : ChanOut p n} {j}
        (h : orth p C f b j x) (i : Bool) (z : Place p) (φ : Ray p n)
        (hh : φ∈annih (sPin f (flipZ p z) i)) :
        IP p n i *ᵥ ((x i).val z.1 *ᵥ φ) ∈ f z := by
    …

    Mentions: OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.Xpair, OAI.HadwigerCounterexample.ChanOut, OAI.HadwigerCounterexample.orth, OAI.HadwigerCounterexample.Place, OAI.HadwigerCounterexample.Ray, OAI.HadwigerCounterexample.annih, OAI.HadwigerCounterexample.sPin, OAI.HadwigerCounterexample.flipZ, OAI.HadwigerCounterexample.IP