OAI/Combinatorics/BalancedRyser/Profiles/ProfileContinuity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.ProfileContinuity.summable_mul_of_abs_le_one line 11
2. theorem OAI.Balanced.ProfileContinuity.abs_tsum_mul_sub_le_tsum_abs line 19
3. theorem OAI.Balanced.ProfileContinuity.tendsto_tsum_mul_of_probability_mass line 38
4. theorem OAI.Balanced.ProfileContinuity.continuous_tsum_mul_of_probability_mass line 64
5. theorem OAI.Balanced.ProfileContinuity.continuous_profile_bounded_test_sum line 77
6. theorem OAI.Balanced.ProfileContinuity.continuous_profile_power_series line 98
7. theorem OAI.Balanced.ProfileContinuity.continuous_profile_selected_power_series line 113
8. theorem OAI.Balanced.ProfileContinuity.continuous_plane_profile_transform line 135
9. theorem OAI.Balanced.ProfileContinuity.continuous_deletion_profile_transform line 145
10. theorem OAI.Balanced.ProfileContinuity.continuous_cover_profile_transform line 161