OAI/Combinatorics/BalancedRyser/Profiles/ProfileEmpirical.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.hasSum_card_fibers line 13
  2. theorem OAI.Balanced.hasSum_normalized_card_fibers line 30
  3. theorem OAI.Balanced.hasSum_weighted_card_fibers line 36
  4. theorem OAI.Balanced.planeProfile_nonneg line 68
  5. theorem OAI.Balanced.planeProfile_hasSum line 73
  6. theorem OAI.Balanced.lineProfile_nonneg line 84
  7. theorem OAI.Balanced.lineProfile_hasSum_of_card line 89
  8. theorem OAI.Balanced.lineProfile_hasSum line 103
  9. theorem OAI.Balanced.planeProfile_weighted_hasSum line 107
  10. theorem OAI.Balanced.lineProfile_weighted_hasSum line 120
  11. theorem OAI.Balanced.sum_lineMultiplicity line 136
  12. theorem OAI.Balanced.sum_univ_lineMultiplicity line 143
  13. theorem OAI.Balanced.planeProfile_firstMoment_hasSum line 149
  14. theorem OAI.Balanced.profile_deletionSet_card line 161
  15. theorem OAI.Balanced.planeProfile_isBounded line 173
  16. theorem OAI.Balanced.sum_on_line_lineMultiplicity_le line 191
  17. theorem OAI.Balanced.lineProfile_isBounded line 217