OAI/Combinatorics/SharpRamsey/Execution/OriginalTargetLoss.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLogRamsey.ActualPivot.firstTargetDensity line 20
2. def OAI.SharpLogRamsey.ActualPivot.secondTargetDensity line 24
3. lemma OAI.SharpLogRamsey.ActualPivot.firstTargetDensity_nonneg line 31
4. lemma OAI.SharpLogRamsey.ActualPivot.secondTargetDensity_nonneg line 40
5. lemma OAI.SharpLogRamsey.ActualPivot.firstTargetDensity_eq line 49
6. lemma OAI.SharpLogRamsey.ActualPivot.secondTargetDensity_eq line 60
7. theorem OAI.SharpLogRamsey.ActualPivot.Book.target_loss line 74