OAI/Computability/UniqueGames/Reduction/BinaryLinear.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Exact transport from XOR bit vectors to vector spaces over ZMod 2.

  1. def OAI.UniqueGamesTheorem.Integration.BinaryLinear.ofBit line 15
  2. def OAI.UniqueGamesTheorem.Integration.BinaryLinear.toBit line 16
  3. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.scalar_cases line 18
  4. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.ofBit_toBit line 19
  5. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.toBit_ofBit line 20
  6. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.ofBit_xor line 21
  7. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.toBit_add line 22
  8. def OAI.UniqueGamesTheorem.Integration.BinaryLinear.toVector line 24
  9. def OAI.UniqueGamesTheorem.Integration.BinaryLinear.fromVector line 25
  10. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.toVector_fromVector line 27
  11. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.fromVector_toVector line 31
  12. def OAI.UniqueGamesTheorem.Integration.BinaryLinear.coordinatesEquiv line 35
  13. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.toVector_xor line 41
  14. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.fromVector_add line 46
  15. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.toVector_zero line 50
  16. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.fromVector_zero line 55
  17. def OAI.UniqueGamesTheorem.Integration.BinaryLinear.liftLinear line 59

    Source documentation

    A zero-preserving XOR-additive map becomes a genuine binary linear map.

    def liftLinear {n m : Nat} (f : BitVec n → BitVec m)
    (hzero : f 0 = 0) (hadd : ∀ x y, f (x ^^^ y) = f x ^^^ f y) :
    Vector n →ₗ[F2] Vector m where
…

    Mentions: OAI.UniqueGamesTheorem.Integration.BinaryLinear.Vector, OAI.UniqueGamesTheorem.Integration.BinaryLinear.F2

  18. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.liftLinear_apply line 70
  19. theorem OAI.UniqueGamesTheorem.Integration.BinaryLinear.finrank_vector line 75