OAI/Combinatorics/IndependentSets/Repetition/SelectedProfiles.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.Repetition.finiteDistribution_nonempty line 16
  2. def OAI.IndependentSetsGames.Foundations.Repetition.selectedProfileFallback line 26
  3. def OAI.IndependentSetsGames.Foundations.Repetition.selectedLeftProfile line 34
  4. def OAI.IndependentSetsGames.Foundations.Repetition.selectedRightProfile line 47
  5. def OAI.IndependentSetsGames.Foundations.Repetition.selectedLeftProfileError line 60
  6. def OAI.IndependentSetsGames.Foundations.Repetition.selectedRightProfileError line 67
  7. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedLeftProfileError_le line 74
  8. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedRightProfileError_le line 88
  9. def OAI.IndependentSetsGames.Foundations.Repetition.selectedSamplingTarget line 102
  10. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedSamplingTarget_left_error line 110
  11. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedSamplingTarget_right_error line 123
  12. theorem OAI.IndependentSetsGames.Foundations.Repetition.pushforward_snd_weight_eq_secondMarginal line 141
  13. def OAI.IndependentSetsGames.Foundations.Repetition.revealDataSplitEquiv line 151
  14. theorem OAI.IndependentSetsGames.Foundations.Repetition.partialRevealMarginal_secondMarginal line 168
  15. def OAI.IndependentSetsGames.Foundations.Repetition.selectedObservationDataEquiv line 188
  16. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedFullReveal_secondMarginal line 197
  17. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedRawMarginal_secondMarginal line 211
  18. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedCommonLaw_secondMarginal line 233
  19. theorem OAI.IndependentSetsGames.Foundations.Repetition.selectedCommonLaw_questions_pushforward line 244