OAI/Analysis/MarkovType/FinitePredictableTransform.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.partialSumProcess line 19
  2. theorem OAI.MarkovSuperreflexivity.partialSumProcess_zero line 23
  3. theorem OAI.MarkovSuperreflexivity.difference_partialSumProcess_succ line 27
  4. theorem OAI.MarkovSuperreflexivity.partialSumProcess_isMartingale line 33
  5. theorem OAI.MarkovSuperreflexivity.predictableTransform_isMartingale line 52
  6. def OAI.MarkovSuperreflexivity.cumulativeCost line 67
  7. theorem OAI.MarkovSuperreflexivity.cumulativeCost_zero line 71
  8. theorem OAI.MarkovSuperreflexivity.cumulativeCost_succ line 75
  9. theorem OAI.MarkovSuperreflexivity.cumulativeCost_mono line 79
  10. theorem OAI.MarkovSuperreflexivity.cumulativeCost_predictable line 88
  11. def OAI.MarkovSuperreflexivity.budgetCoefficient line 100
  12. theorem OAI.MarkovSuperreflexivity.budgetCoefficient_predictable line 103
  13. theorem OAI.MarkovSuperreflexivity.budgetTransform_isMartingale line 112
  14. theorem OAI.MarkovSuperreflexivity.budgetCoefficient_eq_one_of_cost_le line 124
  15. theorem OAI.MarkovSuperreflexivity.budgetTransform_eq_of_cost_le line 131
  16. theorem OAI.MarkovSuperreflexivity.retainedCost_eq_of_cost_le line 142
  17. theorem OAI.MarkovSuperreflexivity.retainedCost_le line 153
  18. theorem OAI.MarkovSuperreflexivity.budgetTransform_energy_le line 166