OAI/Combinatorics/Chromatic/Shuffle/VariableMean.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ElementaryPositivity.RawShuffle.variableSum line 13
  2. lemma OAI.ElementaryPositivity.RawShuffle.derivativeS_variableSum line 21
  3. lemma OAI.ElementaryPositivity.RawShuffle.variables_nonempty_of_ne_zero line 31
  4. def OAI.ElementaryPositivity.RawShuffle.meanS line 39
  5. lemma OAI.ElementaryPositivity.RawShuffle.derivativeS_meanS line 43
  6. def OAI.ElementaryPositivity.RawShuffle.meanB line 51
  7. lemma OAI.ElementaryPositivity.RawShuffle.derivativeB_meanB line 54
  8. def OAI.ElementaryPositivity.RawShuffle.meanMultiplyB line 58
  9. lemma OAI.ElementaryPositivity.RawShuffle.derivativeB_meanMultiply_weyl line 61
  10. lemma OAI.ElementaryPositivity.RawShuffle.meanMultiplyB_filtered line 68
  11. def OAI.ElementaryPositivity.RawShuffle.gradeMeanMultiply line 76
  12. lemma OAI.ElementaryPositivity.RawShuffle.gradeDerivative_meanMultiply_weyl line 85
  13. def OAI.ElementaryPositivity.RawShuffle.SplitTree.IsProper line 103
  14. def OAI.ElementaryPositivity.RawShuffle.properSourceFiltration line 108
  15. lemma OAI.ElementaryPositivity.RawShuffle.sourceFiltration_le_proper line 119
  16. lemma OAI.ElementaryPositivity.RawShuffle.properSourceFiltration_translation_mem line 125
  17. lemma OAI.ElementaryPositivity.RawShuffle.properSourceFiltration_mul_mem line 147
  18. lemma OAI.ElementaryPositivity.RawShuffle.proper_next_iff_leading_zero line 163