OAI/Combinatorics/BalancedRyser/Incidence/AffineProfileExposure.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.AffineProfileExposure.multiplicity_erase_on_target line 22
  2. def OAI.Balanced.AffineProfileExposure.targetExposureMean line 28
  3. def OAI.Balanced.AffineProfileExposure.targetPowerMean line 36
  4. theorem OAI.Balanced.AffineProfileExposure.targetExposureMean_eq line 41
  5. theorem OAI.Balanced.AffineProfileExposure.target_weights_sum line 76
  6. theorem OAI.Balanced.AffineProfileExposure.uniform_target_exposure_approximation line 81
  7. theorem OAI.Balanced.AffineProfileExposure.uniform_target_exposure_approximation_empty_witness line 100
  8. theorem OAI.Balanced.AffineProfileExposure.shifted_target_mean_le line 123
  9. theorem OAI.Balanced.AffineProfileExposure.uniform_profile_pair_target_approximation line 144
  10. theorem OAI.Balanced.AffineProfileExposure.uniform_deletion_target_approximation line 156
  11. theorem OAI.Balanced.AffineProfileExposure.targetPowerMean_eq_profile_transform line 171
  12. theorem OAI.Balanced.AffineProfileExposure.shifted_cover_target_mean_le line 180
  13. theorem OAI.Balanced.AffineProfileExposure.uniform_profile_pair_cover_target_approximation line 202