OAI/Computability/BinPacking/Games/Holenstein.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.Repetition.selectedLabelAccepts line 15
  2. def OAI.BinPackingGames.Foundations.Repetition.selectedLocalAnswers line 21
  3. def OAI.BinPackingGames.Foundations.Repetition.selectedLocalTest line 26
  4. theorem OAI.BinPackingGames.Foundations.Repetition.selectedLocalTest_nonnegative line 32
  5. theorem OAI.BinPackingGames.Foundations.Repetition.selectedQuestionTuple_left line 41
  6. theorem OAI.BinPackingGames.Foundations.Repetition.selectedQuestionTuple_right line 50
  7. theorem OAI.BinPackingGames.Foundations.Repetition.selectedWins_of_answerLabel line 59
  8. theorem OAI.BinPackingGames.Foundations.Repetition.selectedLikelihood_factorization line 83
  9. theorem OAI.BinPackingGames.Foundations.Repetition.pushforward_snd_weight_eq_secondMarginal line 126
  10. def OAI.BinPackingGames.Foundations.Repetition.revealDataSplitEquiv line 136
  11. theorem OAI.BinPackingGames.Foundations.Repetition.partialRevealMarginal_secondMarginal line 153
  12. def OAI.BinPackingGames.Foundations.Repetition.selectedObservationDataEquiv line 173
  13. theorem OAI.BinPackingGames.Foundations.Repetition.selectedFullReveal_secondMarginal line 182
  14. theorem OAI.BinPackingGames.Foundations.Repetition.selectedRawMarginal_secondMarginal line 196
  15. theorem OAI.BinPackingGames.Foundations.Repetition.selectedCommonLaw_secondMarginal line 218
  16. theorem OAI.BinPackingGames.Foundations.Repetition.selectedCommonLaw_questions_pushforward line 229
  17. def OAI.BinPackingGames.Foundations.Repetition.completionTupleEquiv line 254
  18. def OAI.BinPackingGames.Foundations.Repetition.updatedTableFallback line 260
  19. theorem OAI.BinPackingGames.Foundations.Repetition.updatedTableFallback_zero line 265
  20. theorem OAI.BinPackingGames.Foundations.Repetition.normalizeOr_weight_eq_zero_of_zero line 277
  21. def OAI.BinPackingGames.Foundations.Repetition.selectedLeftRaw line 294
  22. def OAI.BinPackingGames.Foundations.Repetition.selectedRightRaw line 302
  23. theorem OAI.BinPackingGames.Foundations.Repetition.selectedLeftRaw_nonnegative line 311
  24. theorem OAI.BinPackingGames.Foundations.Repetition.selectedRightRaw_nonnegative line 324
  25. def OAI.BinPackingGames.Foundations.Repetition.selectedLeftCompletion line 336
  26. def OAI.BinPackingGames.Foundations.Repetition.selectedRightCompletion line 345
  27. theorem OAI.BinPackingGames.Foundations.Repetition.selectedLeftCompletion_zero line 355
  28. theorem OAI.BinPackingGames.Foundations.Repetition.selectedRightCompletion_zero line 366
  29. theorem OAI.BinPackingGames.Foundations.Repetition.selectedLeftCompletion_support line 377
  30. theorem OAI.BinPackingGames.Foundations.Repetition.selectedRightCompletion_support line 387
  31. def OAI.BinPackingGames.Foundations.Repetition.selectedCompletionScale line 396
  32. theorem OAI.BinPackingGames.Foundations.Repetition.selected_completion_factorization line 405
  33. theorem OAI.BinPackingGames.Foundations.Repetition.selectedCommonLaw_completion_row_mass line 430
  34. theorem OAI.BinPackingGames.Foundations.Repetition.selected_completion_row_recombine line 452
  35. theorem OAI.BinPackingGames.Foundations.Repetition.partialRevealWeight_forget line 488
  36. theorem OAI.BinPackingGames.Foundations.Repetition.partialReveal_event_forget line 500
  37. theorem OAI.BinPackingGames.Foundations.Repetition.selectedOutsideLikelihood_event_sum line 517
  38. theorem OAI.BinPackingGames.Foundations.Repetition.selected_partial_event_total line 580
  39. def OAI.BinPackingGames.Foundations.Repetition.selectedFullLeftCompletion line 601
  40. def OAI.BinPackingGames.Foundations.Repetition.selectedFullRightCompletion line 609
  41. theorem OAI.BinPackingGames.Foundations.Repetition.selectedFullLeftCompletion_support line 618
  42. theorem OAI.BinPackingGames.Foundations.Repetition.selectedFullRightCompletion_support line 640
  43. theorem OAI.BinPackingGames.Foundations.Repetition.selected_full_completion_probability line 661
  44. theorem OAI.BinPackingGames.Foundations.Repetition.selected_completion_event_row line 687
  45. def OAI.BinPackingGames.Foundations.Repetition.selectedFullCompletionMixture line 731
  46. theorem OAI.BinPackingGames.Foundations.Repetition.selectedFullCompletionMixture_probability line 740
  47. theorem OAI.BinPackingGames.Foundations.Repetition.selectedFullCompletionMixture_eq_conditionedQuestions line 762
  48. theorem OAI.BinPackingGames.Foundations.Repetition.selectedQuestionRadius_le_informationRadius line 785
  49. theorem OAI.BinPackingGames.Foundations.Repetition.selectedQuestionMarginal_error_sum line 801
  50. def OAI.BinPackingGames.Foundations.Repetition.selectedEmbeddingError line 811
  51. theorem OAI.BinPackingGames.Foundations.Repetition.selectedEmbeddingError_nonnegative line 818
  52. theorem OAI.BinPackingGames.Foundations.Repetition.selectedLeftProfileError_sum line 827
  53. theorem OAI.BinPackingGames.Foundations.Repetition.selectedRightProfileError_sum line 845
  54. theorem OAI.BinPackingGames.Foundations.Repetition.selectedEmbeddingError_sum_le_fifteen line 863
  55. theorem OAI.BinPackingGames.Foundations.Repetition.selected_coordinate_probability_le_value_add_error line 884
  56. theorem OAI.BinPackingGames.Foundations.Repetition.holenstein_conditionalCoordinateBound line 913
  57. theorem OAI.BinPackingGames.Foundations.Repetition.holenstein_repetition_success line 927
  58. theorem OAI.BinPackingGames.Foundations.Repetition.holenstein_repetition_value line 937