OAI/Computability/UniqueGames/Games/SelectionSequence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.exists_unused line 11
2. def OAI.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.nextSet line 28

   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.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.selectedSet line 35

   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.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.nextSet

4. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.selectedSet_card line 41
5. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.selectedSet_subset_succ line 64
6. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.selectedSet_monotone line 74
7. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.selectedSet_univ line 80
8. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.selectedSet_step line 87
9. def OAI.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.SetStep line 103

   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.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.totalSetStep line 110

    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.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.SetStep

11. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.exists_scalar_sequence line 126

    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.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.SetStep, OAI.UniqueGamesTheorem.Foundations.Repetition.ScalarRecurrence

12. def OAI.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.ConditionalCoordinateBound line 161
13. theorem OAI.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.repetition_success_le_of_conditionalCoordinateBound line 175

    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.UniqueGamesTheorem.Foundations.Repetition.SelectionSequence.ConditionalCoordinateBound