OAI/Combinatorics/BalancedRyser/Incidence/AffinePlaneOrderExposure.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.AffinePlaneOrderExposure.planeOrderMean line 15
  2. def OAI.Balanced.AffinePlaneOrderExposure.planePowerMean line 24
  3. def OAI.Balanced.AffinePlaneOrderExposure.erasedPlanePowerMean line 28
  4. theorem OAI.Balanced.AffinePlaneOrderExposure.erased_subtype_card line 34
  5. theorem OAI.Balanced.AffinePlaneOrderExposure.planeOrderMean_eq line 54
  6. theorem OAI.Balanced.AffinePlaneOrderExposure.plane_weights_sum line 100
  7. theorem OAI.Balanced.AffinePlaneOrderExposure.multiplicity_erase_le line 109
  8. theorem OAI.Balanced.AffinePlaneOrderExposure.multiplicity_erase_eq_off line 116
  9. theorem OAI.Balanced.AffinePlaneOrderExposure.erasedPlanePowerMean_error line 124
  10. theorem OAI.Balanced.AffinePlaneOrderExposure.planePowerMean_eq_profile_transform line 144
  11. theorem OAI.Balanced.AffinePlaneOrderExposure.plane_mean_le line 152
  12. theorem OAI.Balanced.AffinePlaneOrderExposure.erased_plane_mean_le line 160
  13. theorem OAI.Balanced.AffinePlaneOrderExposure.uniform_plane_order_approximation line 171
  14. theorem OAI.Balanced.AffinePlaneOrderExposure.uniform_plane_order_approximation_empty_witness line 201
  15. theorem OAI.Balanced.AffinePlaneOrderExposure.planePowerMean_swap line 231
  16. theorem OAI.Balanced.AffinePlaneOrderExposure.erased_cover_plane_mean_le line 239
  17. theorem OAI.Balanced.AffinePlaneOrderExposure.exists_reciprocal_cutoff line 253
  18. theorem OAI.Balanced.AffinePlaneOrderExposure.uniform_profile_pair_order_plane_approximation line 259
  19. theorem OAI.Balanced.AffinePlaneOrderExposure.uniform_profile_pair_order_cover_plane_approximation line 281
  20. theorem OAI.Balanced.AffinePlaneOrderExposure.uniform_deletion_order_plane_approximation line 303