OAI/Computability/UniqueGames/Reduction/ActualSourceLemmas.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.UniqueGamesTheorem.Reduction.ActualSource.Source line 17
2. def OAI.UniqueGamesTheorem.Reduction.ActualSource.Source.sourceList line 23
3. def OAI.UniqueGamesTheorem.Reduction.ActualSource.Source.ofList line 27

   Source documentation

   Retain every list position as its own occurrence identifier.

   def Source.ofList {n : Nat} (es : List (CloneGap.Equation (Fin n)))
       (hne : es ≠ []) : Source where
   …

   Mentions: OAI.UniqueGamesTheorem.Reduction.CloneGap.Equation, OAI.UniqueGamesTheorem.Reduction.ActualSource.Source

4. theorem OAI.UniqueGamesTheorem.Reduction.ActualSource.Source.sourceList_ofList line 34
5. theorem OAI.UniqueGamesTheorem.Reduction.ActualSource.Source.sourceList_length line 39
6. theorem OAI.UniqueGamesTheorem.Reduction.ActualSource.Source.sourceList_nonempty line 42
7. instance OAI.UniqueGamesTheorem.Reduction.ActualSource.sourceIndexNonempty line 50
8. def OAI.UniqueGamesTheorem.Reduction.ActualSource.Source.satisfied line 53
9. def OAI.UniqueGamesTheorem.Reduction.ActualSource.Source.failure line 56
10. def OAI.UniqueGamesTheorem.Reduction.ActualSource.Source.DistinctNames line 59
11. abbrev OAI.UniqueGamesTheorem.Reduction.ActualSource.Alphabet line 64
12. abbrev OAI.UniqueGamesTheorem.Reduction.ActualSource.Ambient line 65
13. def OAI.UniqueGamesTheorem.Reduction.ActualSource.alphabetEmbedding line 67
14. theorem OAI.UniqueGamesTheorem.Reduction.ActualSource.alphabetEmbedding_apply line 70
15. structure OAI.UniqueGamesTheorem.Reduction.ActualSource.SplitGadget line 74

    Source documentation

    Noise indices retain multiplicity even if several indices have equal vectors.

    structure SplitGadget (s d : Nat) where
    …

16. def OAI.UniqueGamesTheorem.Reduction.ActualSource.SplitGadget.stabilityError line 84
17. def OAI.UniqueGamesTheorem.Reduction.ActualSource.SplitGadget.kernelError line 88
18. theorem OAI.UniqueGamesTheorem.Reduction.ActualSource.SplitGadget.stabilityError_nonneg line 92
19. theorem OAI.UniqueGamesTheorem.Reduction.ActualSource.SplitGadget.stabilityError_le_one line 98
20. theorem OAI.UniqueGamesTheorem.Integration.SplitGadget.exists_split_equiv line 120

    Source documentation

    Any injective symbol embedding admits finite coordinates in which it is the first summand. This is a theorem about the actual ambient vector space.

    theorem exists_split_equiv {s : Nat} (e : Vector s →ₗ[F2] R)
        (he : Function.Injective e) :
        ∃ d : Nat, ∃ φ : R ≃ₗ[F2] (Vector s × Vector d),
          ∀ c, φ (e c) = (c, 0) := by
    …

21. def OAI.UniqueGamesTheorem.Integration.SplitGadget.kernelProbability line 139
22. theorem OAI.UniqueGamesTheorem.Integration.SplitGadget.kernelProbability_eq_kernelError line 145
23. def OAI.UniqueGamesTheorem.Integration.SplitGadget.transport line 155

    Source documentation

    Move all ambient vectors through a linear equivalence, retaining the same noise indices and their multiplicities.

    noncomputable def transport {s d : Nat} (g : Data (Vector s))
        (φ : g.Ambient ≃ₗ[F2] Ambient s d)
        (he : ∀ c, φ (g.embed c) = (c, 0)) : SplitGadget s d where
    …

24. theorem OAI.UniqueGamesTheorem.Integration.SplitGadget.transport_stabilityError line 169

    Source documentation

    Uniform stability is invariant under the coordinate change.

    theorem transport_stabilityError {s d : Nat} (g : Data (Vector s))
        (φ : g.Ambient ≃ₗ[F2] Ambient s d)
        (he : ∀ c, φ (g.embed c) = (c, 0)) :
        (transport g φ he).stabilityError = stabilityError g := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.SplitGadget.transport

25. theorem OAI.UniqueGamesTheorem.Integration.SplitGadget.transport_kernelError line 179

    Source documentation

    Every zero-image probability is invariant under the same coordinate change.

    theorem transport_kernelError {s d p : Nat} (g : Data (Vector s))
        (φ : g.Ambient ≃ₗ[F2] Ambient s d)
        (he : ∀ c, φ (g.embed c) = (c, 0))
        (S : Ambient s d →ₗ[F2] Vector p) :
        (transport g φ he).kernelError S = kernelError g (S.comp φ.toLinearMap) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.SplitGadget.transport

26. theorem OAI.UniqueGamesTheorem.Integration.SplitGadget.transport_symbol_map line 190

    Source documentation

    The restriction to the symbol space is exactly the same linear map.

    theorem transport_symbol_map {s d : Nat} (g : Data (Vector s))
        (φ : g.Ambient ≃ₗ[F2] Ambient s d)
        (he : ∀ c, φ (g.embed c) = (c, 0))
        {P : Type} [AddCommGroup P] [Module F2 P]
        (S : Ambient s d →ₗ[F2] P) :
        (S.comp φ.toLinearMap).comp g.embed = S.comp (alphabetEmbedding s d) := by
    …

27. theorem OAI.UniqueGamesTheorem.Integration.SplitGadget.transport_kernelProbability line 201
28. theorem OAI.UniqueGamesTheorem.Integration.SplitGadget.transport_satisfies line 211

    Source documentation

    Both numerical gadget guarantees survive the coordinate change.

    theorem transport_satisfies {s d : Nat} (g : Data (Vector s))
        (φ : g.Ambient ≃ₗ[F2] Ambient s d)
        (he : ∀ c, φ (g.embed c) = (c, 0))
        {ζ ν : ℚ} {r : Nat} (hg : Satisfies g ζ ν r) :
        (transport g φ he).stabilityError ≤ ζ ∧
          ∀ p (S : Ambient s d →ₗ[F2] Vector p),
            r ≤ Module.finrank F2 (S.comp (alphabetEmbedding s d)).range →
            (transport g φ he).kernelError S ≤ ν := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.SplitGadget.transport

29. theorem OAI.UniqueGamesTheorem.Integration.SplitGadget.exists_split_gadget line 229

    Source documentation

    Every actual gadget satisfying the quantitative guarantees has a split coordinate representative with exactly those guarantees.

    theorem exists_split_gadget {s : Nat} (g : Data (Vector s))
        {ζ ν : ℚ} {r : Nat} (hg : Satisfies g ζ ν r) :
        ∃ d : Nat, ∃ h : SplitGadget s d,
          h.stabilityError ≤ ζ ∧
          ∀ p (S : Ambient s d →ₗ[F2] Vector p),
            r ≤ Module.finrank F2 (S.comp (alphabetEmbedding s d)).range →
            h.kernelError S ≤ ν := by
    …

30. theorem OAI.UniqueGamesTheorem.Integration.SplitGadget.exists_split_gadget_general line 241

    Source documentation

    The coordinate representative preserves dispersion for every target, including the question spaces used directly by the soundness analysis.

    theorem exists_split_gadget_general {s : Nat} (g : Data (Vector s))
        {ζ ν : ℚ} {r : Nat} (hg : Satisfies g ζ ν r) :
        ∃ d : Nat, ∃ h : SplitGadget s d,
          h.stabilityError ≤ ζ ∧
          ∀ (P : Type) [AddCommGroup P] [Module F2 P]
            (S : Ambient s d →ₗ[F2] P),
            r ≤ Module.finrank F2 (S.comp (alphabetEmbedding s d)).range →
            kernelProbability h S ≤ ν := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.SplitGadget.kernelProbability