OAI/Computability/UniqueGames/Foundations/SamplingLemmas.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Exact finite sampling laws used to identify verifier distributions with repeated game question laws. These are finite sum/product identities, not independence assumptions about an unspecified distribution.

  1. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.iid_pushforward line 25
  2. def OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.uniform line 45
  3. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.iid_uniform line 54
  4. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.expectation_uniform line 61
  5. def OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.reindexEquiv line 89
  6. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.pushforward_equiv line 95
  7. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.table_const_reindex line 113
  8. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.iid_reindex line 126
  9. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_reindex_of_weight line 138

    Source documentation

    Weighted finite change of variables; no independence hypothesis.

    theorem probability_reindex_of_weight {Ω Γ : Type*} [Fintype Ω] [Fintype Γ]
    (μ : FiniteDistribution Ω) (ν : FiniteDistribution Γ) (e : Ω ≃ Γ)
    (hweight : ∀ x, ν.weight (e x) = μ.weight x) (event : Γ → Bool) :
    ν.probability event = μ.probability (fun x => event (e x)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution

  10. def OAI.UniqueGamesTheorem.Foundations.Games.Game.questionReindexEquiv line 157
  11. def OAI.UniqueGamesTheorem.Foundations.Games.Game.reindexStrategy line 163

    Source documentation

    Each player only permutes that player's own questions and answers.

    def reindexStrategy {n m : Nat} (e : Fin m ≃ Fin n)
    (s : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂)) :
    Strategy (Fin m → Q₁) (Fin m → Q₂) (Fin m → A₁) (Fin m → A₂) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Strategy

  12. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.repetition_question_weight_reindex line 170

    Source documentation

    Simultaneous coordinate permutation preserves the actual joint question weight.

    theorem repetition_question_weight_reindex (G : Game Q₁ Q₂ A₁ A₂)
    {n m : Nat} (e : Fin m ≃ Fin n)
    (q : (Fin n → Q₁) × (Fin n → Q₂)) :
    (G.repetition m).questions.weight (questionReindexEquiv e q) =
      (G.repetition n).questions.weight q := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Game, OAI.UniqueGamesTheorem.Foundations.Games.Game.questionReindexEquiv

  13. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.repetition_questions_reindex line 181
  14. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.coordinateWin_reindex line 195

    Source documentation

    Coordinate successes transform pointwise; they are not assumed independent.

    theorem coordinateWin_reindex (G : Game Q₁ Q₂ A₁ A₂)
    {n m : Nat} (e : Fin m ≃ Fin n)
    (s : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (i : Fin m) (q : (Fin n → Q₁) × (Fin n → Q₂)) :
    G.coordinateWin (reindexStrategy e s) i (questionReindexEquiv e q) =
      G.coordinateWin s (e i) q := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Game, OAI.UniqueGamesTheorem.Foundations.Games.Strategy, OAI.UniqueGamesTheorem.Foundations.Games.Game.reindexStrategy, OAI.UniqueGamesTheorem.Foundations.Games.Game.questionReindexEquiv

  15. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.selectedWins_reindex line 213
  16. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.selectedSuccess_reindex line 234

    Source documentation

    The actual selected-success probability is invariant under the same relabeling.

    theorem selectedSuccess_reindex (G : Game Q₁ Q₂ A₁ A₂)
    {n m : Nat} (e : Fin m ≃ Fin n)
    (s : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (S : Finset (Fin m)) :
    G.selectedSuccess (reindexStrategy e s) S =
      G.selectedSuccess s (S.map e.toEmbedding) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Game, OAI.UniqueGamesTheorem.Foundations.Games.Strategy, OAI.UniqueGamesTheorem.Foundations.Games.Game.reindexStrategy

  17. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.repetition_success_reindex line 250

    Source documentation

    Full repetition success is a special case, including zero repetitions.

    theorem repetition_success_reindex (G : Game Q₁ Q₂ A₁ A₂)
    {n m : Nat} (e : Fin m ≃ Fin n)
    (s : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂)) :
    (G.repetition m).success (reindexStrategy e s) =
      (G.repetition n).success s := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Game, OAI.UniqueGamesTheorem.Foundations.Games.Strategy, OAI.UniqueGamesTheorem.Foundations.Games.Game.success, OAI.UniqueGamesTheorem.Foundations.Games.Game.reindexStrategy

  18. def OAI.UniqueGamesTheorem.Foundations.Information.IsProbability line 290
  19. def OAI.UniqueGamesTheorem.Foundations.Information.SupportedBy line 293
  20. def OAI.UniqueGamesTheorem.Foundations.Information.relativeEntropy line 295
  21. def OAI.UniqueGamesTheorem.Foundations.Information.totalVariation line 298
  22. def OAI.UniqueGamesTheorem.Foundations.Information.posterior line 301
  23. theorem OAI.UniqueGamesTheorem.Foundations.Information.posterior_isProbability line 304
  24. theorem OAI.UniqueGamesTheorem.Foundations.Information.posterior_supportedBy line 314
  25. theorem OAI.UniqueGamesTheorem.Foundations.Information.mul_log_div_ge_sub line 319
  26. theorem OAI.UniqueGamesTheorem.Foundations.Information.relativeEntropy_nonneg line 327
  27. theorem OAI.UniqueGamesTheorem.Foundations.Information.posterior_relativeEntropy_le line 339
  28. theorem OAI.UniqueGamesTheorem.Foundations.Information.totalVariation_nonneg line 363
  29. theorem OAI.UniqueGamesTheorem.Foundations.Information.totalVariation_symm line 366
  30. theorem OAI.UniqueGamesTheorem.Foundations.Information.totalVariation_le_one line 369
  31. theorem OAI.UniqueGamesTheorem.Foundations.Information.le_binaryLog_of_le_log line 380
  32. theorem OAI.UniqueGamesTheorem.Foundations.Information.weighted_sum_sq_le line 392

    Source documentation

    Finite weighted Cauchy–Schwarz for probability weights. The summands need not be nonnegative.

    theorem weighted_sum_sq_le (w x : α → ℝ) (hw : IsProbability w) :
    (∑ a, w a * x a)^2 ≤ ∑ a, w a * (x a)^2 := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Information.IsProbability

  33. def OAI.UniqueGamesTheorem.Foundations.Information.firstMarginal line 418
  34. def OAI.UniqueGamesTheorem.Foundations.Information.secondMarginal line 420
  35. def OAI.UniqueGamesTheorem.Foundations.Information.product line 422
  36. theorem OAI.UniqueGamesTheorem.Foundations.Information.firstMarginal_isProbability line 424
  37. theorem OAI.UniqueGamesTheorem.Foundations.Information.secondMarginal_isProbability line 431
  38. theorem OAI.UniqueGamesTheorem.Foundations.Information.product_isProbability line 440
  39. theorem OAI.UniqueGamesTheorem.Foundations.Information.point_le_firstMarginal line 447
  40. theorem OAI.UniqueGamesTheorem.Foundations.Information.point_le_secondMarginal line 452
  41. theorem OAI.UniqueGamesTheorem.Foundations.Information.joint_supportedBy_product_marginals line 457
  42. theorem OAI.UniqueGamesTheorem.Foundations.Information.relativeEntropy_product_reference line 465
  43. theorem OAI.UniqueGamesTheorem.Foundations.Information.marginal_relativeEntropy_sum_le line 499
  44. def OAI.UniqueGamesTheorem.Foundations.Information.conditionalKernel line 528
  45. theorem OAI.UniqueGamesTheorem.Foundations.Information.conditionalKernel_isProbability line 534
  46. theorem OAI.UniqueGamesTheorem.Foundations.Information.marginal_mul_conditionalKernel line 550
  47. theorem OAI.UniqueGamesTheorem.Foundations.Information.law_of_total_probability line 567
  48. theorem OAI.UniqueGamesTheorem.Foundations.Information.kernelProduct_isProbability line 574
  49. theorem OAI.UniqueGamesTheorem.Foundations.Information.alternativeInput_conditionalProduct_isProbability line 584
  50. theorem OAI.UniqueGamesTheorem.Foundations.Information.gameLaw_isProbability line 607
  51. def OAI.UniqueGamesTheorem.Foundations.Information.toGameLaw line 610
  52. def OAI.UniqueGamesTheorem.Foundations.Information.gameLawEquiv line 615
  53. theorem OAI.UniqueGamesTheorem.Foundations.Information.totalVariation_gameLaw line 621
  54. def OAI.UniqueGamesTheorem.Foundations.Information.gameConditionalKernel line 624
  55. theorem OAI.UniqueGamesTheorem.Foundations.Information.gameConditionalKernel_recombine line 630
  56. def OAI.UniqueGamesTheorem.Foundations.Information.gameConditionalProduct line 636
  57. theorem OAI.UniqueGamesTheorem.Foundations.Information.gameConditionalProduct_weight line 643
  58. theorem OAI.UniqueGamesTheorem.Foundations.Information.gameCondition_weight line 649
  59. theorem OAI.UniqueGamesTheorem.Foundations.Information.gameCondition_relativeEntropy_le line 656
  60. theorem OAI.UniqueGamesTheorem.Foundations.Information.totalVariation_joint_common_weights line 687
  61. theorem OAI.UniqueGamesTheorem.Foundations.Information.totalVariation_joint_common_kernel line 698
  62. theorem OAI.UniqueGamesTheorem.Foundations.Information.totalVariation_condition_le line 708
  63. theorem OAI.UniqueGamesTheorem.Foundations.Information.weighted_coordinate_sum_sq_le line 727
  64. theorem OAI.UniqueGamesTheorem.Foundations.Information.normalize_isProbability line 773
  65. theorem OAI.UniqueGamesTheorem.Foundations.Information.relativeEntropy_normalize_right line 781
  66. theorem OAI.UniqueGamesTheorem.Foundations.Information.neg_relativeEntropy_le_log_mass line 795
  67. theorem OAI.UniqueGamesTheorem.Foundations.Information.posterior_weighted_log_inverse_le line 808

    Source documentation

    Entropy budget for a finite posterior indexed by side information. The baseline masses b may have total mass B, rather than one. In the application, b(t,v)=P_T(t) and B is the number of possible side labels.

    theorem posterior_weighted_log_inverse_le (p b c : α → ℝ) (hp : IsProbability p)
    (hb : ∀ a, 0 ≤ b a) {z B : ℝ} (hz : 0 < z) (hB : 0 < B)
    (hmass : ∑ a, b a = B) (hpost : ∀ a, p a = b a * c a / z) :
    (∑ a, p a * Real.log (1 / c a)) ≤ Real.log (B / z) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Information.IsProbability