OAI/Combinatorics/ThinTrees/RootBound.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrongThinTree.MSS.pencil line 15
  2. lemma OAI.StrongThinTree.MSS.pencil_eval line 19
  3. lemma OAI.StrongThinTree.MSS.pencil_map line 30
  4. lemma OAI.StrongThinTree.MSS.posSemidef_complex line 42
  5. lemma OAI.StrongThinTree.MSS.real_pencil_stable line 57
  6. lemma OAI.StrongThinTree.MSS.pencil_above line 72
  7. lemma OAI.StrongThinTree.MSS.sum_update_smul line 83
  8. lemma OAI.StrongThinTree.MSS.ray_pencil_constant line 99
  9. lemma OAI.StrongThinTree.MSS.ray_pencil_factor line 110
  10. lemma OAI.StrongThinTree.MSS.pencil_barrier line 122
  11. def OAI.StrongThinTree.MSS.realDifferentialProduct line 135
  12. def OAI.StrongThinTree.MSS.shiftVector line 138
  13. lemma OAI.StrongThinTree.MSS.shiftVector_cons line 142
  14. lemma OAI.StrongThinTree.MSS.many_barrier_shifts line 146
  15. lemma OAI.StrongThinTree.MSS.shiftVector_univ line 158
  16. lemma OAI.StrongThinTree.MSS.skew_root_bound line 162