OAI/Probability/SwitchChain/DisjointAlgebra.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.disjoint_plane_bound line 7
2. theorem OAI.Problem315.sum_rows_le line 18
3. theorem OAI.Problem315.ordered_interactions_nonnegative line 23
4. theorem OAI.Problem315.disjoint_interaction_of_orthogonal_parts line 42
5. theorem OAI.Problem315.disjoint_inner_sum_nonnegative line 58