OAI/Probability/SwitchChain/SliceBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.SliceBounds.product_ge_sum_sub_one line 9
2. def OAI.Problem315.SliceBounds.equalityProbability line 13
3. theorem OAI.Problem315.SliceBounds.equalityProbability_pos line 16
4. theorem OAI.Problem315.SliceBounds.equalityProbability_complement line 28
5. theorem OAI.Problem315.SliceBounds.linear_numerator_identity line 37
6. theorem OAI.Problem315.SliceBounds.linear_eigenvalue_le line 48
7. theorem OAI.Problem315.SliceBounds.quadratic_eigenvalue_le line 64
8. theorem OAI.Problem315.SliceBounds.disjoint_plane_bound line 78