OAI/Combinatorics/HadwigerCounterexample/SparseCutProfiles.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.HadwigerCounterexample.Wtag_disabled line 14
2. theorem OAI.HadwigerCounterexample.Wtag_majority_star line 29

   Source documentation

   Intersect W_l over a strict majority. Every O coordinate is forced to zero and projecting onto the shared variables fixes the matrix.

   theorem Wtag_majority_star {I : Finset (Tag p.g)}
       (hI : p.g < 2 * I.card) {m : Moment p n} (h : ∀ l ∈ I, m ∈ Wtag p n l) :
       m ∈ Wstar p n := by
   …

   Mentions: OAI.HadwigerCounterexample.Tag, OAI.HadwigerCounterexample.Moment, OAI.HadwigerCounterexample.Wtag, OAI.HadwigerCounterexample.Wstar

3. def OAI.HadwigerCounterexample.totalRank line 85
4. def OAI.HadwigerCounterexample.nonzeroTags line 86
5. theorem OAI.HadwigerCounterexample.mem_nonzeroTags line 89
6. theorem OAI.HadwigerCounterexample.cut_const line 92
7. theorem OAI.HadwigerCounterexample.common_zero line 98
8. theorem OAI.HadwigerCounterexample.small_cut_unique line 112
9. theorem OAI.HadwigerCounterexample.nz_rank line 121
10. theorem OAI.HadwigerCounterexample.few_unequal line 130
11. theorem OAI.HadwigerCounterexample.sparse_rep line 177

    Source documentation

    Sparse representatives: the bound here is g*(number of supported tags) ≤ 2*total rank (apply with total rank ≤ 2D).

    theorem sparse_rep {x : Profile p n} (h : x ∈ Xspace p n)
        (hg : 4*totalRank x < p.g*p.g) :
        ∃ w : Tag p.g → Moment p n, cut p n w=x ∧
          (∀ l,w l∈Wtag p n l) ∧
          p.g*(nonzeroTags w).card ≤ 2*totalRank x ∧ 2*(nonzeroTags w).card < p.g := by
    …

    Mentions: OAI.HadwigerCounterexample.Profile, OAI.HadwigerCounterexample.Xspace, OAI.HadwigerCounterexample.totalRank, OAI.HadwigerCounterexample.Tag, OAI.HadwigerCounterexample.Moment, OAI.HadwigerCounterexample.cut, OAI.HadwigerCounterexample.Wtag, OAI.HadwigerCounterexample.nonzeroTags