OAI/Probability/SwitchChain/CrossCellAffineComposition.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.CrossCellMoments.count_pos_of_state line 14
2. theorem OAI.Problem315.CrossCellMoments.conditionalRight_constant_of_ne_two line 22
3. theorem OAI.Problem315.CrossCellMoments.conditionalLeft_constant_of_ne_two line 39
4. theorem OAI.Problem315.CrossCellMoments.expectation_first_second_affine line 64
5. theorem OAI.Problem315.CrossCellMoments.expectation_second_first_affine line 88