OAI/Probability/ThorpCompatibility/ClumpCost.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ThorpCompatibility.cellRows line 10
2. def OAI.ThorpCompatibility.clumpCount line 14
3. lemma OAI.ThorpCompatibility.protected_mass_le line 18
4. lemma OAI.ThorpCompatibility.light_restrict_mass_le line 35
5. def OAI.ThorpCompatibility.entryClumpSize line 45
6. def OAI.ThorpCompatibility.exposureError line 48
7. lemma OAI.ThorpCompatibility.exposureError_nonneg line 52
8. lemma OAI.ThorpCompatibility.average_columnCost_good line 58