OAI/Computability/DirectedFeedback/Games/SelectedInformation.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Foundations.Repetition.mergeCoordinates line 12
  2. def OAI.DFVSGames.Foundations.Repetition.coordinateSplitEquiv line 16
  3. theorem OAI.DFVSGames.Foundations.Repetition.iid_coordinate_split line 24
  4. abbrev OAI.DFVSGames.Foundations.Repetition.SelectedLabels line 54
  5. def OAI.DFVSGames.Foundations.Repetition.selectedQuestionTuple line 57
  6. def OAI.DFVSGames.Foundations.Repetition.selectedAnswerLabel line 64
  7. def OAI.DFVSGames.Foundations.Repetition.selectedLikelihood line 70
  8. theorem OAI.DFVSGames.Foundations.Repetition.selectedLikelihood_nonnegative line 81
  9. theorem OAI.DFVSGames.Foundations.Repetition.selectedLikelihood_sum line 92
  10. theorem OAI.DFVSGames.Foundations.Repetition.selectedLikelihood_sum_le_one line 103
  11. def OAI.DFVSGames.Foundations.Repetition.selectedSplitLaw line 111
  12. theorem OAI.DFVSGames.Foundations.Repetition.selectedSplit_probability line 118
  13. abbrev OAI.DFVSGames.Foundations.Repetition.SelectedInput line 134
  14. def OAI.DFVSGames.Foundations.Repetition.selectedInputLaw line 137
  15. def OAI.DFVSGames.Foundations.Repetition.selectedInputProfile line 142
  16. def OAI.DFVSGames.Foundations.Repetition.selectedSideMass line 146
  17. theorem OAI.DFVSGames.Foundations.Repetition.selectedSideMass_sum line 154
  18. theorem OAI.DFVSGames.Foundations.Repetition.selectedSideMass_total line 166
  19. def OAI.DFVSGames.Foundations.Repetition.selectedSideWeight line 188
  20. theorem OAI.DFVSGames.Foundations.Repetition.selected_information_bound line 195
  21. def OAI.DFVSGames.Foundations.Repetition.selectedJointWeight line 234
  22. theorem OAI.DFVSGames.Foundations.Repetition.selectedJointWeight_nonnegative line 245
  23. theorem OAI.DFVSGames.Foundations.Repetition.selectedJointWeight_firstMarginal line 257
  24. theorem OAI.DFVSGames.Foundations.Repetition.selectedJointWeight_isProbability line 268
  25. def OAI.DFVSGames.Foundations.Repetition.selectedJointLaw line 279
  26. theorem OAI.DFVSGames.Foundations.Repetition.selectedJointWeight_factorization line 285
  27. def OAI.DFVSGames.Foundations.Repetition.maskedJoint line 308
  28. def OAI.DFVSGames.Foundations.Repetition.maskedModel line 312
  29. def OAI.DFVSGames.Foundations.Repetition.leftRevealModel line 316
  30. def OAI.DFVSGames.Foundations.Repetition.rightRevealModel line 320
  31. theorem OAI.DFVSGames.Foundations.Repetition.sum_maskedJoint line 324
  32. theorem OAI.DFVSGames.Foundations.Repetition.maskedJoint_isProbability_iff line 340
  33. theorem OAI.DFVSGames.Foundations.Repetition.maskedJoint_firstMarginal_inl line 362
  34. theorem OAI.DFVSGames.Foundations.Repetition.maskedJoint_firstMarginal_inr line 371
  35. theorem OAI.DFVSGames.Foundations.Repetition.abs_half_sub_half_mul_inline_MaskedVariation line 377
  36. theorem OAI.DFVSGames.Foundations.Repetition.abs_masked_inl line 383
  37. theorem OAI.DFVSGames.Foundations.Repetition.abs_masked_inr line 397
  38. theorem OAI.DFVSGames.Foundations.Repetition.masked_totalVariation_identity line 410
  39. theorem OAI.DFVSGames.Foundations.Repetition.leftRevealModel_totalVariation_le line 451
  40. theorem OAI.DFVSGames.Foundations.Repetition.rightRevealModel_totalVariation_le line 458
  41. def OAI.DFVSGames.Foundations.Repetition.mergeAt line 475
  42. theorem OAI.DFVSGames.Foundations.Repetition.mergeAt_self line 479
  43. theorem OAI.DFVSGames.Foundations.Repetition.mergeAt_other line 483
  44. def OAI.DFVSGames.Foundations.Repetition.partialRevealWeight line 487
  45. theorem OAI.DFVSGames.Foundations.Repetition.product_reveal_at line 491
  46. def OAI.DFVSGames.Foundations.Repetition.partialRevealMarginal line 501
  47. def OAI.DFVSGames.Foundations.Repetition.fullRevealMarginal line 508
  48. theorem OAI.DFVSGames.Foundations.Repetition.fullRevealMarginal_merge line 517
  49. def OAI.DFVSGames.Foundations.Repetition.fullRevealModel line 543
  50. theorem OAI.DFVSGames.Foundations.Repetition.fullRevealModel_merge line 550
  51. def OAI.DFVSGames.Foundations.Repetition.revealSplitEquiv line 558
  52. theorem OAI.DFVSGames.Foundations.Repetition.totalVariation_comp_equiv line 580
  53. theorem OAI.DFVSGames.Foundations.Repetition.fullReveal_totalVariation line 588
  54. theorem OAI.DFVSGames.Foundations.Repetition.leftReveal_full_error line 603
  55. theorem OAI.DFVSGames.Foundations.Repetition.rightReveal_full_error line 612
  56. def OAI.DFVSGames.Foundations.Repetition.selectedRawMarginal line 633
  57. theorem OAI.DFVSGames.Foundations.Repetition.selectedPosterior_eq_raw line 641
  58. theorem OAI.DFVSGames.Foundations.Repetition.selectedRawMarginal_firstMarginal line 669
  59. theorem OAI.DFVSGames.Foundations.Repetition.selectedRawMarginal_isProbability line 680
  60. theorem OAI.DFVSGames.Foundations.Repetition.selected_raw_information_bound line 698
  61. def OAI.DFVSGames.Foundations.Repetition.selectedOutsideLikelihood line 713
  62. def OAI.DFVSGames.Foundations.Repetition.selectedObservationEquiv line 721
  63. theorem OAI.DFVSGames.Foundations.Repetition.selectedRawMarginal_fullReveal line 731
  64. theorem OAI.DFVSGames.Foundations.Repetition.selectedRawReference_fullReveal line 748
  65. theorem OAI.DFVSGames.Foundations.Repetition.selected_raw_error_eq_fullReveal line 764
  66. theorem OAI.DFVSGames.Foundations.Repetition.selected_fullReveal_information_bound line 778
  67. def OAI.DFVSGames.Foundations.Repetition.selectedInformationRadius line 792
  68. theorem OAI.DFVSGames.Foundations.Repetition.selected_leftReveal_error_sum line 799
  69. theorem OAI.DFVSGames.Foundations.Repetition.selected_rightReveal_error_sum line 822