OAI/Computability/UniqueGames/Games/PartialRevealLemmas.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Removing one independent reveal from the explicit product law. The likelihood can be any function of the questions and outside data.

  1. def OAI.UniqueGamesTheorem.Foundations.Repetition.mergeAt line 18
  2. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.mergeAt_self line 22
  3. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.mergeAt_other line 26
  4. def OAI.UniqueGamesTheorem.Foundations.Repetition.partialRevealWeight line 30
  5. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.product_reveal_at line 34
  6. def OAI.UniqueGamesTheorem.Foundations.Repetition.partialRevealMarginal line 44
  7. def OAI.UniqueGamesTheorem.Foundations.Repetition.fullRevealMarginal line 51
  8. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.fullRevealMarginal_merge line 59
  9. def OAI.UniqueGamesTheorem.Foundations.Repetition.fullRevealModel line 85
  10. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.fullRevealModel_merge line 92
  11. def OAI.UniqueGamesTheorem.Foundations.Repetition.revealSplitEquiv line 100
  12. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.totalVariation_comp_equiv line 122
  13. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.fullReveal_totalVariation line 132

    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.UniqueGamesTheorem.Foundations.Games.FiniteDistribution, OAI.UniqueGamesTheorem.Foundations.Information.totalVariation, OAI.UniqueGamesTheorem.Foundations.Repetition.fullRevealMarginal, OAI.UniqueGamesTheorem.Foundations.Repetition.fullRevealModel, OAI.UniqueGamesTheorem.Foundations.Repetition.maskedJoint, OAI.UniqueGamesTheorem.Foundations.Repetition.partialRevealMarginal, OAI.UniqueGamesTheorem.Foundations.Repetition.maskedModel

  14. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.leftReveal_full_error line 147
  15. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.rightReveal_full_error line 156
  16. def OAI.UniqueGamesTheorem.Foundations.Repetition.revealLeftFactor line 181
  17. def OAI.UniqueGamesTheorem.Foundations.Repetition.revealRightFactor line 186
  18. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealLeftFactor_nonnegative line 192
  19. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealRightFactor_nonnegative line 199
  20. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.revealLaw_factorization line 205
  21. def OAI.UniqueGamesTheorem.Foundations.Repetition.partialLeftFactor line 220
  22. def OAI.UniqueGamesTheorem.Foundations.Repetition.partialRightFactor line 224
  23. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.partialRevealWeight_factorization line 228
  24. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRawMarginal line 258
  25. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedPosterior_eq_raw line 266
  26. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRawMarginal_firstMarginal line 294
  27. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRawMarginal_isProbability line 305
  28. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_raw_information_bound line 323
  29. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedOutsideLikelihood line 338
  30. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedObservationEquiv line 346
  31. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRawMarginal_fullReveal line 356
  32. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedRawReference_fullReveal line 373
  33. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_raw_error_eq_fullReveal line 389
  34. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_fullReveal_information_bound line 403
  35. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedInformationRadius line 417
  36. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_leftReveal_error_sum line 424
  37. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_rightReveal_error_sum line 447
  38. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLabels_card line 490
  39. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.unusedCoordinates_card line 495
  40. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.unusedCoordinates_card_real line 500
  41. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.log_le_logTwo line 505
  42. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedLabels_log_le line 515
  43. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selectedInformationRadius_le line 530

    Source documentation

    The actual selected-label radius is bounded by the base-two alphabet budget. The unused-coordinate factor is a real subtraction, as in the scalar recurrence.

    theorem selectedInformationRadius_le [Nonempty A₁] [Nonempty A₂]
    (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)
    (ell : ℝ)
    (hell : logTwo ((Fintype.card A₁ : ℝ) * (Fintype.card A₂ : ℝ)) ≤ ell) :
    selectedInformationRadius G strategy selected ≤
      Real.sqrt (((n : ℝ) - selected.card) *
        ((selected.card : ℝ) * ell + logTwo (1 / G.selectedSuccess strategy selected))) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.logTwo, OAI.UniqueGamesTheorem.Foundations.Repetition.selectedInformationRadius

  44. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.sqrt_budget_factor line 549
  45. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.exists_coordinate_le_information_budget line 559

    Source documentation

    An actual finite average over all unused coordinates yields the numerical bound needed by the selected-success recurrence. No sign condition on the individual errors is required.

    theorem exists_coordinate_le_information_budget [Nonempty A₁] [Nonempty A₂]
    (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)
    (ell : ℝ)
    (hell : logTwo ((Fintype.card A₁ : ℝ) * (Fintype.card A₂ : ℝ)) ≤ ell)
    (hselected : selected.card < n)
    (error : {i : Fin n // i ∉ selected} → ℝ)
    (hsum : (∑ j, error j) ≤ 15 * selectedInformationRadius G strategy selected) :
    ∃ j : {i : Fin n // i ∉ selected}, error j ≤ 15 * Real.sqrt
      (((selected.card : ℝ) * ell + logTwo (1 / G.selectedSuccess strategy selected)) /
        ((n : ℝ) - selected.card)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Repetition.logTwo, OAI.UniqueGamesTheorem.Foundations.Repetition.selectedInformationRadius

  46. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.isProbability_comp_equiv line 605
  47. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.partialRevealMarginal_isProbability line 614
  48. abbrev OAI.UniqueGamesTheorem.Foundations.Repetition.SelectedCommonData line 635
  49. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.selected_fullReveal_isProbability line 640
  50. def OAI.UniqueGamesTheorem.Foundations.Repetition.selectedCommonLaw line 657
  51. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.firstMarginal_totalVariation_le line 682
  52. def OAI.UniqueGamesTheorem.Foundations.Repetition.leftCommonMarginal line 691
  53. def OAI.UniqueGamesTheorem.Foundations.Repetition.leftCommonProfile line 694
  54. def OAI.UniqueGamesTheorem.Foundations.Repetition.swapSeedLeft line 697
  55. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.leftCommonMarginal_isProbability line 703
  56. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.leftCommonProfile_isProbability line 708
  57. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.leftCommonProfile_error line 713
  58. def OAI.UniqueGamesTheorem.Foundations.Repetition.swapQuestionEndpoints line 763
  59. def OAI.UniqueGamesTheorem.Foundations.Repetition.rightCommonMarginal line 769
  60. def OAI.UniqueGamesTheorem.Foundations.Repetition.rightCommonProfile line 772
  61. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.rightCommonProfile_isProbability line 775
  62. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.swap_question_pushforward_snd line 781
  63. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.leftRevealModel_swap line 787
  64. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.rightCommonProfile_error line 797