OAI/Probability/Ballisticity/Estimates/CurvePolicyPMF.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.curvePolicyPMF line 16
  2. lemma OAI.DirectionalTransience.curvePolicyPMF_apply line 22
  3. lemma OAI.DirectionalTransience.curvePolicy_average_probability line 27
  4. def OAI.DirectionalTransience.curvePolicy_average line 37
  5. lemma OAI.DirectionalTransience.curvePolicyPMF_average line 43
  6. def OAI.DirectionalTransience.alignedCurvePolicy line 55
  7. lemma OAI.DirectionalTransience.alignedCurvePolicy_rows line 60
  8. theorem OAI.DirectionalTransience.alignedCurvePolicy_annealed line 69
  9. def OAI.DirectionalTransience.policySafe line 91
  10. lemma OAI.DirectionalTransience.curveIncrement_singleton line 95
  11. lemma OAI.DirectionalTransience.curvePolicyPMF_atom_domination line 106
  12. lemma OAI.DirectionalTransience.curvePolicy_word_density line 117
  13. lemma OAI.DirectionalTransience.curvePolicy_event_density line 137