OAI/Computability/MaxCut/PCP/SelectedInformation.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

Concrete selected-coordinate questions and answer labels for the side-information inequality. The event is the actual repeated game's selected success event.

  1. def OAI.MaxCutGames.Foundations.Repetition.mergeCoordinates line 18
  2. def OAI.MaxCutGames.Foundations.Repetition.coordinateSplitEquiv line 22
  3. theorem OAI.MaxCutGames.Foundations.Repetition.iid_coordinate_split line 30
  4. abbrev OAI.MaxCutGames.Foundations.Repetition.SelectedLabels line 60
  5. def OAI.MaxCutGames.Foundations.Repetition.selectedQuestionTuple line 63
  6. def OAI.MaxCutGames.Foundations.Repetition.selectedAnswerLabel line 70
  7. def OAI.MaxCutGames.Foundations.Repetition.selectedLikelihood line 76
  8. theorem OAI.MaxCutGames.Foundations.Repetition.selectedLikelihood_nonnegative line 87
  9. theorem OAI.MaxCutGames.Foundations.Repetition.selectedLikelihood_sum line 98
  10. theorem OAI.MaxCutGames.Foundations.Repetition.selectedLikelihood_sum_le_one line 109
  11. def OAI.MaxCutGames.Foundations.Repetition.selectedSplitLaw line 117
  12. theorem OAI.MaxCutGames.Foundations.Repetition.selectedSplit_probability line 124
  13. abbrev OAI.MaxCutGames.Foundations.Repetition.SelectedInput line 140
  14. def OAI.MaxCutGames.Foundations.Repetition.selectedInputLaw line 143
  15. def OAI.MaxCutGames.Foundations.Repetition.selectedInputProfile line 148
  16. def OAI.MaxCutGames.Foundations.Repetition.selectedSideMass line 152
  17. theorem OAI.MaxCutGames.Foundations.Repetition.selectedSideMass_sum line 160
  18. theorem OAI.MaxCutGames.Foundations.Repetition.selectedSideMass_total line 174

    Source documentation

    The side-information normalizer is the actual selected-win probability of the repeated strategy. No event-mass hypothesis is required.

    theorem selectedSideMass_total (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) :
    (∑ tv, (selectedInputLaw G selected).weight tv.1 *
      selectedSideMass G strategy selected tv) = G.selectedSuccess strategy selected := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.selectedInputLaw, OAI.MaxCutGames.Foundations.Repetition.selectedSideMass

  19. def OAI.MaxCutGames.Foundations.Repetition.selectedSideWeight line 196
  20. theorem OAI.MaxCutGames.Foundations.Repetition.selected_information_bound line 203
  21. def OAI.MaxCutGames.Foundations.Repetition.selectedJointWeight line 241
  22. theorem OAI.MaxCutGames.Foundations.Repetition.selectedJointWeight_nonnegative line 252
  23. theorem OAI.MaxCutGames.Foundations.Repetition.selectedJointWeight_firstMarginal line 264
  24. theorem OAI.MaxCutGames.Foundations.Repetition.selectedJointWeight_isProbability line 275
  25. def OAI.MaxCutGames.Foundations.Repetition.selectedJointLaw line 286
  26. theorem OAI.MaxCutGames.Foundations.Repetition.selectedJointWeight_factorization line 294

    Source documentation

    Pointwise product formula for the actual conditional joint law. The selected-answer test depends on the question tuples, and not on any reveal.

    theorem selectedJointWeight_factorization (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (tv) (u) :
    selectedJointWeight G strategy selected (tv,u) =
      (∏ i : selected, G.questions.weight (tv.1.1 i)) *
        (∏ i : {i : Fin n // i ∉ selected}, (revealLaw G.questions).weight (u i,tv.1.2 i)) *
          selectedLikelihood G strategy selected tv.1.1 tv.2 u /
            G.selectedSuccess strategy selected := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.selectedJointWeight, OAI.MaxCutGames.Foundations.Repetition.revealLaw, OAI.MaxCutGames.Foundations.Repetition.selectedLikelihood

  27. def OAI.MaxCutGames.Foundations.Repetition.maskedJoint line 317
  28. def OAI.MaxCutGames.Foundations.Repetition.maskedModel line 321
  29. def OAI.MaxCutGames.Foundations.Repetition.leftRevealModel line 325
  30. def OAI.MaxCutGames.Foundations.Repetition.rightRevealModel line 329
  31. theorem OAI.MaxCutGames.Foundations.Repetition.sum_maskedJoint line 333
  32. theorem OAI.MaxCutGames.Foundations.Repetition.maskedJoint_isProbability_iff line 349
  33. theorem OAI.MaxCutGames.Foundations.Repetition.maskedJoint_firstMarginal_inl line 371
  34. theorem OAI.MaxCutGames.Foundations.Repetition.maskedJoint_firstMarginal_inr line 380
  35. theorem OAI.MaxCutGames.Foundations.Repetition.abs_half_sub_half_mul_inline_MaskedVariation line 386
  36. theorem OAI.MaxCutGames.Foundations.Repetition.abs_masked_inl line 392
  37. theorem OAI.MaxCutGames.Foundations.Repetition.abs_masked_inr line 406
  38. theorem OAI.MaxCutGames.Foundations.Repetition.masked_totalVariation_identity line 419
  39. theorem OAI.MaxCutGames.Foundations.Repetition.leftRevealModel_totalVariation_le line 460
  40. theorem OAI.MaxCutGames.Foundations.Repetition.rightRevealModel_totalVariation_le line 467
  41. def OAI.MaxCutGames.Foundations.Repetition.mergeAt line 483
  42. theorem OAI.MaxCutGames.Foundations.Repetition.mergeAt_self line 487
  43. theorem OAI.MaxCutGames.Foundations.Repetition.mergeAt_other line 491
  44. def OAI.MaxCutGames.Foundations.Repetition.partialRevealWeight line 495
  45. theorem OAI.MaxCutGames.Foundations.Repetition.product_reveal_at line 499
  46. def OAI.MaxCutGames.Foundations.Repetition.partialRevealMarginal line 509
  47. def OAI.MaxCutGames.Foundations.Repetition.fullRevealMarginal line 516
  48. theorem OAI.MaxCutGames.Foundations.Repetition.fullRevealMarginal_merge line 525
  49. def OAI.MaxCutGames.Foundations.Repetition.fullRevealModel line 551
  50. theorem OAI.MaxCutGames.Foundations.Repetition.fullRevealModel_merge line 558
  51. def OAI.MaxCutGames.Foundations.Repetition.revealSplitEquiv line 566
  52. theorem OAI.MaxCutGames.Foundations.Repetition.totalVariation_comp_equiv line 588
  53. theorem OAI.MaxCutGames.Foundations.Repetition.fullReveal_totalVariation line 598

    Source documentation

    The variation quantity for the explicit full reveal law equals the two-branch masked quantity after extracting one reveal coordinate.

    theorem fullReveal_totalVariation (μ : Games.FiniteDistribution (X × Y)) (j : I)
    (likelihood : T → (I → X × Y) → ℝ) :
    Information.totalVariation (fullRevealMarginal μ j likelihood) (fullRevealModel μ j likelihood) =
      Information.totalVariation (maskedJoint (partialRevealMarginal μ j likelihood))
        (maskedModel μ (partialRevealMarginal μ j likelihood)) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Games.FiniteDistribution, OAI.MaxCutGames.Foundations.Information.totalVariation, OAI.MaxCutGames.Foundations.Repetition.fullRevealMarginal, OAI.MaxCutGames.Foundations.Repetition.fullRevealModel, OAI.MaxCutGames.Foundations.Repetition.maskedJoint, OAI.MaxCutGames.Foundations.Repetition.partialRevealMarginal, OAI.MaxCutGames.Foundations.Repetition.maskedModel

  54. theorem OAI.MaxCutGames.Foundations.Repetition.leftReveal_full_error line 613
  55. theorem OAI.MaxCutGames.Foundations.Repetition.rightReveal_full_error line 622
  56. def OAI.MaxCutGames.Foundations.Repetition.selectedRawMarginal line 641
  57. theorem OAI.MaxCutGames.Foundations.Repetition.selectedPosterior_eq_raw line 649
  58. theorem OAI.MaxCutGames.Foundations.Repetition.selectedRawMarginal_firstMarginal line 677
  59. theorem OAI.MaxCutGames.Foundations.Repetition.selectedRawMarginal_isProbability line 688
  60. theorem OAI.MaxCutGames.Foundations.Repetition.selected_raw_information_bound line 706
  61. def OAI.MaxCutGames.Foundations.Repetition.selectedOutsideLikelihood line 721
  62. def OAI.MaxCutGames.Foundations.Repetition.selectedObservationEquiv line 729
  63. theorem OAI.MaxCutGames.Foundations.Repetition.selectedRawMarginal_fullReveal line 739
  64. theorem OAI.MaxCutGames.Foundations.Repetition.selectedRawReference_fullReveal line 756
  65. theorem OAI.MaxCutGames.Foundations.Repetition.selected_raw_error_eq_fullReveal line 772
  66. theorem OAI.MaxCutGames.Foundations.Repetition.selected_fullReveal_information_bound line 786
  67. def OAI.MaxCutGames.Foundations.Repetition.selectedInformationRadius line 800
  68. theorem OAI.MaxCutGames.Foundations.Repetition.selected_leftReveal_error_sum line 807
  69. theorem OAI.MaxCutGames.Foundations.Repetition.selected_rightReveal_error_sum line 830