OAI/Combinatorics/ThinTrees/Interlacing.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrongThinTree.MSS.Selection.coeff_prod_negative line 14
  2. lemma OAI.StrongThinTree.MSS.Selection.coeff_pos_of_negative_roots line 44
  3. lemma OAI.StrongThinTree.MSS.Selection.eval_pos_of_nonneg_coeff line 50
  4. lemma OAI.StrongThinTree.MSS.Selection.coeff_pos_of_nonneg line 58
  5. lemma OAI.StrongThinTree.MSS.Selection.positive_coeff_path line 67
  6. lemma OAI.StrongThinTree.MSS.Selection.monic_segment line 104
  7. lemma OAI.StrongThinTree.MSS.Selection.negative_roots_segment line 118
  8. lemma OAI.StrongThinTree.MSS.Selection.roots_shift_iff line 157
  9. lemma OAI.StrongThinTree.MSS.Selection.roots_lt_segment line 162
  10. lemma OAI.StrongThinTree.MSS.Selection.eval_pos_above_roots line 192
  11. lemma OAI.StrongThinTree.MSS.Selection.monic_mean line 202
  12. lemma OAI.StrongThinTree.MSS.Selection.selection_strict line 213
  13. lemma OAI.StrongThinTree.MSS.Selection.selection line 238