OAI/Analysis/NodalLength/StoppedTrees.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SharpNodal.Descent.Label line 163
  2. inductive OAI.SharpNodal.Descent.Tree line 168
  3. def OAI.SharpNodal.Descent.Tree.root line 175
  4. def OAI.SharpNodal.Descent.Tree.massCost line 179
  5. def OAI.SharpNodal.Descent.Tree.tiltCost line 183
  6. def OAI.SharpNodal.Descent.Tree.floorCost line 187
  7. def OAI.SharpNodal.Descent.Tree.Valid line 191
  8. lemma OAI.SharpNodal.Descent.Tree.mass_nonneg line 198
  9. lemma OAI.SharpNodal.Descent.Tree.floor_nonneg line 201
  10. lemma OAI.SharpNodal.Descent.Tree.cost_nonneg line 206
  11. theorem OAI.SharpNodal.Descent.Tree.stopped_descent line 215
  12. lemma OAI.SharpNodal.Descent.Tree.stopped_total_cost line 241
  13. lemma OAI.SharpNodal.Descent.Tree.stopped_total_uniform line 247
  14. def OAI.SharpNodal.Descent.Tree.goodProb line 262
  15. lemma OAI.SharpNodal.Descent.Tree.goodProb_bounds line 266
  16. theorem OAI.SharpNodal.Descent.Tree.failure_cost line 277
  17. theorem OAI.SharpNodal.Descent.Tree.stable_probability line 331