OAI/Computability/UniqueGames/Reduction/GapSemanticsLemmas.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Integration.GapSemantics.errorValue line 21
2. def OAI.UniqueGamesTheorem.Integration.GapSemantics.satisfactionRate line 23
3. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.countSatisfied_eq_sum line 26
4. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.countSatisfied_ofFn line 34
5. def OAI.UniqueGamesTheorem.Integration.GapSemantics.uniformConstraintAcceptance line 41
6. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.uniformConstraintAcceptance_eq_rate line 48

   Source documentation

   Uniform sampling is over occurrence indices, so equal constraints are counted with exactly their stored multiplicity.

   theorem uniformConstraintAcceptance_eq_rate {q : Nat} (g : Instance q)
       (labeling : Fin g.vertices → Fin q) :
       uniformConstraintAcceptance g labeling = satisfactionRate g labeling := by
   …

   Mentions: OAI.UniqueGamesTheorem.Integration.GapSemantics.uniformConstraintAcceptance, OAI.UniqueGamesTheorem.Integration.GapSemantics.satisfactionRate

7. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.errorValue_pos line 59
8. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.errorValue_lt_half line 64
9. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.satisfactionRate_nonneg line 71
10. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.satisfactionRate_le_one line 75
11. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.completeAt_iff line 83
12. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.soundAt_iff line 108
13. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.completeAt_mono line 129

    Source documentation

    Strengthening either error threshold implies the requested weaker gap.

    theorem completeAt_mono {q : Nat} {e e' : RationalError} {g : Instance q}
        (hee : errorValue e ≤ errorValue e') (hg : CompleteAt e g) : CompleteAt e' g := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.GapSemantics.errorValue

14. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.soundAt_mono line 135
15. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.completeAt_iff_real line 142

    Source documentation

    The same target gap is obtained when the analysis uses real expectations.

    theorem completeAt_iff_real {q : Nat} (e : RationalError) (g : Instance q) :
        CompleteAt e g ↔ ∃ labeling,
          1 - (errorValue e : ℝ) ≤
            (countSatisfied labeling g.constraints : ℝ) / g.constraints.length := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.GapSemantics.errorValue

16. theorem OAI.UniqueGamesTheorem.Integration.GapSemantics.soundAt_iff_real line 153
17. def OAI.UniqueGamesTheorem.Integration.DyadicErrors.dyadicError line 178

    Source documentation

    The index starts at denominator four, so every encoded error is below one half.

    def dyadicError (n : Nat) : RationalError where
    …

18. theorem OAI.UniqueGamesTheorem.Integration.DyadicErrors.errorValue_dyadic line 188
19. theorem OAI.UniqueGamesTheorem.Integration.DyadicErrors.exists_dyadic_below_real line 193

    Source documentation

    Positive dyadic errors are cofinal among all positive real tolerances.

    theorem exists_dyadic_below_real {ε : ℝ} (hε : 0 < ε) :
        ∃ n : Nat, (errorValue (dyadicError n) : ℝ) < ε := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.DyadicErrors.dyadicError

20. theorem OAI.UniqueGamesTheorem.Integration.DyadicErrors.exists_dyadic_below line 205
21. theorem OAI.UniqueGamesTheorem.Integration.DyadicErrors.completeAt_real_of_dyadic line 212

    Source documentation

    A proved dyadic completeness gap gives the claimed real tolerance.

    theorem completeAt_real_of_dyadic {q n : Nat} {ε : ℝ} {g : Instance q}
        (hε : (errorValue (dyadicError n) : ℝ) ≤ ε)
        (hg : CompleteAt (dyadicError n) g) :
        ∃ labeling, 1 - ε ≤
          (countSatisfied labeling g.constraints : ℝ) / g.constraints.length := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.DyadicErrors.dyadicError

22. theorem OAI.UniqueGamesTheorem.Integration.DyadicErrors.soundAt_real_of_dyadic line 220
23. def OAI.UniqueGamesTheorem.Integration.InstanceEquivalences.renameConstraint line 241
24. theorem OAI.UniqueGamesTheorem.Integration.InstanceEquivalences.renameConstraint_satisfied line 247
25. theorem OAI.UniqueGamesTheorem.Integration.InstanceEquivalences.rename_count line 251
26. def OAI.UniqueGamesTheorem.Integration.InstanceEquivalences.renameInstance line 260
27. theorem OAI.UniqueGamesTheorem.Integration.InstanceEquivalences.countSatisfied_perm line 268
28. theorem OAI.UniqueGamesTheorem.Integration.InstanceEquivalences.satisfactionRate_eq_of_rename_perm line 277

    Source documentation

    This statement is directly usable by an executable adapter: only its vertex equivalence and its permutation of the explicit edge list are needed.

    theorem satisfactionRate_eq_of_rename_perm {q : Nat} (g h : Instance q)
        (e : Fin g.vertices ≃ Fin h.vertices)
        (hp : h.constraints.Perm (g.constraints.map (renameConstraint e)))
        (labeling : Fin h.vertices → Fin q) :
        satisfactionRate h labeling = satisfactionRate g (labeling ∘ e) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Integration.InstanceEquivalences.renameConstraint

29. theorem OAI.UniqueGamesTheorem.Integration.InstanceEquivalences.completeAt_iff_of_rename_perm line 289
30. theorem OAI.UniqueGamesTheorem.Integration.InstanceEquivalences.soundAt_iff_of_rename_perm line 303
31. theorem OAI.UniqueGamesTheorem.Integration.InstanceEquivalences.rename_rate line 317
32. theorem OAI.UniqueGamesTheorem.Integration.InstanceEquivalences.completeAt_rename_iff line 322
33. theorem OAI.UniqueGamesTheorem.Integration.InstanceEquivalences.soundAt_rename_iff line 327