OAI/Probability/MatroidProphet/SafeParity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.safeEndpointParityCount line 10
  2. def OAI.MatroidProphet.safeSampleCount line 15
  3. lemma OAI.MatroidProphet.safeSampleCount_parity_split line 20
  4. def OAI.MatroidProphet.fairParityExpectation line 39
  5. lemma OAI.MatroidProphet.safeSampleCount_fair_parity line 42
  6. theorem OAI.MatroidProphet.safeSampleCount_lower line 49
  7. lemma OAI.MatroidProphet.sum_unique_indicators line 72
  8. def OAI.MatroidProphet.IsSafeSample line 92
  9. lemma OAI.MatroidProphet.isSafeSample_iff_endpoint line 102
  10. def OAI.MatroidProphet.safeSampleSet line 127
  11. lemma OAI.MatroidProphet.safeSampleCount_eq_card line 133