OAI/Combinatorics/BalancedRyser/Profiles/ProfileMarginalLimits.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.ProfileMarginalLimits.abs_tsum_comp_sub_le line 12
2. theorem OAI.Balanced.ProfileMarginalLimits.tendsto_tsum_comp_of_probability_mass line 28
3. theorem OAI.Balanced.ProfileMarginalLimits.finite_totalDegree_sublevel line 41
4. theorem OAI.Balanced.ProfileMarginalLimits.planeProfile_limit_hasSum line 53
5. theorem OAI.Balanced.ProfileMarginalLimits.planeProfile_tendsto_l1 line 77
6. theorem OAI.Balanced.ProfileMarginalLimits.planeProfile_tendsto_marginal line 90
7. theorem OAI.Balanced.ProfileMarginalLimits.planeProfile_core_density_tendsto line 104
8. theorem OAI.Balanced.ProfileMarginalLimits.planeProfile_uncovered_density_tendsto line 113
9. theorem OAI.Balanced.ProfileMarginalLimits.planeProfile_uncovered_lower_bound line 122
10. theorem OAI.Balanced.ProfileMarginalLimits.planeProfile_zero_row_hasSum_of_density line 134