OAI/Combinatorics/BalancedRyser/Profiles/ProfileOrderComplements.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.ProfileOrderComplements.future line 19
2. theorem OAI.Balanced.ProfileOrderComplements.current_not_future line 21
3. theorem OAI.Balanced.ProfileOrderComplements.exposed_image_eq line 24
4. theorem OAI.Balanced.ProfileOrderComplements.exposed_image_eq_complement line 47
5. theorem OAI.Balanced.ProfileOrderComplements.future_card_add_one line 52
6. theorem OAI.Balanced.ProfileOrderComplements.targetFraction_eq_filter line 68
7. theorem OAI.Balanced.ProfileOrderComplements.conditional_targetMean_eq_remaining line 81
8. theorem OAI.Balanced.ProfileOrderComplements.uniform_profile_pair_conditional_target_approximation line 101
9. theorem OAI.Balanced.ProfileOrderComplements.uniform_profile_pair_conditional_cover_target_approximation line 121