OAI/Probability/SwitchChain/PairEqualityInactive.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.PairEquality.projection_apply_eq_zero_on_inactive_fiber line 12
2. theorem OAI.Problem315.PairEquality.projection_apply_eq_zero_of_inactive line 21
3. theorem OAI.Problem315.PairEquality.sum_projection_sq_on_inactive_fiber line 28
4. theorem OAI.Problem315.PairEquality.projection_apply_eq_zero_of_centered_zero line 38
5. theorem OAI.Problem315.PairEquality.centered_same_label line 47
6. theorem OAI.Problem315.PairEquality.projection_same_label line 59