OAI/Computability/MaxCut/PCP/SelectionSequence.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Quantitative parallel repetition for actual finite two-player games. The coordinate bound is derived from the explicitly conditioned question law, finite reveal «variables», information estimates, shared rejection sampler, and normalized local completions. The scalar recurrence is then applied to the actual repeated strategy's success probability.

  1. theorem OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.exists_unused_inline_SelectionSequence line 10
  2. def OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.nextSet line 27

    Source documentation

    Insert a chosen unused coordinate while there are coordinates remaining.

    noncomputable def nextSet {n : Nat}
    (Step : Finset (Fin n) → Fin n → Prop)
    (witness : ∀ S, S.card < n → ∃ j, j ∉ S ∧ Step S j)
    (S : Finset (Fin n)) : Finset (Fin n) :=
…
  3. def OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.selectedSet line 34

    Source documentation

    A total sequence, constant after all n coordinates have been selected.

    noncomputable def selectedSet {n : Nat}
    (Step : Finset (Fin n) → Fin n → Prop)
    (witness : ∀ S, S.card < n → ∃ j, j ∉ S ∧ Step S j) : Nat → Finset (Fin n)
  | 0 => ∅
  | m + 1 => nextSet Step witness (selectedSet Step witness m)

    Mentions: OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.nextSet

  4. theorem OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.selectedSet_card line 40
  5. theorem OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.selectedSet_subset_succ line 63
  6. theorem OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.selectedSet_monotone line 73
  7. theorem OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.selectedSet_univ line 79
  8. theorem OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.selectedSet_step line 86
  9. def OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.SetStep line 102

    Source documentation

    The multiplicative scalar inequality for one actual selected-set update.

    def SetStep {n : Nat} (P : Finset (Fin n) → ℝ) (v ell : ℝ)
    (S : Finset (Fin n)) (j : Fin n) : Prop :=
…
  10. theorem OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.totalSetStep line 109

    Source documentation

    At zero success, any unused coordinate is safe and no conditioning occurs.

    theorem totalSetStep {n : Nat} (P : Finset (Fin n) → ℝ) (v ell : ℝ)
    (hnonneg : ∀ S, 0 ≤ P S) (hanti : Antitone P)
    (hpositive : ∀ S, S.card < n → 0 < P S →
      ∃ j, j ∉ S ∧ SetStep P v ell S j) :
    ∀ S, S.card < n → ∃ j, j ∉ S ∧ SetStep P v ell S j := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.SetStep

  11. theorem OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.exists_scalar_sequence line 125

    Source documentation

    Construct the scalar sequence from actual selected-set probabilities.

    theorem exists_scalar_sequence {n : Nat} (P : Finset (Fin n) → ℝ) (v ell : ℝ)
    (hempty : P ∅ = 1) (hnonneg : ∀ S, 0 ≤ P S) (hanti : Antitone P)
    (hpositive : ∀ S, S.card < n → 0 < P S →
      ∃ j, j ∉ S ∧ SetStep P v ell S j) :
    ∃ p : Nat → ℝ, p 0 = 1 ∧ (∀ m, 0 ≤ p m) ∧ Antitone p ∧
      ScalarRecurrence p n v ell ∧ p n = P Finset.univ := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.SetStep, OAI.MaxCutGames.Foundations.Repetition.ScalarRecurrence

  12. def OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.ConditionalCoordinateBound line 158
  13. theorem OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.repetition_success_le_of_conditionalCoordinateBound line 172

    Source documentation

    Apply the proved scalar estimate to the success of an actual repeated-game strategy. The conditional-coordinate bound is the sole game-theoretic premise.

    theorem repetition_success_le_of_conditionalCoordinateBound
    (G : Game Q₁ Q₂ A₁ A₂) (n : Nat)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    {v ell : ℝ} (hvalue : G.value ≤ v) (hv1 : v < 1) (hell : 1 ≤ ell)
    (hcoordinate : ConditionalCoordinateBound G n strategy ell) :
    (G.repetition n).success strategy ≤
      (1 - (1 - v)^3 / 6000)^((n : ℝ) / ell) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.SelectionSequence.ConditionalCoordinateBound

  14. theorem OAI.MaxCutGames.Foundations.Repetition.selected_coordinate_probability_le_value_add_error line 214
  15. theorem OAI.MaxCutGames.Foundations.Repetition.holenstein_conditionalCoordinateBound line 243
  16. theorem OAI.MaxCutGames.Foundations.Repetition.holenstein_repetition_success line 259

    Source documentation

    Holenstein's explicit constant-6000 repetition estimate, for the actual success probability of every finite deterministic repeated strategy.

    theorem holenstein_repetition_success
    (G : Game Q₁ Q₂ A₁ A₂) (n : Nat)
    (strategy : Strategy (Fin n → Q₁) (Fin n → Q₂) (Fin n → A₁) (Fin n → A₂))
    {v ell : ℝ} (hvalue : G.value ≤ v) (hv : v < 1) (hell : 1 ≤ ell)
    (halphabet : logTwo ((Fintype.card A₁ : ℝ) * (Fintype.card A₂ : ℝ)) ≤ ell) :
    (G.repetition n).success strategy ≤
      (1 - (1 - v)^3 / 6000)^((n : ℝ) / ell) :=
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.logTwo

  17. theorem OAI.MaxCutGames.Foundations.Repetition.holenstein_repetition_value line 271

    Source documentation

    Quantitative parallel repetition of the actual maximum game value. There is no repetition, embedding, information-budget, or independence premise.

    theorem holenstein_repetition_value
    (G : Game Q₁ Q₂ A₁ A₂) (n : Nat)
    {v ell : ℝ} (hvalue : G.value ≤ v) (hv : v < 1) (hell : 1 ≤ ell)
    (halphabet : logTwo ((Fintype.card A₁ : ℝ) * (Fintype.card A₂ : ℝ)) ≤ ell) :
    (G.repetition n).value ≤
      (1 - (1 - v)^3 / 6000)^((n : ℝ) / ell) := by
…

    Mentions: OAI.MaxCutGames.Foundations.Repetition.logTwo