OAI/Probability/Ballisticity/Estimates/CurvePolicy.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.curveIncrement line 15
  2. instance OAI.DirectionalTransience.curveIncrement_finite line 19
  3. lemma OAI.DirectionalTransience.curveIncrement_total line 24
  4. lemma OAI.DirectionalTransience.curveIncrement_le_crossing line 30
  5. lemma OAI.DirectionalTransience.curveIncrement_rows line 39
  6. def OAI.DirectionalTransience.curvePolicy line 44
  7. lemma OAI.DirectionalTransience.curvePolicy_probability line 51
  8. lemma OAI.DirectionalTransience.curvePolicy_rows line 64
  9. lemma OAI.DirectionalTransience.curvePolicy_domination line 76
  10. lemma OAI.DirectionalTransience.curveIncrement_translation line 100
  11. lemma OAI.DirectionalTransience.crossingQuenched_translation line 108
  12. lemma OAI.DirectionalTransience.curvePolicy_translation line 116
  13. lemma OAI.DirectionalTransience.curvePolicy_annealed_translation line 124