OAI/Computability/UniqueGames/Decoding/NativeExperiment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Clean.NativeExperiment.expectation_transport line 18
2. theorem OAI.UniqueGamesTheorem.Clean.NativeExperiment.iid_product_split line 24
3. theorem OAI.UniqueGamesTheorem.Clean.NativeExperiment.expectation_iid_product line 34
4. def OAI.UniqueGamesTheorem.Clean.NativeExperiment.maskSet line 48
5. abbrev OAI.UniqueGamesTheorem.Clean.NativeExperiment.MaskStrategy line 51
6. def OAI.UniqueGamesTheorem.Clean.NativeExperiment.liftStrategy line 55
7. def OAI.UniqueGamesTheorem.Clean.NativeExperiment.success line 61

   Source documentation

   The actual law: independent singleton choices followed by one independent uniform coefficient at the intercept and each surviving partner coordinate.

   def success (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
       (g : IncidenceExtraction.Incidence O N)
       (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
       (strategy : MaskStrategy k R O N) : ℝ :=
   …

   Mentions: OAI.UniqueGamesTheorem.Clean.NativeExperiment.MaskStrategy

8. theorem OAI.UniqueGamesTheorem.Clean.NativeExperiment.success_eq_flat line 70