OAI/Probability/SwitchChain/PairEqualityBudgetUnordered.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem315.PairEquality.orderedGain_eq_gain line 15
2. theorem OAI.Problem315.PairEquality.gain_diag_right line 19
3. theorem OAI.Problem315.PairEquality.sum_gain_eq_half_ordered line 23
4. theorem OAI.Problem315.PairEquality.pair_projection_budget line 42
5. theorem OAI.Problem315.PairEquality.sum_gain_norm_sq line 61
6. theorem OAI.Problem315.PairEquality.disjoint_pair_projection_budget line 72