OAI/Probability/MatroidProphet/SeedLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.seedSet line 12
  2. def OAI.MatroidProphet.setSeed line 15
  3. lemma OAI.MatroidProphet.seedSet_setSeed line 18
  4. lemma OAI.MatroidProphet.setSeed_seedSet line 23
  5. def OAI.MatroidProphet.seedFinsetEquiv line 27
  6. lemma OAI.MatroidProphet.seedWeight_sum line 33
  7. def OAI.MatroidProphet.seedPMF line 42
  8. def OAI.MatroidProphet.bernoulliSeedLaw line 48
  9. instance OAI.MatroidProphet.bernoulliSeedLaw_probability line 52
  10. theorem OAI.MatroidProphet.integral_bernoulliSeedLaw line 58