OAI/Probability/ThorpShuffle/MarginalBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Thorp.Conditional.fairMass_test line 16
2. theorem OAI.Thorp.Conditional.fairMass_tv_le_of_test line 28
3. theorem OAI.Thorp.Conditional.marginal_tv_200 line 48
4. def OAI.Thorp.Conditional.marginalRate line 69
5. theorem OAI.Thorp.Conditional.marginalRate_tendsto line 72
6. theorem OAI.Thorp.Conditional.marginal_tv_rate line 83
7. theorem OAI.Thorp.Conditional.marginal_tendsto line 122