OAI/Combinatorics/BalancedRyser/Incidence/AffinePermutationExposure.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.AffinePermutationExposure.subtype_filter_card line 14
  2. theorem OAI.Balanced.AffinePermutationExposure.erased_subtype_incidence_card line 32
  3. def OAI.Balanced.AffinePermutationExposure.targetOrderMean line 49
  4. theorem OAI.Balanced.AffinePermutationExposure.remaining_count_le line 60
  5. theorem OAI.Balanced.AffinePermutationExposure.targetOrderMean_eq_targetExposureMean line 71
  6. theorem OAI.Balanced.AffinePermutationExposure.uniform_profile_pair_order_target_approximation line 118
  7. theorem OAI.Balanced.AffinePermutationExposure.uniform_deletion_order_target_approximation line 139
  8. theorem OAI.Balanced.AffinePermutationExposure.coverTargetPowerMean_eq_profile_transform line 154
  9. theorem OAI.Balanced.AffinePermutationExposure.uniform_profile_pair_order_cover_target_approximation line 173