OAI/Computability/UniqueGames/Decoding/MatrixCoordinates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.domainCoordinates line 24
  2. def OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.changeDomain line 29
  3. def OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.mapEquiv line 39
  4. theorem OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.mapEquiv_apply line 44
  5. theorem OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.mapEquiv_symm_apply line 49
  6. def OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.functionalEquiv line 54
  7. theorem OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.functionalEquiv_apply line 58
  8. theorem OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.mapEquiv_rankOne line 63
  9. theorem OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.mapEquiv_symm_add_rankOne line 69
  10. def OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.coordinateTau line 77
  11. theorem OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.functionalEquiv_tau line 80
  12. theorem OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.mapEquiv_symm_firstBit_shift line 87
  13. theorem OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.affine_evaluation line 95
  14. theorem OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.mapEquiv_rowAdvice line 105
  15. theorem OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.indicator_congr line 114
  16. theorem OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.shortcodeAcceptance_eq line 121

    Source documentation

    Coordinate change preserves the complete uniform matrix equality test.

    theorem shortcodeAcceptance_eq (k ell : ℕ)
    (f : (ActualHomogeneous.E k →ₗ[F2] (Fin ell → F2)) → (Fin ell → F2)) :
    SurrogateFibers.shortcodeAcceptance f =
      Inverse.Shortcode.equalityAcceptance (fun M => f ((mapEquiv k ell).symm M)) := by
…

    Mentions: OAI.UniqueGamesTheorem.Decoder.SurrogateFibers.shortcodeAcceptance, OAI.UniqueGamesTheorem.Inverse.Shortcode.equalityAcceptance, OAI.UniqueGamesTheorem.Decoder.MatrixCoordinates.mapEquiv