OAI/Combinatorics/BalancedRyser/Profiles/ProfileScheduledApproximation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.ProfileScheduledApproximation.planeFraction_eq_filter line 20
  2. theorem OAI.Balanced.ProfileScheduledApproximation.conditional_planeMean_eq_remaining line 33
  3. theorem OAI.Balanced.ProfileScheduledApproximation.remaining_D_counts line 53
  4. theorem OAI.Balanced.ProfileScheduledApproximation.remaining_C_counts line 64
  5. theorem OAI.Balanced.ProfileScheduledApproximation.uniform_scheduled_D_means line 74
  6. theorem OAI.Balanced.ProfileScheduledApproximation.uniform_scheduled_C_means line 102
  7. theorem OAI.Balanced.ProfileScheduledApproximation.future_ID_fraction_exact line 133
  8. theorem OAI.Balanced.ProfileScheduledApproximation.uniform_scheduled_empty_means line 139