OAI/Probability/SwitchChain/DisjointGraphAffine.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem315.DisjointMarginal.crossCellRestriction line 14
2. theorem OAI.Problem315.DisjointMarginal.crossCellRestriction_apply_equiv line 18
3. theorem OAI.Problem315.DisjointMarginal.left_expectation_eq_crossCell line 24
4. theorem OAI.Problem315.DisjointMarginal.right_expectation_eq_crossCell line 37
5. theorem OAI.Problem315.DisjointMarginal.crossCellRestriction_left_expectation line 50
6. theorem OAI.Problem315.DisjointMarginal.crossCellRestriction_right_expectation line 59
7. theorem OAI.Problem315.DisjointMarginal.right_left_expectation_cell_affine line 68
8. theorem OAI.Problem315.DisjointMarginal.left_right_expectation_cell_affine line 91