OAI/Computability/UniqueGames/Reduction/FixedOutcomes.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.Parameter line 15
2. def OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.occurrenceTuples line 18
3. def OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.fixedParams line 23

   Source documentation

   Ambient linear map, noise occurrence index, scalar linear functional, in exactly the original nested enumeration order.

   def fixedParams (k s d : Nat) (indices : List N) : List (Parameter k s d N) :=
   …

   Mentions: OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.Parameter

4. def OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.assemble line 27
5. def OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.outcomeEquiv line 32

   Source documentation

   The reassociation changes only parentheses, not enumeration order.

   def outcomeEquiv (m k s d : Nat) (N : Type*) :
       (Query m k s d × (N × (E k →ₗ[F2] F2))) ≃
         ((Fin k → Fin m) × Parameter k s d N) :=
   …

   Mentions: OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.Parameter

6. theorem OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.pairs_associate line 37
7. theorem OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.indexedOutcomes_factor line 44
8. theorem OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.indexedOutcomes_reassociate line 51
9. theorem OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.occurrenceTuples_length line 58
10. theorem OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.fixedParams_length line 61
11. theorem OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.fixedParams_nonempty line 70
12. abbrev OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.CoefficientParameter line 77

    Source documentation

    A coefficient-only representation of each fixed linear-map parameter.

    abbrev CoefficientParameter (k s d : Nat) (N : Type*) :=
    …

13. def OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.coefficientValues line 80
14. def OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.fixedCoefficientParams line 84
15. def OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.fromCoefficientParameter line 89
16. theorem OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.fixedCoefficientParams_map line 95

    Source documentation

    The concrete coefficient enumeration produces precisely the fixed parameter list. No choice of maps or representatives is made by this constructor.

    theorem fixedCoefficientParams_map (k s d : Nat) (indices : List N) :
        (fixedCoefficientParams k s d indices).map fromCoefficientParameter =
          fixedParams k s d indices := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.fixedCoefficientParams, OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.fromCoefficientParameter, OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.fixedParams

17. theorem OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.fixedCoefficientParams_length line 102
18. def OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.tableParams line 107
19. theorem OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.tableParams_length line 111
20. theorem OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.outputInstance_constraints line 115
21. theorem OAI.UniqueGamesTheorem.Reduction.FixedOutcomes.tableOutput_constraints line 126