OAI/Combinatorics/BalancedRyser/Probability/ExposureMeshLimits.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.ExposureInterleaving.uniform_remainingD_fraction_error line 11
2. theorem OAI.Balanced.ExposureInterleaving.uniform_remainingC_fraction_error line 21
3. theorem OAI.Balanced.ExposureInterleaving.remainingD_fraction_sub_tendsto_zero line 31
4. theorem OAI.Balanced.ExposureInterleaving.remainingC_fraction_sub_tendsto_zero line 42
5. theorem OAI.Balanced.ExposureInterleaving.remainingD_fraction_tendsto line 53
6. theorem OAI.Balanced.ExposureInterleaving.remainingC_fraction_tendsto line 61