OAI/Analysis/MarkovType/ReversibleMartingales.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.chainAverage line 22
  2. def OAI.MarkovSuperreflexivity.chainDrift line 25
  3. theorem OAI.MarkovSuperreflexivity.chainDrift_eq_sum line 28
  4. theorem OAI.MarkovSuperreflexivity.chainAverage_centered_sum line 33
  5. def OAI.MarkovSuperreflexivity.sampledEvenIndex line 40
  6. def OAI.MarkovSuperreflexivity.sampledOddIndex line 43
  7. def OAI.MarkovSuperreflexivity.sampledDifference line 46
  8. def OAI.MarkovSuperreflexivity.sampledForward line 50
  9. def OAI.MarkovSuperreflexivity.sampledBackward line 54
  10. def OAI.MarkovSuperreflexivity.sampledKey line 58
  11. theorem OAI.MarkovSuperreflexivity.sampledForward_zero line 62
  12. theorem OAI.MarkovSuperreflexivity.sampledForward_step line 67
  13. theorem OAI.MarkovSuperreflexivity.sampledForward_end line 90
  14. theorem OAI.MarkovSuperreflexivity.sampledForward_fiber_constant line 97
  15. theorem OAI.MarkovSuperreflexivity.sum_fin_successive_sub line 118
  16. theorem OAI.MarkovSuperreflexivity.sampledDifference_reverse line 131
  17. theorem OAI.MarkovSuperreflexivity.even_displacement_decomposition line 146
  18. theorem OAI.MarkovSuperreflexivity.sum_fiber_comp_zero line 167
  19. theorem OAI.MarkovSuperreflexivity.sampledDifference_fine_cancel line 197
  20. theorem OAI.MarkovSuperreflexivity.sampledForward_fiber_cancel line 224
  21. theorem OAI.MarkovSuperreflexivity.sampledBackward_fiber_constant line 237
  22. theorem OAI.MarkovSuperreflexivity.sampledBackward_fiber_cancel line 243
  23. theorem OAI.MarkovSuperreflexivity.sum_weighted_two line 256
  24. theorem OAI.MarkovSuperreflexivity.chainDrift_q_moment_le line 269
  25. theorem OAI.MarkovSuperreflexivity.centered_edge_q_moment_le_four line 283
  26. theorem OAI.MarkovSuperreflexivity.sampledDifference_q_moment_le_four line 322
  27. theorem OAI.MarkovSuperreflexivity.sampledForward_q_moment_le line 346
  28. theorem OAI.MarkovSuperreflexivity.sampledBackward_q_moment_le line 373
  29. theorem OAI.MarkovSuperreflexivity.even_stateCost_le line 390
  30. theorem OAI.MarkovSuperreflexivity.stateCost_succ_le_two line 417