OAI/Probability/MatroidProphet/Pivots/Patterns.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.Pivots.occurrenceMark line 18
  2. def OAI.MatroidProphet.Pivots.markedScore line 21
  3. lemma OAI.MatroidProphet.Pivots.abs_markedScore line 26
  4. def OAI.MatroidProphet.Pivots.fixedOldScore line 32
  5. def OAI.MatroidProphet.Pivots.constantScore line 35
  6. def OAI.MatroidProphet.Pivots.coordinateScore line 38
  7. def OAI.MatroidProphet.Pivots.patternLinear line 41
  8. def OAI.MatroidProphet.Pivots.patternConstant line 45
  9. lemma OAI.MatroidProphet.Pivots.affineScore_eq_sum line 49
  10. def OAI.MatroidProphet.Pivots.RecordsPivots line 63
  11. lemma OAI.MatroidProphet.Pivots.recordsPivots_affine line 69