OAI/Computability/UniqueGames/Reduction/OuterCompletenessLemmas.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.UniqueGamesTheorem.Reduction.OuterCompleteness.weighted_completeAt line 18

   Source documentation

   Completeness for the actual output after rounding and finite cloning.

   theorem weighted_completeAt {n s d : Nat}
       (W : RationalSource (CloneGap.Equation (Fin n))) (γ ξ : ℚ)
       (hγ : 0 < γ) (hξ : ξ ≤ γ / 4) (k : Nat) (g : SplitGadget s d)
       (error : RationalError)
       (hsource : ∃ A : Fin n → Bool,
         1 - ξ ≤ W.weightedValue (fun e => CloneGap.satisfied e A))
       (hbudget : (k : ℚ) * γ + g.stabilityError / 2 ≤ GapSemantics.errorValue error) :
       CompleteAt error
         (ActualGame.outputInstance (Preprocessing.uniformSource W γ hγ) k g) := by
   …

   Mentions: OAI.UniqueGamesTheorem.Reduction.CloneGap.Equation, OAI.UniqueGamesTheorem.Reduction.CloneGap.satisfied, OAI.UniqueGamesTheorem.Reduction.ActualGame.outputInstance, OAI.UniqueGamesTheorem.Reduction.Preprocessing.uniformSource

2. def OAI.UniqueGamesTheorem.Reduction.OuterCompleteness.sourceError line 32
3. theorem OAI.UniqueGamesTheorem.Reduction.OuterCompleteness.sourceError_pos line 35
4. theorem OAI.UniqueGamesTheorem.Reduction.OuterCompleteness.weighted_completeAt_of_parameters line 40
5. theorem OAI.UniqueGamesTheorem.Reduction.OuterCompleteness.weighted_explicit_completeAt_of_parameters line 61
6. def OAI.UniqueGamesTheorem.Reduction.UniformReduction.rawSource line 90
7. def OAI.UniqueGamesTheorem.Reduction.UniformReduction.source line 93
8. def OAI.UniqueGamesTheorem.Reduction.UniformReduction.output line 98

   Source documentation

   All proof-only numerical parameters and the correcting function are absent from the runtime input of this map.

   def output (es : List (CloneGap.Equation (Fin n))) (hne : es ≠ [])
       (k : Nat) (T : NoiseTables.Table s d) : Instance (2 ^ s) :=
   …

   Mentions: OAI.UniqueGamesTheorem.Reduction.CloneGap.Equation

9. def OAI.UniqueGamesTheorem.Reduction.UniformReduction.satisfaction line 102
10. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.source_variables line 105
11. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.source_occurrences line 108
12. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.source_occurrences_le line 112
13. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.source_distinct line 120
14. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.output_constraint_count line 123
15. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.output_vertex_count line 133
16. def OAI.UniqueGamesTheorem.Reduction.UniformReduction.liftAssignment line 138
17. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.source_failure_preserved line 142
18. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.raw_failure_add_satisfaction line 147
19. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.source_complete line 156
20. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.raw_quarter_count_gap line 167

    Source documentation

    The original uniform ((1+ξ)/2) satisfaction bound supplies exactly the quarter-gap premise needed by the cloning theorem.

    theorem raw_quarter_count_gap (es : List (CloneGap.Equation (Fin n))) (hne : es ≠ [])
        (ξ : ℚ) (hξ : ξ ≤ 1 / 2)
        (hsource : ∀ A : Fin n → Bool, satisfaction es A ≤ (1 + ξ) / 2) :
        ∀ A : Fin (rawSource es hne).variables → Bool,
          (rawSource es hne).sourceList.length ≤
            4 * (rawSource es hne).sourceList.countP (fun e => !CloneGap.satisfied e A) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Reduction.CloneGap.Equation, OAI.UniqueGamesTheorem.Reduction.UniformReduction.satisfaction, OAI.UniqueGamesTheorem.Reduction.UniformReduction.rawSource, OAI.UniqueGamesTheorem.Reduction.CloneGap.satisfied

21. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.source_sound line 179
22. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.sourceGame_sound line 199
23. theorem OAI.UniqueGamesTheorem.Reduction.UniformReduction.completeAt_of_parameters line 214