OAI/Computability/UniqueGames/Decoding/MatrixGapFromInverseLemmas.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The matrix reduction assembled from the gadget and decoder, conditional on the dimension-uniform shortcode inverse.

  1. theorem OAI.UniqueGamesTheorem.Decoder.MatrixGap.parameters_of_inverse line 22
  2. theorem OAI.UniqueGamesTheorem.Decoder.MatrixGap.exists_parameters line 77