OAI/Combinatorics/HadwigerCounterexample/MixerConditions.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Mixer Conditions

  1. abbrev OAI.HadwigerCounterexample.MIdx line 15
  2. abbrev OAI.HadwigerCounterexample.MArr line 16
  3. abbrev OAI.HadwigerCounterexample.Draw line 17
  4. def OAI.HadwigerCounterexample.drawn line 20
  5. abbrev OAI.HadwigerCounterexample.MOne line 25
  6. abbrev OAI.HadwigerCounterexample.MBits line 26
  7. def OAI.HadwigerCounterexample.orderedM line 27
  8. def OAI.HadwigerCounterexample.eitherM line 29
  9. def OAI.HadwigerCounterexample.indexedSum line 31
  10. def OAI.HadwigerCounterexample.selfSum line 33
  11. def OAI.HadwigerCounterexample.blockRank line 36
  12. def OAI.HadwigerCounterexample.binaryGood line 39
  13. def OAI.HadwigerCounterexample.qmix line 46

    Source documentation

    Matrix on a point's v coordinates for Tmix(x,atom_l).

    def qmix (m : Mixer p n) (x : Profile p n) (l : Tag p.g) : Moment p n :=
…

    Mentions: OAI.HadwigerCounterexample.Mixer, OAI.HadwigerCounterexample.Profile, OAI.HadwigerCounterexample.Tag, OAI.HadwigerCounterexample.Moment

  14. theorem OAI.HadwigerCounterexample.Tmix_atom line 51
  15. theorem OAI.HadwigerCounterexample.qmix_rank line 95
  16. def OAI.HadwigerCounterexample.unaryGood line 114