OAI/Computability/UniqueGames/Foundations/FiniteTrialsLemmas.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

Exact finite probability mass of a bounded rejection process.

Each trial independently draws from a finite mass function w. Its first accepted proposal is represented by some proposal; exhaustion is none. The recursive definition exposes the one-step probability transition. We prove normalization, nonnegativity, the exact survival probability, and an exact agreement-event formula with the finite-truncation error.

  1. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.eventMass line 31
  2. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.eventMass_nonneg line 34
  3. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.eventMass_complement line 40
  4. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.geometricMass line 52
  5. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.geometricMass_nonneg line 56
  6. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.geometricMass_identity line 62
  7. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.firstHitWeight line 76

    Source documentation

    Probability transition for a finite first-acceptance process. A successful first trial contributes its own mass; a rejected first trial continues with one fewer trial.

    def firstHitWeight (w : σ → ℝ) (accept : σ → Bool) : Nat → Option σ → ℝ
  | 0, none => 1
  | 0, some _ => 0
  | n + 1, none => eventMass w (fun s => !(accept s)) * firstHitWeight w accept n none
  | n + 1, some s =>
      (if accept s then w s else 0) +
        eventMass w (fun s => !(accept s)) * firstHitWeight w accept n (some s)

    Mentions: OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.eventMass

  8. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.firstHitWeight_nonneg line 84
  9. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.firstHitWeight_none line 98
  10. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.firstHitWeight_some line 104
  11. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.firstHitWeight_normalized line 114
  12. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodFirstMass line 130

    Source documentation

    Probability that the first accepted proposal satisfies an additional test. For two threshold samplers, take accept = left || right and good = left && right. first_union_common gives deterministic agreement on this event.

    def goodFirstMass (w : σ → ℝ) (accept good : σ → Bool) (n : Nat) : ℝ :=
…
  13. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodFirstMass_eq line 133
  14. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodFirstMass_exact line 147

    Source documentation

    Exact finite geometric law: the first accepted proposal lies in the good part with probability (good accepted mass / total accepted mass) times the probability of seeing any accepted proposal within the trial bound.

    theorem goodFirstMass_exact (w : σ → ℝ) (accept good : σ → Bool)
    (hw : ∑ s, w s = 1) (ha : eventMass w accept ≠ 0) (n : Nat) :
    goodFirstMass w accept good n =
      eventMass w (fun s => accept s && good s) / eventMass w accept *
        (1 - eventMass w (fun s => !(accept s)) ^ n) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.eventMass, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodFirstMass

  15. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.commonMass_le_acceptMass line 163
  16. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodFirstMass_lower_bound line 173

    Source documentation

    A finite truncation loses at most its exhaustion probability in addition to the conditional bad-first-proposal probability. All quantities are exact finite sums; the rightmost term is the explicit geometric tail.

    theorem goodFirstMass_lower_bound (w : σ → ℝ) (accept good : σ → Bool)
    (hw : ∀ s, 0 ≤ w s) (hw_sum : ∑ s, w s = 1)
    (ha : 0 < eventMass w accept) (n : Nat) :
    eventMass w (fun s => accept s && good s) / eventMass w accept -
        eventMass w (fun s => !(accept s)) ^ n ≤ goodFirstMass w accept good n := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.eventMass, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodFirstMass

  17. structure OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.ThresholdInterval line 202
  18. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.splitPoint line 207
  19. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.splitLeft line 209
  20. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.splitRight line 212
  21. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.cutAt line 215
  22. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.intervalCDF line 217
  23. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.split_cdf line 219
  24. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.accepted_interval_mass line 224
  25. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.splitLeft_cut line 232
  26. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.splitRight_cut line 237
  27. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.splitLeft_preserves_cut line 245
  28. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.splitRight_preserves_cut line 251
  29. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.splitAll line 257
  30. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.unitThresholdInterval line 261
  31. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.thresholdPartition line 263
  32. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.sumOnIntervals line 267
  33. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.sumOn_splitAll line 271
  34. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.partition_sum line 281
  35. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.partition_total_mass line 290
  36. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.partition_cdf line 296
  37. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.splitAll_new_cuts line 301
  38. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.splitAll_preserves_cuts line 313
  39. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.partition_cuts line 327
  40. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.sumOnIntervals_congr line 337
  41. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.partition_acceptance_mass line 347
  42. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.sum_interval_get line 357
  43. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.traceAverage line 387

    Source documentation

    Expectation over a length-n list of independent proposals with mass w. This is defined directly as a finite nested weighted sum.

    def traceAverage (w : σ → ℝ) : Nat → (List σ → ℝ) → ℝ
  | 0, observable => observable []
  | n + 1, observable => ∑ s, w s * traceAverage w n (fun tail => observable (s :: tail))
  44. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.traceAverage_const line 391
  45. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.traceAverage_mono line 397
  46. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.traceAverage_sum line 409
  47. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.firstAccepted_law line 423

    Source documentation

    The recursively constructed first-hit distribution is the actual law of the finite shared-list rejection sampler.

    theorem firstAccepted_law (w : σ → ℝ) (accept : σ → Bool)
    (hw : ∑ s, w s = 1) (n : Nat) (output : Option σ) :
    traceAverage w n (fun proposals =>
      if firstAccepted accept proposals = output then 1 else 0) =
      firstHitWeight w accept n output := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.traceAverage, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.firstAccepted, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.firstHitWeight

  48. def OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodFirstIndicator line 470

    Source documentation

    Indicator of the first accepted proposal passing a second test.

    def goodFirstIndicator (accept good : σ → Bool) (proposals : List σ) : ℝ :=
…
  49. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodFirstIndicator_expansion line 475
  50. theorem OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodFirstIndicator_law line 492

    Source documentation

    Exact good-event probability of the actual bounded sampler.

    theorem goodFirstIndicator_law (w : σ → ℝ) (accept good : σ → Bool)
    (hw : ∑ s, w s = 1) (n : Nat) :
    traceAverage w n (goodFirstIndicator accept good) = goodFirstMass w accept good n := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.traceAverage, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodFirstIndicator, OAI.UniqueGamesTheorem.Foundations.CorrelatedSampling.goodFirstMass

  51. structure OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution line 529
  52. def OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.expectation line 538
  53. def OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability line 541
  54. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_nonnegative line 544
  55. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_le_one line 552
  56. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_true line 561
  57. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_false line 565
  58. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_mono line 569
  59. def OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.pushforward line 582

    Source documentation

    Pushforward counts all preimages, including collisions.

    def pushforward (μ : FiniteDistribution Ω) (f : Ω → Γ) : FiniteDistribution Γ := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution

  60. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_pushforward line 594
  61. def OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.transport line 606
  62. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_transport line 611
  63. def OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.iid line 618

    Source documentation

    Independent repeated sampling, including the single empty tuple at n=0.

    def iid (μ : FiniteDistribution Ω) (n : Nat) : FiniteDistribution (Fin n → Ω) where
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution

  64. theorem OAI.UniqueGamesTheorem.Foundations.Games.FiniteDistribution.probability_iid_all line 623
  65. abbrev OAI.UniqueGamesTheorem.Foundations.Games.Strategy line 642
  66. structure OAI.UniqueGamesTheorem.Foundations.Games.Game line 644
  67. def OAI.UniqueGamesTheorem.Foundations.Games.Game.wins line 654
  68. def OAI.UniqueGamesTheorem.Foundations.Games.Game.success line 658
  69. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.success_nonnegative line 661
  70. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.success_le_one line 665
  71. def OAI.UniqueGamesTheorem.Foundations.Games.Game.simulatedStrategy line 672

    Source documentation

    Local question reconstruction and answer decoding never expose the other player's question to a strategy. Any fixed advice is an ordinary fixed parameter of these functions.

    def simulatedStrategy {R₁ R₂ B₁ B₂ : Type*}
    (questionMap₁ : Q₁ → R₁) (questionMap₂ : Q₂ → R₂)
    (answerMap₁ : Q₁ → B₁ → A₁) (answerMap₂ : Q₂ → B₂ → A₂)
    (strategy : Strategy R₁ R₂ B₁ B₂) : Strategy Q₁ Q₂ A₁ A₂ :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Strategy

  72. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.success_le_of_localSimulation line 681

    Source documentation

    An acceptance implication under an exact question-law pushforward gives an actual success-probability comparison for every pair of local strategies.

    theorem success_le_of_localSimulation {R₁ R₂ B₁ B₂ : Type*}
    [Fintype R₁] [Fintype R₂] [Fintype B₁] [Fintype B₂]
    (G : Game Q₁ Q₂ A₁ A₂) (H : Game R₁ R₂ B₁ B₂)
    (questionMap₁ : Q₁ → R₁) (questionMap₂ : Q₂ → R₂)
    (answerMap₁ : Q₁ → B₁ → A₁) (answerMap₂ : Q₂ → B₂ → A₂)
    (questionLaw : H.questions =
      G.questions.pushforward (fun q => (questionMap₁ q.1, questionMap₂ q.2)))
    (acceptance : ∀ x y a b,
      H.accepts (questionMap₁ x) (questionMap₂ y) a b = true →
      G.accepts x y (answerMap₁ x a) (answerMap₂ y b) = true)
    (strategy : Strategy R₁ R₂ B₁ B₂) :
    H.success strategy ≤
…

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

  73. def OAI.UniqueGamesTheorem.Foundations.Games.Game.tupleQuestionEquiv line 700
  74. def OAI.UniqueGamesTheorem.Foundations.Games.Game.repetition line 708

    Source documentation

    Parallel repetition retains arbitrary dependence on each full local tuple.

    def repetition (G : Game Q₁ Q₂ A₁ A₂) (n : Nat) :
    Game (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂) := by
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Game

  75. def OAI.UniqueGamesTheorem.Foundations.Games.Game.repeatStrategy line 717

    Source documentation

    Playing a fixed base strategy separately in each coordinate is one permitted repeated strategy, though repeated strategies are more general.

    def repeatStrategy (strategy : Strategy Q₁ Q₂ A₁ A₂) (n : Nat) :
    Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂) :=
…

    Mentions: OAI.UniqueGamesTheorem.Foundations.Games.Strategy

  76. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.success_repeatStrategy line 721
  77. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.repetition_question_weight line 729
  78. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.repetition_accepts_iff line 734
  79. def OAI.UniqueGamesTheorem.Foundations.Games.Game.coordinateWin line 742

    Source documentation

    One coordinate's success may depend on the entire local question tuples.

    def coordinateWin (G : Game Q₁ Q₂ A₁ A₂) {n : Nat}
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    (coordinate : Fin n) (questions : (Fin n → Q₁) × (Fin n → Q₂)) : Bool :=
…

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

  80. def OAI.UniqueGamesTheorem.Foundations.Games.Game.selectedWins line 748
  81. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.selectedWins_mono line 754
  82. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.selectedWins_empty line 765
  83. theorem OAI.UniqueGamesTheorem.Foundations.Games.Game.selectedWins_univ line 771