OAI/Computability/MaxCut/Encoding/MatrixCoordinates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Decoder.MatrixCoordinates.domainCoordinates line 20
2. def OAI.MaxCutGames.Decoder.MatrixCoordinates.changeDomain line 25
3. def OAI.MaxCutGames.Decoder.MatrixCoordinates.mapEquiv line 35
4. theorem OAI.MaxCutGames.Decoder.MatrixCoordinates.mapEquiv_apply line 40
5. theorem OAI.MaxCutGames.Decoder.MatrixCoordinates.mapEquiv_symm_apply line 45
6. def OAI.MaxCutGames.Decoder.MatrixCoordinates.functionalEquiv line 50
7. theorem OAI.MaxCutGames.Decoder.MatrixCoordinates.functionalEquiv_apply line 54
8. theorem OAI.MaxCutGames.Decoder.MatrixCoordinates.mapEquiv_rankOne line 59
9. theorem OAI.MaxCutGames.Decoder.MatrixCoordinates.mapEquiv_symm_add_rankOne line 65
10. def OAI.MaxCutGames.Decoder.MatrixCoordinates.coordinateTau line 73
11. theorem OAI.MaxCutGames.Decoder.MatrixCoordinates.functionalEquiv_tau line 76
12. theorem OAI.MaxCutGames.Decoder.MatrixCoordinates.mapEquiv_symm_firstBit_shift line 83
13. theorem OAI.MaxCutGames.Decoder.MatrixCoordinates.affine_evaluation line 91
14. theorem OAI.MaxCutGames.Decoder.MatrixCoordinates.mapEquiv_rowAdvice line 101
15. theorem OAI.MaxCutGames.Decoder.MatrixCoordinates.indicator_congr_inline_MatrixCoordinates line 110
16. theorem OAI.MaxCutGames.Decoder.MatrixCoordinates.shortcodeAcceptance_eq line 117

    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.MaxCutGames.Decoder.SurrogateFibers.shortcodeAcceptance, OAI.MaxCutGames.Inverse.Shortcode.equalityAcceptance, OAI.MaxCutGames.Decoder.MatrixCoordinates.mapEquiv