OAI/Combinatorics/HadwigerCounterexample/MomentLabelSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Moment Label Support

  1. theorem OAI.HadwigerCounterexample.zero_extension line 14

    Source documentation

    Zero extension by the Boolean union rule for low rank matrices.

    theorem zero_extension {M : Moment p n} (hh : hankel M) (hr : M.rank≤k)
    (hk : k≤p.j) (hg : atLayer M hk=0) : M=0 := by
…

    Mentions: OAI.HadwigerCounterexample.Moment, OAI.HadwigerCounterexample.hankel, OAI.HadwigerCounterexample.atLayer

  2. theorem OAI.HadwigerCounterexample.mrk_sum_le line 75
  3. theorem OAI.HadwigerCounterexample.mput_rank_le line 84
  4. def OAI.HadwigerCounterexample.labelSum line 88
  5. theorem OAI.HadwigerCounterexample.label_support line 92