OAI/Probability/MatroidProphet/Simulation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatroidProphet.glue line 10
  2. lemma OAI.MatroidProphet.measurable_glue line 14
  3. lemma OAI.MatroidProphet.measurable_glue_seed line 23
  4. theorem OAI.MatroidProphet.glue_fixed_law line 30
  5. theorem OAI.MatroidProphet.glue_seed_joint_law line 69
  6. theorem OAI.MatroidProphet.glue_seed_law line 95
  7. lemma OAI.MatroidProphet.measurable_weight_eval line 108
  8. def OAI.MatroidProphet.simulationHistory line 112
  9. lemma OAI.MatroidProphet.measurable_simulationHistory line 117
  10. lemma OAI.MatroidProphet.measurable_observed line 131
  11. def OAI.MatroidProphet.currentLabel line 140
  12. def OAI.MatroidProphet.sampleSimulation line 143
  13. lemma OAI.MatroidProphet.observed_glue line 159
  14. lemma OAI.MatroidProphet.simulationHistory_eq line 165
  15. lemma OAI.MatroidProphet.currentLabel_history line 171
  16. theorem OAI.MatroidProphet.sampleSimulation_acceptedThrough line 175
  17. theorem OAI.MatroidProphet.sampleSimulation_reward line 185
  18. theorem OAI.MatroidProphet.sampleSimulation_feasible line 196
  19. lemma OAI.MatroidProphet.glue_self line 211
  20. lemma OAI.MatroidProphet.hiddenWorstReward_le line 217
  21. lemma OAI.MatroidProphet.hiddenWorstReward_nonneg line 223
  22. lemma OAI.MatroidProphet.hiddenWorstReward_le_optimum line 230
  23. lemma OAI.MatroidProphet.measurable_hiddenReward line 240
  24. lemma OAI.MatroidProphet.measurable_hiddenWorstReward line 246