OAI/Probability/SwitchChain/TripleProjectionBridge.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.TripleProjectionBridge.projection_sum_bound line 12
2. theorem OAI.Problem315.TripleProjectionBridge.triple_gap_of_row_variance line 24
3. theorem OAI.Problem315.TripleProjectionBridge.square_bound_of_unit_gap line 38
4. theorem OAI.Problem315.TripleProjectionBridge.triple_square_of_row_variance line 44
5. theorem OAI.Problem315.TripleProjectionBridge.triple_square_of_centered_row_variance line 50