OAI/Computability/UniqueGames/Reduction/FromMatrixGap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.FromMatrixGap.reduction line 22

   Source documentation

   Choose the parity error only after the matrix tuple length is fixed, then compose the actual raw-input, matrix-test, and final graph machines.

   def reduction {ε δ : ℝ} (P : ParameterSelection.OuterParameters ε δ)
       (M : Decoder.MatrixGap.Parameters P.pStar) :
       MachineOutputContract.BinaryGapReduction ε δ := by
   …

   Mentions: OAI.UniqueGamesTheorem.ParameterSelection.OuterParameters, OAI.UniqueGamesTheorem.Decoder.MatrixGap.Parameters