OAI/Computability/BinPacking/Games/SelectedProfiles.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.Repetition.mergeAt line 15
  2. theorem OAI.BinPackingGames.Foundations.Repetition.mergeAt_self line 19
  3. theorem OAI.BinPackingGames.Foundations.Repetition.mergeAt_other line 23
  4. def OAI.BinPackingGames.Foundations.Repetition.partialRevealWeight line 27
  5. theorem OAI.BinPackingGames.Foundations.Repetition.product_reveal_at line 31
  6. def OAI.BinPackingGames.Foundations.Repetition.partialRevealMarginal line 41
  7. def OAI.BinPackingGames.Foundations.Repetition.fullRevealMarginal line 48
  8. theorem OAI.BinPackingGames.Foundations.Repetition.fullRevealMarginal_merge line 56
  9. def OAI.BinPackingGames.Foundations.Repetition.fullRevealModel line 82
  10. theorem OAI.BinPackingGames.Foundations.Repetition.fullRevealModel_merge line 89
  11. def OAI.BinPackingGames.Foundations.Repetition.revealSplitEquiv line 97
  12. theorem OAI.BinPackingGames.Foundations.Repetition.totalVariation_comp_equiv line 119
  13. theorem OAI.BinPackingGames.Foundations.Repetition.fullReveal_totalVariation line 127
  14. theorem OAI.BinPackingGames.Foundations.Repetition.leftReveal_full_error line 142
  15. theorem OAI.BinPackingGames.Foundations.Repetition.rightReveal_full_error line 151
  16. theorem OAI.BinPackingGames.Foundations.Repetition.selectedSplit_question_probability line 172
  17. theorem OAI.BinPackingGames.Foundations.Repetition.selectedJoint_eventMass line 188
  18. theorem OAI.BinPackingGames.Foundations.Repetition.selectedJointLaw_question_probability line 234
  19. theorem OAI.BinPackingGames.Foundations.Repetition.selectedJointLaw_questions_pushforward line 272
  20. def OAI.BinPackingGames.Foundations.Repetition.selectedRawMarginal line 301
  21. theorem OAI.BinPackingGames.Foundations.Repetition.selectedPosterior_eq_raw line 309
  22. theorem OAI.BinPackingGames.Foundations.Repetition.selectedRawMarginal_firstMarginal line 337
  23. theorem OAI.BinPackingGames.Foundations.Repetition.selectedRawMarginal_isProbability line 348
  24. theorem OAI.BinPackingGames.Foundations.Repetition.selected_raw_information_bound line 366
  25. def OAI.BinPackingGames.Foundations.Repetition.selectedOutsideLikelihood line 381
  26. def OAI.BinPackingGames.Foundations.Repetition.selectedObservationEquiv line 389
  27. theorem OAI.BinPackingGames.Foundations.Repetition.selectedRawMarginal_fullReveal line 399
  28. theorem OAI.BinPackingGames.Foundations.Repetition.selectedRawReference_fullReveal line 416
  29. theorem OAI.BinPackingGames.Foundations.Repetition.selected_raw_error_eq_fullReveal line 432
  30. theorem OAI.BinPackingGames.Foundations.Repetition.selected_fullReveal_information_bound line 446
  31. def OAI.BinPackingGames.Foundations.Repetition.selectedInformationRadius line 460
  32. theorem OAI.BinPackingGames.Foundations.Repetition.selected_leftReveal_error_sum line 467
  33. theorem OAI.BinPackingGames.Foundations.Repetition.selected_rightReveal_error_sum line 490
  34. def OAI.BinPackingGames.Foundations.Repetition.revealLeftFactor line 521
  35. def OAI.BinPackingGames.Foundations.Repetition.revealRightFactor line 526
  36. theorem OAI.BinPackingGames.Foundations.Repetition.revealLeftFactor_nonnegative line 532
  37. theorem OAI.BinPackingGames.Foundations.Repetition.revealRightFactor_nonnegative line 539
  38. theorem OAI.BinPackingGames.Foundations.Repetition.revealLaw_factorization line 545
  39. def OAI.BinPackingGames.Foundations.Repetition.partialLeftFactor line 560
  40. def OAI.BinPackingGames.Foundations.Repetition.partialRightFactor line 564
  41. theorem OAI.BinPackingGames.Foundations.Repetition.partialRevealWeight_factorization line 568
  42. theorem OAI.BinPackingGames.Foundations.Repetition.isProbability_comp_equiv line 587
  43. theorem OAI.BinPackingGames.Foundations.Repetition.partialRevealMarginal_isProbability line 596
  44. abbrev OAI.BinPackingGames.Foundations.Repetition.SelectedCommonData line 617
  45. theorem OAI.BinPackingGames.Foundations.Repetition.selected_fullReveal_isProbability line 622
  46. def OAI.BinPackingGames.Foundations.Repetition.selectedCommonLaw line 639
  47. theorem OAI.BinPackingGames.Foundations.Repetition.firstMarginal_totalVariation_le line 656
  48. def OAI.BinPackingGames.Foundations.Repetition.leftCommonMarginal line 665
  49. def OAI.BinPackingGames.Foundations.Repetition.leftCommonProfile line 668
  50. def OAI.BinPackingGames.Foundations.Repetition.swapSeedLeft line 671
  51. theorem OAI.BinPackingGames.Foundations.Repetition.leftCommonMarginal_isProbability line 677
  52. theorem OAI.BinPackingGames.Foundations.Repetition.leftCommonProfile_isProbability line 682
  53. theorem OAI.BinPackingGames.Foundations.Repetition.leftCommonProfile_error line 687
  54. def OAI.BinPackingGames.Foundations.Repetition.swapQuestionEndpoints line 724
  55. def OAI.BinPackingGames.Foundations.Repetition.rightCommonMarginal line 730
  56. def OAI.BinPackingGames.Foundations.Repetition.rightCommonProfile line 733
  57. theorem OAI.BinPackingGames.Foundations.Repetition.rightCommonProfile_isProbability line 736
  58. theorem OAI.BinPackingGames.Foundations.Repetition.swap_question_pushforward_snd line 742
  59. theorem OAI.BinPackingGames.Foundations.Repetition.leftRevealModel_swap line 748
  60. theorem OAI.BinPackingGames.Foundations.Repetition.rightCommonProfile_error line 758
  61. theorem OAI.BinPackingGames.Foundations.Repetition.finiteDistribution_nonempty line 791
  62. def OAI.BinPackingGames.Foundations.Repetition.selectedProfileFallback line 801
  63. def OAI.BinPackingGames.Foundations.Repetition.selectedLeftProfile line 809
  64. def OAI.BinPackingGames.Foundations.Repetition.selectedRightProfile line 822
  65. def OAI.BinPackingGames.Foundations.Repetition.selectedLeftProfileError line 835
  66. def OAI.BinPackingGames.Foundations.Repetition.selectedRightProfileError line 842
  67. theorem OAI.BinPackingGames.Foundations.Repetition.selectedLeftProfileError_le line 849
  68. theorem OAI.BinPackingGames.Foundations.Repetition.selectedRightProfileError_le line 863
  69. def OAI.BinPackingGames.Foundations.Repetition.selectedSamplingTarget line 877
  70. theorem OAI.BinPackingGames.Foundations.Repetition.selectedSamplingTarget_left_error line 885
  71. theorem OAI.BinPackingGames.Foundations.Repetition.selectedSamplingTarget_right_error line 898