OAI/Probability/SwitchChain/DisjointStateExpectation.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Problem315.DisjointMarginal.CellSpace line 13
2. def OAI.Problem315.DisjointMarginal.restrictToStateCell line 16
3. theorem OAI.Problem315.DisjointMarginal.restrictToStateCell_apply line 20
4. def OAI.Problem315.DisjointMarginal.stateCellFiberEquiv line 25
5. theorem OAI.Problem315.DisjointMarginal.expectation_restrictToStateCell line 44
6. theorem OAI.Problem315.DisjointMarginal.left_expectation_restrictToStateCell line 77
7. theorem OAI.Problem315.DisjointMarginal.right_expectation_restrictToStateCell line 84
8. theorem OAI.Problem315.DisjointMarginal.left_deviation_restrictToStateCell line 91
9. theorem OAI.Problem315.DisjointMarginal.right_deviation_restrictToStateCell line 99