OAI/Computability/MaxCut/Encoding/ActualInputRows.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Soundness.ActualInputRows.restrictedFirst line 18
2. def OAI.MaxCutGames.Soundness.ActualInputRows.firstMap line 24
3. theorem OAI.MaxCutGames.Soundness.ActualInputRows.firstMap_eq line 29
4. def OAI.MaxCutGames.Soundness.ActualInputRows.restrictedSecond line 38
5. def OAI.MaxCutGames.Soundness.ActualInputRows.secondMap line 44
6. theorem OAI.MaxCutGames.Soundness.ActualInputRows.secondMap_eq line 49
7. theorem OAI.MaxCutGames.Soundness.ActualInputRows.firstMap_actual line 60

   Source documentation

   The first player's extraction on the actual sampled input equals Y π. There is no assumption that an arbitrary input row is linear.

   theorem firstMap_actual [Fintype Q] [DecidableEq Q]
       (J : Finset (Fin k)) (rhs : Id → Bool) (occ : Fin k → Id)
       (slot : Fin k → PartnerProjection.Slot) (Y : RawPoint J →ₗ[F2] (Q → F2)) :
       firstMap rhs (actualFirst J (rowCoefficients J (gammaOfRawMap J Y))
         (fun j => (occ j, ConcreteExtraction.slotIndex (slot j)))) =
         Y.comp (rawProjection (fun j => rhs (occ j)) J slot) := by
   …

   Mentions: OAI.MaxCutGames.Soundness.PartnerProjection.Slot, OAI.MaxCutGames.Soundness.ActualInputRows.firstMap, OAI.MaxCutGames.Soundness.ConcreteExtraction.slotIndex

8. theorem OAI.MaxCutGames.Soundness.ActualInputRows.secondMap_actual line 80

   Source documentation

   The second player's extraction equals the genuine supplied raw target map.

   theorem secondMap_actual [Fintype Q] [DecidableEq Q]
       (J : Finset (Fin k)) (names : Id → Fin 3 → Name) (draw : Draw (Fin k) Id)
       (Y : RawPoint J →ₗ[F2] (Q → F2)) :
       secondMap J (actualSecond J names (rowCoefficients J (gammaOfRawMap J Y)) draw) = Y := by
   …

   Mentions: OAI.MaxCutGames.Soundness.ActualInputRows.secondMap