OAI/Probability/MatroidProphet/Algorithm/SeedLaw.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MatroidProphet.MainSeedBlocks line 11
2. def OAI.MatroidProphet.encodeMainSeed line 13
3. lemma OAI.MatroidProphet.encodeMainSeed_mask line 21
4. lemma OAI.MatroidProphet.encodeMainSeed_branch line 35
5. lemma OAI.MatroidProphet.encodeMainSeed_odd line 39
6. def OAI.MatroidProphet.maskCoinLaw line 44
7. instance OAI.MatroidProphet.maskCoinLaw_probability line 47
8. def OAI.MatroidProphet.mainBlockLaw line 52
9. instance OAI.MatroidProphet.mainBlockLaw_probability line 60
10. def OAI.MatroidProphet.mainSeedLaw line 66
11. instance OAI.MatroidProphet.mainSeedLaw_probability line 70
12. lemma OAI.MatroidProphet.integral_mainSeedLaw line 75
13. lemma OAI.MatroidProphet.mainSeedLaw_expectation line 101