OAI/Computability/MaxCut/PCP/SelectedJointGame.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Identification of the auxiliary selected-answer/reveal law with the actual repeated-game question law conditioned on selected-coordinate success. The proof sums out answer labels and reveal «variables» before merging the selected and unselected question coordinates.

  1. theorem OAI.MaxCutGames.Foundations.Repetition.selectedSplit_question_probability line 25
  2. theorem OAI.MaxCutGames.Foundations.Repetition.selectedJoint_eventMass line 43

    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.MaxCutGames.Foundations.Repetition.SelectedInput, OAI.MaxCutGames.Foundations.Repetition.SelectedLabels

  3. theorem OAI.MaxCutGames.Foundations.Repetition.selectedJointLaw_question_probability line 89
  4. theorem OAI.MaxCutGames.Foundations.Repetition.selectedJointLaw_questions_pushforward line 129

    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.MaxCutGames.Foundations.Repetition.selectedJointLaw, OAI.MaxCutGames.Foundations.Repetition.selectedQuestionTuple

  5. def OAI.MaxCutGames.Foundations.Repetition.selectedTupleLikelihood line 168
  6. theorem OAI.MaxCutGames.Foundations.Repetition.selectedTupleLikelihood_nonnegative line 174
  7. theorem OAI.MaxCutGames.Foundations.Repetition.selectedTupleLikelihood_le_one line 182
  8. theorem OAI.MaxCutGames.Foundations.Repetition.selectedTupleLikelihood_mass line 190
  9. def OAI.MaxCutGames.Foundations.Repetition.selectedQuestionMarginal line 205

    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₂) :=
…
  10. theorem OAI.MaxCutGames.Foundations.Repetition.selectedQuestionMarginal_weight line 212
  11. theorem OAI.MaxCutGames.Foundations.Repetition.selectedQuestionMarginal_totalVariation_sq_sum_le_log line 232

    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.MaxCutGames.Foundations.Repetition.selectedQuestionMarginal

  12. theorem OAI.MaxCutGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sq_sum_le_log line 252

    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.MaxCutGames.Foundations.Repetition.selectedQuestionMarginal

  13. theorem OAI.MaxCutGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt line 276

    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.MaxCutGames.Foundations.Repetition.selectedQuestionMarginal

  14. theorem OAI.MaxCutGames.Foundations.Repetition.unselectedQuestionMarginal_totalVariation_sum_le_sqrt_sub_card line 304
  15. theorem OAI.MaxCutGames.Foundations.Repetition.isProbability_comp_equiv line 329
  16. theorem OAI.MaxCutGames.Foundations.Repetition.partialRevealMarginal_isProbability line 338
  17. abbrev OAI.MaxCutGames.Foundations.Repetition.SelectedCommonData line 359
  18. theorem OAI.MaxCutGames.Foundations.Repetition.selected_fullReveal_isProbability line 364
  19. def OAI.MaxCutGames.Foundations.Repetition.selectedCommonLaw line 381
  20. theorem OAI.MaxCutGames.Foundations.Repetition.firstMarginal_totalVariation_le line 402
  21. def OAI.MaxCutGames.Foundations.Repetition.leftCommonMarginal line 411
  22. def OAI.MaxCutGames.Foundations.Repetition.leftCommonProfile line 414
  23. def OAI.MaxCutGames.Foundations.Repetition.swapSeedLeft line 417
  24. theorem OAI.MaxCutGames.Foundations.Repetition.leftCommonMarginal_isProbability line 423
  25. theorem OAI.MaxCutGames.Foundations.Repetition.leftCommonProfile_isProbability line 428
  26. theorem OAI.MaxCutGames.Foundations.Repetition.leftCommonProfile_error line 433
  27. def OAI.MaxCutGames.Foundations.Repetition.swapQuestionEndpoints line 479
  28. def OAI.MaxCutGames.Foundations.Repetition.rightCommonMarginal line 485
  29. def OAI.MaxCutGames.Foundations.Repetition.rightCommonProfile line 488
  30. theorem OAI.MaxCutGames.Foundations.Repetition.rightCommonProfile_isProbability line 491
  31. theorem OAI.MaxCutGames.Foundations.Repetition.swap_question_pushforward_snd line 497
  32. theorem OAI.MaxCutGames.Foundations.Repetition.leftRevealModel_swap line 503
  33. theorem OAI.MaxCutGames.Foundations.Repetition.rightCommonProfile_error line 513
  34. theorem OAI.MaxCutGames.Foundations.Repetition.finiteDistribution_nonempty line 551
  35. def OAI.MaxCutGames.Foundations.Repetition.selectedProfileFallback line 561
  36. def OAI.MaxCutGames.Foundations.Repetition.selectedLeftProfile line 569
  37. def OAI.MaxCutGames.Foundations.Repetition.selectedRightProfile line 582
  38. def OAI.MaxCutGames.Foundations.Repetition.selectedLeftProfileError line 595
  39. def OAI.MaxCutGames.Foundations.Repetition.selectedRightProfileError line 602
  40. theorem OAI.MaxCutGames.Foundations.Repetition.selectedLeftProfileError_le line 609
  41. theorem OAI.MaxCutGames.Foundations.Repetition.selectedRightProfileError_le line 623
  42. def OAI.MaxCutGames.Foundations.Repetition.selectedSamplingTarget line 637
  43. theorem OAI.MaxCutGames.Foundations.Repetition.selectedSamplingTarget_left_error line 645
  44. theorem OAI.MaxCutGames.Foundations.Repetition.selectedSamplingTarget_right_error line 658
  45. theorem OAI.MaxCutGames.Foundations.Repetition.pushforward_snd_weight_eq_secondMarginal line 684
  46. def OAI.MaxCutGames.Foundations.Repetition.revealDataSplitEquiv line 694
  47. theorem OAI.MaxCutGames.Foundations.Repetition.partialRevealMarginal_secondMarginal line 711
  48. def OAI.MaxCutGames.Foundations.Repetition.selectedObservationDataEquiv line 731
  49. theorem OAI.MaxCutGames.Foundations.Repetition.selectedFullReveal_secondMarginal line 740
  50. theorem OAI.MaxCutGames.Foundations.Repetition.selectedRawMarginal_secondMarginal line 754
  51. theorem OAI.MaxCutGames.Foundations.Repetition.selectedCommonLaw_secondMarginal line 778

    Source documentation

    The exact marginal identification needed to use the conditioned-question information bound in the two local common-data profile errors.

    theorem selectedCommonLaw_secondMarginal (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)
    (j : {i : Fin n // i ∉ selected}) :
    secondMarginal (selectedCommonLaw G strategy selected positive j).weight =
      (selectedQuestionMarginal G strategy selected positive j.1).weight := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.selectedCommonLaw, OAI.MaxCutGames.Foundations.Repetition.selectedQuestionMarginal

  52. theorem OAI.MaxCutGames.Foundations.Repetition.selectedCommonLaw_questions_pushforward line 789