OAI/Analysis/MarkovType/FinitePredictableSelection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.finiteSelectedValue line 19
  2. theorem OAI.MarkovSuperreflexivity.finiteSelectedValue_eq_sum line 23
  3. theorem OAI.MarkovSuperreflexivity.HasZeroConditionalSum.vexpect_eq_zero line 48
  4. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.finiteSelectedValue_zero_conditionalSum line 63
  5. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.finiteSelectedValue_adapted_stopped line 114
  6. def OAI.MarkovSuperreflexivity.FinitePartitionFiltration.selectedFiltration line 128
  7. def OAI.MarkovSuperreflexivity.finiteSelectedProcess line 138
  8. theorem OAI.MarkovSuperreflexivity.finiteSelectedProcess_zero line 143
  9. theorem OAI.MarkovSuperreflexivity.finiteDifference_selectedProcess_succ line 147
  10. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.finiteSelectedProcess_adapted line 157
  11. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.finiteSelectedProcess_isMartingaleUpTo line 172