OAI/Computability/UniqueGames/Gadgets/QuadraticStageNoise.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Gadget.QuadraticStageNoise.rate line 30
  2. theorem OAI.UniqueGamesTheorem.Gadget.QuadraticStageNoise.actual_kernel line 33
  3. def OAI.UniqueGamesTheorem.Gadget.QuadraticStageNoise.stage line 41

    Source documentation

    The actual recursive spaces, shifts, outputs and finite leaf-noise sampler.

    noncomputable def stage (n : ℕ) : Stage (ZMod 2) (Vec F) :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage

  4. theorem OAI.UniqueGamesTheorem.Gadget.QuadraticStageNoise.stage_error line 44
  5. def OAI.UniqueGamesTheorem.Gadget.QuadraticStageNoise.quotientStage line 53

    Source documentation

    The logical alphabet is an actual injected shift subspace after quotient.

    noncomputable def quotientStage (n : ℕ) : Stage (ZMod 2) (Vec F) :=
…

    Mentions: OAI.UniqueGamesTheorem.Gadget.Stage

  6. theorem OAI.UniqueGamesTheorem.Gadget.QuadraticStageNoise.quotientStage_error line 56