OAI/Combinatorics/HadwigerCounterexample/BooleanLabels.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HadwigerCounterexample.monoBit line 14
2. theorem OAI.HadwigerCounterexample.mono_insert line 16
3. theorem OAI.HadwigerCounterexample.mono_union line 24
4. theorem OAI.HadwigerCounterexample.selector_indep line 32

   Source documentation

   Independence up to degree j for at most j+1 labels, in coefficient form.

   theorem selector_indep (L : Finset (Label b)) (c : Label b → F) (j : ℕ)
       (h : L.card ≤ j+1) (hf : ∀ S : Finset (Fin b), S.card ≤ j →
         ∑ s ∈ L,c s*monoBit s S=0) : ∀ i∈L,c i=0 := by
   …

   Mentions: OAI.HadwigerCounterexample.Label, OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.monoBit

5. def OAI.HadwigerCounterexample.hankel line 71
6. def OAI.HadwigerCounterexample.diagBase line 75
7. theorem OAI.HadwigerCounterexample.point_eval line 78
8. theorem OAI.HadwigerCounterexample.Wspace_hank line 82
9. theorem OAI.HadwigerCounterexample.Wspace_diag line 96
10. abbrev OAI.HadwigerCounterexample.BaseMat line 111
11. def OAI.HadwigerCounterexample.labMat line 113
12. theorem OAI.HadwigerCounterexample.labMat_act line 117
13. def OAI.HadwigerCounterexample.mput line 122
14. theorem OAI.HadwigerCounterexample.mput_apply line 125
15. theorem OAI.HadwigerCounterexample.mput_hank line 130
16. theorem OAI.HadwigerCounterexample.ray_indep line 136

    Source documentation

    Short label-tagged rays give a direct family of copies of the affine-vector space.

    theorem ray_indep (L : Finset (Label p.b)) (Z : Label p.b → Vec (AIdx p.g n))
        (hj : L.card ≤ p.j+1) (he : ∑ i∈L, putLab p n i (Z i) = 0) :
        ∀ i∈L, Z i=0 := by
    …

    Mentions: OAI.HadwigerCounterexample.Label, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.AIdx, OAI.HadwigerCounterexample.putLab