OAI/Probability/MatroidProphet/Reverse/Exposure.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MatroidProphet.ReverseLayer line 13
  2. def OAI.MatroidProphet.layerNominal line 19
  3. def OAI.MatroidProphet.layerBatch line 23
  4. def OAI.MatroidProphet.layerUpdate line 27
  5. lemma OAI.MatroidProphet.layerUpdate_eq_batch line 31
  6. def OAI.MatroidProphet.runReverseLayers line 41
  7. def OAI.MatroidProphet.reverseExposureTree line 46
  8. lemma OAI.MatroidProphet.reverseExposureTree_fresh line 53
  9. lemma OAI.MatroidProphet.layerUpdate_congr line 75
  10. lemma OAI.MatroidProphet.runReverseLayers_congr line 86
  11. lemma OAI.MatroidProphet.reverseExposureTree_run line 96
  12. theorem OAI.MatroidProphet.reverseExposure_hybrid_independent line 115
  13. lemma OAI.MatroidProphet.runReverseLayers_append line 130
  14. def OAI.MatroidProphet.sourceLayer line 138
  15. def OAI.MatroidProphet.sourceLayers line 141
  16. lemma OAI.MatroidProphet.sourceLayers_pairwise line 145
  17. lemma OAI.MatroidProphet.runReverseLayers_source line 152
  18. theorem OAI.MatroidProphet.source_reverse_hybrid_independent line 168
  19. def OAI.MatroidProphet.queriedReverseLayers line 191
  20. lemma OAI.MatroidProphet.queriedReverseLayers_congr line 197
  21. lemma OAI.MatroidProphet.reverseExposureTree_queried line 209
  22. lemma OAI.MatroidProphet.queriedReverseLayers_append line 229
  23. lemma OAI.MatroidProphet.queriedReverseLayers_source line 238