OAI/Combinatorics/ThinTrees/Barrier.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrongThinTree.MSS.ray line 16
  2. lemma OAI.StrongThinTree.MSS.ray_eval line 19
  3. lemma OAI.StrongThinTree.MSS.ray_derivative line 31
  4. lemma OAI.StrongThinTree.MSS.ray_map line 46
  5. lemma OAI.StrongThinTree.MSS.eval_map_between line 60
  6. def OAI.StrongThinTree.MSS.RealStable line 68
  7. def OAI.StrongThinTree.MSS.Above line 69
  8. def OAI.StrongThinTree.MSS.barrier line 72
  9. lemma OAI.StrongThinTree.MSS.Above.pos line 76
  10. lemma OAI.StrongThinTree.MSS.Above.add line 81
  11. lemma OAI.StrongThinTree.MSS.Above.update line 86
  12. lemma OAI.StrongThinTree.MSS.ray_zero line 96
  13. lemma OAI.StrongThinTree.MSS.real_ray_upper line 99
  14. lemma OAI.StrongThinTree.MSS.real_ray_splits line 119
  15. lemma OAI.StrongThinTree.MSS.barrier_nonneg line 123
  16. lemma OAI.StrongThinTree.MSS.Stable.log_derivative_im line 143
  17. lemma OAI.StrongThinTree.MSS.ray_log_derivative_im line 160
  18. lemma OAI.StrongThinTree.MSS.barrier_ray_representation line 197
  19. lemma OAI.StrongThinTree.MSS.barrier_update_le line 219
  20. lemma OAI.StrongThinTree.MSS.update_add_single line 231
  21. lemma OAI.StrongThinTree.MSS.barrier_add_le line 238
  22. def OAI.StrongThinTree.MSS.crossBarrier line 255
  23. lemma OAI.StrongThinTree.MSS.hasDerivAt_barrier_ray line 259
  24. lemma OAI.StrongThinTree.MSS.fractions_tangent line 267
  25. lemma OAI.StrongThinTree.MSS.barrier_ray_tangent line 276
  26. lemma OAI.StrongThinTree.MSS.pderiv_commute line 303
  27. lemma OAI.StrongThinTree.MSS.RealStable.sub_pderiv line 320
  28. lemma OAI.StrongThinTree.MSS.eval_sub_pderiv line 326
  29. lemma OAI.StrongThinTree.MSS.barrier_sub_pderiv line 332
  30. lemma OAI.StrongThinTree.MSS.barrier_shift line 345