OAI/Analysis/MarkovType/FiniteSelectionCompression.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.selectionProcess line 17
2. theorem OAI.MarkovSuperreflexivity.selectionProcess_zero line 20
3. theorem OAI.MarkovSuperreflexivity.finiteDifference_selectionProcess_succ line 24
4. theorem OAI.MarkovSuperreflexivity.selectionProcess_eq_sum line 31
5. theorem OAI.MarkovSuperreflexivity.norm_finiteDifference_selectionProcess_le line 59
6. def OAI.MarkovSuperreflexivity.FinitePartitionFiltration.selectionFiltration line 73
7. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.selectionProcess_isMartingaleUpTo line 80
8. theorem OAI.MarkovSuperreflexivity.FinitePartitionFiltration.IsMartingaleUpTo.selectionProcess line 93