OAI/Probability/SwitchChain/ProjectionTools.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.ProjectionTools.rankOne_plane_bound line 10
2. theorem OAI.Problem315.ProjectionTools.sum_disjoint_nonneg line 22
3. theorem OAI.Problem315.ProjectionTools.slice_numerator_bound line 44
4. theorem OAI.Problem315.ProjectionTools.slice_mu_one_le line 55
5. theorem OAI.Problem315.ProjectionTools.slice_mu_two_le line 73
6. theorem OAI.Problem315.ProjectionTools.disjoint_event_correlation line 85
7. theorem OAI.Problem315.ProjectionTools.inner_error_bound line 102
8. theorem OAI.Problem315.ProjectionTools.interaction_of_orthogonal_decomposition line 110