OAI/Analysis/MarkovType/FailureJTriangular.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.finiteArrayRealize line 23
2. theorem OAI.MarkovSuperreflexivity.finiteArrayRealize_apply line 29
3. theorem OAI.MarkovSuperreflexivity.finiteArrayRealize_single line 32
4. theorem OAI.MarkovSuperreflexivity.ApproximateTailSystem.realization_pairing_error line 41
5. theorem OAI.MarkovSuperreflexivity.ApproximateTailSystem.finiteTail_le_realization_add_error line 63
6. def OAI.MarkovSuperreflexivity.ApproximateTailSystem.exactHalf line 84
7. theorem OAI.MarkovSuperreflexivity.exact_triangular_system_of_not_jConvex line 143
8. theorem OAI.MarkovSuperreflexivity.not_finiteTriangularObstruction_of_not_jConvex line 160
9. theorem OAI.MarkovSuperreflexivity.FiniteTriangularObstruction.ambientJConvex line 166