OAI/Computability/UniqueGames/Gadgets/Final.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Gadget.exists_actual_gadget line 19

   Source documentation

   Actual finite gadget data, with a rank threshold independent of the final logical dimension and an arbitrarily small nonlinear change probability.

   theorem exists_actual_gadget (p : ℚ) (hp : 0 < p) :
       ∃ r : ℕ, 1 ≤ r ∧ ∀ ℓ : ℕ, r ≤ ℓ →
         ∃ g : UniqueGamesTheorem.Gadget.ActualGadget.Data (Vector ℓ),
           UniqueGamesTheorem.Gadget.ActualGadget.Satisfies g p (7 / 8) r := by
   …

   Mentions: OAI.UniqueGamesTheorem.Gadget.ActualGadget.Data, OAI.UniqueGamesTheorem.Gadget.ActualGadget.Satisfies

2. theorem OAI.UniqueGamesTheorem.Gadget.exists_split_gadget line 68