OAI/Combinatorics/BalancedRyser/Profiles/ProfileShrinkingExceptions.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.ProfileShrinkingExceptions.integral_le_threshold_mass line 12
2. theorem OAI.Balanced.ProfileShrinkingExceptions.ae_eq_zero_of_shrinking_exceptions line 40
3. theorem OAI.Balanced.ProfileShrinkingExceptions.tendsto_comap_subtype line 56
4. theorem OAI.Balanced.ProfileShrinkingExceptions.ae_eq_const_of_shrinking_exceptions_on_compact line 74
5. theorem OAI.Balanced.ProfileShrinkingExceptions.integral_comap_subtype line 125
6. theorem OAI.Balanced.ProfileShrinkingExceptions.ae_eq_const_of_integral_tendsto_zero_on_compact line 136
7. theorem OAI.Balanced.ProfileShrinkingExceptions.profileSequenceLimit_row_sum_eq_of_integral_tendsto_zero line 173