OAI/Combinatorics/BalancedRyser/Profiles/ProfileCompactness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.tendsto_tsum_abs_sub_of_probability_mass line 15
2. theorem OAI.Balanced.tendsto_totalVariation_of_probability_mass line 56
3. theorem OAI.Balanced.profile_tail_le_of_moment line 65
4. theorem OAI.Balanced.hasSum_one_of_tendsto_of_tight line 87
5. theorem OAI.Balanced.profile_tight_of_moment line 114
6. theorem OAI.Balanced.profile_moment_le_of_tendsto line 141
7. theorem OAI.Balanced.tendsto_selected_mass_of_probability_mass line 162