OAI/Computability/UniqueGames/Games/SelectedInformationLemmas.lean

GitHub source file

48 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.UniqueGamesTheorem.Foundations.Repetition.mergeCoordinates line 16
  2. def OAI.UniqueGamesTheorem.Foundations.Repetition.coordinateSplitEquiv line 20
  3. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.iid_coordinate_split line 28
  4. abbrev OAI.UniqueGamesTheorem.Foundations.Repetition.SelectedLabels line 58
  5. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionTuple line 61
  6. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedAnswerLabel line 68
  7. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLikelihood line 74
  8. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLikelihood_nonnegative line 85
  9. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLikelihood_sum line 96
  10. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLikelihood_sum_le_one line 107
  11. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedSplitLaw line 115
  12. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedSplit_probability line 122
  13. abbrev OAI.UniqueGamesTheorem.Foundations.Repetition.SelectedInput line 138
  14. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedInputLaw line 141
  15. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedInputProfile line 146
  16. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedSideMass line 150
  17. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedSideMass_sum line 158
  18. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedSideMass_total line 172

    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.UniqueGamesTheorem.Foundations.Repetition.selectedInputLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.selectedSideMass

  19. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedSideWeight line 194
  20. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_information_bound line 201
  21. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedTupleLikelihood line 250
  22. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedTupleLikelihood_nonnegative line 256
  23. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedTupleLikelihood_le_one line 264
  24. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedTupleLikelihood_mass line 272
  25. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionMarginal line 287

    Source documentation

    The coordinate pair under the actual repeated question law conditioned on the selected wins, rather than a separately postulated posterior law.

    def selectedQuestionMarginal (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (positive : 0 < G.selectedSuccess strategy selected)
    (i : Fin n) : FiniteDistribution (Q₁ × Q₂) :=
…
  26. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionMarginal_weight line 294
  27. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionMarginal_totalVariation_sq_sum_le_log line 314

    Source documentation

    The full-coordinate squared-distance bound specialized to the actual game and actual selected event.

    theorem selectedQuestionMarginal_totalVariation_sq_sum_le_log
    (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (positive : 0 < G.selectedSuccess strategy selected) :
    (∑ i : Fin n,
      (selectedQuestionMarginal G strategy selected positive i).totalVariation G.questions ^ 2) ≤
        Real.log (1 / G.selectedSuccess strategy selected) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionMarginal

  28. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sq_sum_le_log line 334

    Source documentation

    Restricting to the unused coordinates does not spend any further information budget.

    theorem unselectedQuestionMarginal_totalVariation_sq_sum_le_log
    (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (positive : 0 < G.selectedSuccess strategy selected) :
    (∑ i : {i : Fin n // i ∉ selected},
      (selectedQuestionMarginal G strategy selected positive i.1).totalVariation G.questions ^ 2) ≤
        Real.log (1 / G.selectedSuccess strategy selected) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionMarginal

  29. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt line 358

    Source documentation

    The marginal-pair term used in Holenstein's dependency-breaking argument. The estimate is valid also when there are no unused coordinates.

    theorem unselectedQuestionMarginal_totalVariation_sum_le_sqrt
    (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (positive : 0 < G.selectedSuccess strategy selected) :
    (∑ i : {i : Fin n // i ∉ selected},
      (selectedQuestionMarginal G strategy selected positive i.1).totalVariation G.questions) ≤
        Real.sqrt ((Fintype.card {i : Fin n // i ∉ selected} : ℝ) *
          Real.log (1 / G.selectedSuccess strategy selected)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionMarginal

  30. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt_sub_card line 386
  31. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedJointWeight line 419
  32. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedJointWeight_nonnegative line 430
  33. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedJointWeight_firstMarginal line 442
  34. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedJointWeight_isProbability line 453
  35. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedJointLaw line 464
  36. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedJointWeight_factorization line 472

    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.UniqueGamesTheorem.Foundations.Repetition.selectedJointWeight, OAI.UniqueGamesTheorem.Foundations.Repetition.revealLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLikelihood

  37. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedSplit_question_probability line 510
  38. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedJoint_eventMass line 528

    Source documentation

    Marginalizing the actual likelihood against any question event gives the joint probability of selected-coordinate success and that event.

    theorem selectedJoint_eventMass (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n))
    (event : ((Fin n → Q₁) × (Fin n → Q₂)) → Bool) :
    (∑ tv : SelectedInput Q₁ Q₂ selected ×
        SelectedLabels (A₁ := A₁) (A₂ := A₂) selected,
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.SelectedInput, OAI.UniqueGamesTheorem.Foundations.Repetition.SelectedLabels

  39. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedJointLaw_question_probability line 574
  40. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedJointLaw_questions_pushforward line 614

    Source documentation

    The auxiliary law's question marginal is the actual repeated-game question law conditioned on the selected-win event.

    theorem selectedJointLaw_questions_pushforward (G : Game Q₁ Q₂ A₁ A₂)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (selected : Finset (Fin n)) (positive : 0 < G.selectedSuccess strategy selected) :
    (selectedJointLaw G strategy selected positive).pushforward
      (fun z => selectedQuestionTuple selected z.1.1.1 z.2) =
        (G.repetition n).questions.condition (G.selectedWins strategy selected) positive := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.selectedJointLaw, OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionTuple

  41. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLabelAccepts line 650
  42. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLocalAnswers line 656
  43. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLocalTest line 661
  44. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLocalTest_nonnegative line 667
  45. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionTuple_left line 676
  46. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedQuestionTuple_right line 685
  47. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedWins_of_answerLabel line 694
  48. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLikelihood_factorization line 718