OAI/Probability/SignedSweeps/SubsetLaw.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SignedSweeps.upperInclusionMap line 13
  2. lemma OAI.SignedSweeps.upperInclusion_permutation line 30
  3. lemma OAI.SignedSweeps.upperInclusion_average line 43
  4. lemma OAI.SignedSweeps.subsetAverage_apply line 51
  5. lemma OAI.SignedSweeps.subsetAverage_nonneg line 60
  6. lemma OAI.SignedSweeps.subsetAverage_card_support line 67
  7. lemma OAI.SignedSweeps.subsetAverage_mass line 78
  8. lemma OAI.SignedSweeps.upperInclusion_pointMass line 90
  9. def OAI.SignedSweeps.sweptSubsetLaw line 110
  10. lemma OAI.SignedSweeps.upperInclusion_sweep line 113
  11. lemma OAI.SignedSweeps.subsetSweep_law_properties line 121
  12. lemma OAI.SignedSweeps.sweptSubsetLaw_nonneg line 144
  13. lemma OAI.SignedSweeps.sweptSubsetLaw_card_support line 149
  14. lemma OAI.SignedSweeps.sweptSubsetLaw_mass line 155
  15. lemma OAI.SignedSweeps.sweptSubsetLaw_upper_inclusion line 161