OAI/Combinatorics/BalancedRyser/Profiles/ProfileWeakCompactness.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.ProfileWeakCompactness.exists_finiteMeasure_subsequence line 10
2. theorem OAI.Balanced.ProfileWeakCompactness.exists_simultaneous_subsequence line 36
3. theorem OAI.Balanced.ProfileWeakCompactness.nonempty_profiles line 56
4. theorem OAI.Balanced.ProfileWeakCompactness.exists_profile_measure_subsequence line 74
5. theorem OAI.Balanced.ProfileWeakCompactness.mass_eq_of_weak_limit line 84
6. theorem OAI.Balanced.ProfileWeakCompactness.tendsto_integral_coordinate line 91
7. theorem OAI.Balanced.ProfileWeakCompactness.exists_full_profile_subsequence line 104