OAI/Computability/BinPacking/Games/QuestionMarginal.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.Repetition.revealedProductWeight line 25
  2. def OAI.BinPackingGames.Foundations.Repetition.revealedLeftWeight line 31
  3. def OAI.BinPackingGames.Foundations.Repetition.revealedRightWeight line 36
  4. theorem OAI.BinPackingGames.Foundations.Repetition.revealedProductWeight_factorizes line 41
  5. theorem OAI.BinPackingGames.Foundations.Repetition.revealedProductWeight_local_restrictions line 54
  6. theorem OAI.BinPackingGames.Foundations.Repetition.productWeight_mass line 67
  7. def OAI.BinPackingGames.Foundations.Repetition.normalizedWeight line 73
  8. theorem OAI.BinPackingGames.Foundations.Repetition.normalizedWeight_isProbability line 76
  9. theorem OAI.BinPackingGames.Foundations.Repetition.normalized_productWeight line 84
  10. theorem OAI.BinPackingGames.Foundations.Repetition.normalized_rectangle_restriction line 92
  11. def OAI.BinPackingGames.Foundations.Repetition.normalizeOr line 116
  12. theorem OAI.BinPackingGames.Foundations.Repetition.sum_mul_normalizeOr line 124
  13. theorem OAI.BinPackingGames.Foundations.Repetition.local_completion_recombination line 139
  14. theorem OAI.BinPackingGames.Foundations.Repetition.factorized_completion_row line 152
  15. def OAI.BinPackingGames.Foundations.Repetition.revealEndpoint line 175
  16. def OAI.BinPackingGames.Foundations.Repetition.revealLaw line 178
  17. theorem OAI.BinPackingGames.Foundations.Repetition.revealLaw_weight line 183
  18. def OAI.BinPackingGames.Foundations.Repetition.revealFirstLaw line 193
  19. theorem OAI.BinPackingGames.Foundations.Repetition.revealFirstLaw_weight line 198
  20. def OAI.BinPackingGames.Foundations.Repetition.revealFallback line 202
  21. def OAI.BinPackingGames.Foundations.Repetition.revealProfile line 208
  22. theorem OAI.BinPackingGames.Foundations.Repetition.revealProfile_inl_support line 212
  23. theorem OAI.BinPackingGames.Foundations.Repetition.revealProfile_inr_support line 224
  24. def OAI.BinPackingGames.Foundations.Repetition.revealInputLaw line 236
  25. theorem OAI.BinPackingGames.Foundations.Repetition.revealInputLaw_weight line 239
  26. theorem OAI.BinPackingGames.Foundations.Repetition.reveal_profile_recombination line 245
  27. theorem OAI.BinPackingGames.Foundations.Repetition.reveal_profile_inl_recombination line 252
  28. theorem OAI.BinPackingGames.Foundations.Repetition.reveal_profile_inr_recombination line 259
  29. theorem OAI.BinPackingGames.Foundations.Repetition.revealInputLaw_inl line 266
  30. theorem OAI.BinPackingGames.Foundations.Repetition.revealInputLaw_inr line 274
  31. theorem OAI.BinPackingGames.Foundations.Repetition.revealProfile_inl_diagonal line 281
  32. theorem OAI.BinPackingGames.Foundations.Repetition.revealProfile_inr_diagonal line 303
  33. theorem OAI.BinPackingGames.Foundations.Repetition.revealLaw_sum_left line 329
  34. theorem OAI.BinPackingGames.Foundations.Repetition.revealLaw_sum_right line 334
  35. theorem OAI.BinPackingGames.Foundations.Repetition.revealLaw_forget line 339
  36. theorem OAI.BinPackingGames.Foundations.Repetition.reveal_product_factorization line 348
  37. theorem OAI.BinPackingGames.Foundations.Repetition.reveal_product_forget line 358
  38. theorem OAI.BinPackingGames.Foundations.Repetition.reveal_product_expectation line 375
  39. def OAI.BinPackingGames.Foundations.Repetition.mergeCoordinates line 395
  40. def OAI.BinPackingGames.Foundations.Repetition.coordinateSplitEquiv line 399
  41. theorem OAI.BinPackingGames.Foundations.Repetition.iid_coordinate_split line 407
  42. abbrev OAI.BinPackingGames.Foundations.Repetition.SelectedLabels line 437
  43. def OAI.BinPackingGames.Foundations.Repetition.selectedQuestionTuple line 440
  44. def OAI.BinPackingGames.Foundations.Repetition.selectedAnswerLabel line 447
  45. def OAI.BinPackingGames.Foundations.Repetition.selectedLikelihood line 453
  46. theorem OAI.BinPackingGames.Foundations.Repetition.selectedLikelihood_nonnegative line 464
  47. theorem OAI.BinPackingGames.Foundations.Repetition.selectedLikelihood_sum line 475
  48. theorem OAI.BinPackingGames.Foundations.Repetition.selectedLikelihood_sum_le_one line 486
  49. def OAI.BinPackingGames.Foundations.Repetition.selectedSplitLaw line 494
  50. theorem OAI.BinPackingGames.Foundations.Repetition.selectedSplit_probability line 501
  51. abbrev OAI.BinPackingGames.Foundations.Repetition.SelectedInput line 517
  52. def OAI.BinPackingGames.Foundations.Repetition.selectedInputLaw line 520
  53. def OAI.BinPackingGames.Foundations.Repetition.selectedInputProfile line 525
  54. def OAI.BinPackingGames.Foundations.Repetition.selectedSideMass line 529
  55. theorem OAI.BinPackingGames.Foundations.Repetition.selectedSideMass_sum line 537
  56. theorem OAI.BinPackingGames.Foundations.Repetition.selectedSideMass_total line 549
  57. def OAI.BinPackingGames.Foundations.Repetition.selectedSideWeight line 571
  58. theorem OAI.BinPackingGames.Foundations.Repetition.selected_information_bound line 578
  59. def OAI.BinPackingGames.Foundations.Repetition.maskedJoint line 611
  60. def OAI.BinPackingGames.Foundations.Repetition.maskedModel line 615
  61. def OAI.BinPackingGames.Foundations.Repetition.leftRevealModel line 619
  62. def OAI.BinPackingGames.Foundations.Repetition.rightRevealModel line 623
  63. theorem OAI.BinPackingGames.Foundations.Repetition.sum_maskedJoint line 627
  64. theorem OAI.BinPackingGames.Foundations.Repetition.maskedJoint_isProbability_iff line 643
  65. theorem OAI.BinPackingGames.Foundations.Repetition.maskedJoint_firstMarginal_inl line 665
  66. theorem OAI.BinPackingGames.Foundations.Repetition.maskedJoint_firstMarginal_inr line 674
  67. theorem OAI.BinPackingGames.Foundations.Repetition.abs_half_sub_half_mul line 680
  68. theorem OAI.BinPackingGames.Foundations.Repetition.abs_masked_inl line 686
  69. theorem OAI.BinPackingGames.Foundations.Repetition.abs_masked_inr line 700
  70. theorem OAI.BinPackingGames.Foundations.Repetition.masked_totalVariation_identity line 713
  71. theorem OAI.BinPackingGames.Foundations.Repetition.leftRevealModel_totalVariation_le line 754
  72. theorem OAI.BinPackingGames.Foundations.Repetition.rightRevealModel_totalVariation_le line 761
  73. def OAI.BinPackingGames.Foundations.Repetition.selectedJointWeight line 778
  74. theorem OAI.BinPackingGames.Foundations.Repetition.selectedJointWeight_nonnegative line 789
  75. theorem OAI.BinPackingGames.Foundations.Repetition.selectedJointWeight_firstMarginal line 801
  76. theorem OAI.BinPackingGames.Foundations.Repetition.selectedJointWeight_isProbability line 812
  77. def OAI.BinPackingGames.Foundations.Repetition.selectedJointLaw line 823
  78. theorem OAI.BinPackingGames.Foundations.Repetition.selectedJointWeight_factorization line 829
  79. def OAI.BinPackingGames.Foundations.Repetition.selectedTupleLikelihood line 852
  80. theorem OAI.BinPackingGames.Foundations.Repetition.selectedTupleLikelihood_nonnegative line 858
  81. theorem OAI.BinPackingGames.Foundations.Repetition.selectedTupleLikelihood_le_one line 866
  82. theorem OAI.BinPackingGames.Foundations.Repetition.selectedTupleLikelihood_mass line 874
  83. def OAI.BinPackingGames.Foundations.Repetition.selectedQuestionMarginal line 887
  84. theorem OAI.BinPackingGames.Foundations.Repetition.selectedQuestionMarginal_weight line 894
  85. theorem OAI.BinPackingGames.Foundations.Repetition.selectedQuestionMarginal_totalVariation_sq_sum_le_log line 912
  86. theorem OAI.BinPackingGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sq_sum_le_log line 930
  87. theorem OAI.BinPackingGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt line 952
  88. theorem OAI.BinPackingGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt_sub_card line 980