OAI/Combinatorics/SharpRamsey/Trees/PivotLosses.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.ActualPivot.mask line 17
2. lemma OAI.SharpLogRamsey.ActualPivot.read_mask_first line 22
3. lemma OAI.SharpLogRamsey.ActualPivot.read_mask_second line 30
4. def OAI.SharpLogRamsey.ActualPivot.Input.dualLoss line 40
5. def OAI.SharpLogRamsey.ActualPivot.Input.primalLoss line 45
6. lemma OAI.SharpLogRamsey.ActualPivot.Input.dual_loss_le line 50
7. lemma OAI.SharpLogRamsey.ActualPivot.Input.primal_loss_eq line 66
8. theorem OAI.SharpLogRamsey.ActualPivot.Input.dual_loss_bound line 89
9. theorem OAI.SharpLogRamsey.ActualPivot.Input.primal_loss_bound line 108