OAI/Computability/UniqueGames/Decoding/ActualAdviceBridgeLemmas.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.indexSlot line 26
2. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.slotIndex_indexSlot line 29
3. structure OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.Policies line 33
4. def OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.projection line 40
5. def OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.displayedQuestion line 45
6. def OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.agrees line 49
7. def OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.strategy line 55
8. def OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.encodedMapCoefficients line 61
9. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.sample_question line 66
10. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.agrees_implies_actualWin line 77

    Source documentation

    Every actual projection-agreement event is accepted after the two separate local input/answer conversions. This is pointwise in all sampled maps/questions.

    theorem agrees_implies_actualWin [Fintype Q] [DecidableEq Q]
        (coordinates : D ≃ₗ[F2] (Q → F2))
        (g : IncidenceExtraction.Incidence O N) (policy : Policies k g D)
        (J : Finset (Fin k)) (Y : RawPoint J →ₗ[F2] D) (draw : Draw (Fin k) O)
        (hagree : agrees g policy J Y draw) :
        actualWin J g (encodedMapCoefficients coordinates J Y)
          (strategy coordinates g policy J) draw := by
    …

    Mentions: OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.Policies, OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.agrees, OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.encodedMapCoefficients, OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.strategy

11. def OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.fixedMapSuccess line 118

    Source documentation

    Actual independent weighted occurrence/position draws, at a fixed genuine partner map. table is the product of the identical coordinate laws.

    def fixedMapSuccess (μ : FiniteDistribution (O × Fin 3))
        (g : IncidenceExtraction.Incidence O N) (policy : Policies k g D)
        (J : Finset (Fin k)) (Y : RawPoint J →ₗ[F2] D) : ℝ :=
    …

    Mentions: OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.Policies

12. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.fixedMapSuccess_le line 125
13. def OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.mapBitsEquiv line 137
14. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.uniform_maps_to_bits line 141
15. def OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.nativeStrategy line 149
16. def OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.success line 156

    Source documentation

    Sample the Bernoulli mask, a uniform actual map on its partner space, and independent weighted equation/position draws. This is the actual advice law.

    def success (μ : FiniteDistribution (O × Fin 3))
        (g : IncidenceExtraction.Incidence O N) (policy : Policies k g D)
        (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1) : ℝ :=
    …

    Mentions: OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.Policies

17. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.expectation_mono line 163
18. theorem OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.success_le_native line 170

    Source documentation

    The exact map/coefficient bijection joins the actual policy success to the already-defined native clean experiment.

    theorem success_le_native (coordinates : D ≃ₗ[F2] (Q → F2))
        (μ : FiniteDistribution (O × Fin 3))
        (g : IncidenceExtraction.Incidence O N) (policy : Policies k g D)
        (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1) :
        success μ g policy β hβ₀ hβ₁ ≤
          NativeExperiment.success k μ g β hβ₀ hβ₁ (nativeStrategy coordinates g policy) := by
    …

    Mentions: OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.Policies, OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.success, OAI.UniqueGamesTheorem.Clean.NativeExperiment.success, OAI.UniqueGamesTheorem.Clean.ActualAdviceBridge.nativeStrategy

19. theorem OAI.UniqueGamesTheorem.Clean.Bound.repeated_incidence_value_le line 205

    Source documentation

    The precise rate is obtained from the proved ordinary projection-game bound, with no question-set or alphabet parameter in its base.

    theorem repeated_incidence_value_le
        (g : IncidenceExtraction.Incidence O N) (ω : FiniteDistribution O)
        (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
        (hopt : IncidenceGap.parityValue g ω ≤ (4 : ℝ) / 5) (n : ℕ) :
        ((incidenceGame g ((IncidenceGap.slotLaw ω).pushforward (incidence g.name))).repetition n).value ≤
          (1 - (1 : ℝ) / 3600) ^ n := by
    …

    Mentions: OAI.UniqueGamesTheorem.Clean.IncidenceGap.parityValue, OAI.UniqueGamesTheorem.Clean.IncidenceGap.slotLaw

20. theorem OAI.UniqueGamesTheorem.Clean.Bound.clean_success_le line 218

    Source documentation

    Section 5's clean agreement estimate, with every sampling/locality/rate step discharged for the explicit advice experiment.

    theorem clean_success_le (k : ℕ) (g : IncidenceExtraction.Incidence O N)
        (ω : FiniteDistribution O) (extraLaw : FiniteDistribution (Additional k R))
        (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
        (strategy : Additional k R → SparseSeed k R → LocalStrategies k R O N)
        (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
        (hopt : IncidenceGap.parityValue g ω ≤ (4 : ℝ) / 5) :
        success k (IncidenceGap.slotLaw ω) g extraLaw β hβ₀ hβ₁ strategy ≤
          (1 - (β / (Fintype.card (Coefficient R) : ℝ)) / 3600) ^ k := by
    …

    Mentions: OAI.UniqueGamesTheorem.Clean.IncidenceGap.parityValue, OAI.UniqueGamesTheorem.Clean.IncidenceGap.slotLaw

21. theorem OAI.UniqueGamesTheorem.Clean.Bound.clean_success_le_dimension line 235

    Source documentation

    A uniform bound on visible advice dimension makes the estimate independent of the sampled map A. Apply with Coefficient R ≃ W × range A.

    theorem clean_success_le_dimension (k : ℕ) (g : IncidenceExtraction.Incidence O N)
        (ω : FiniteDistribution O) (extraLaw : FiniteDistribution (Additional k R))
        (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
        (strategy : Additional k R → SparseSeed k R → LocalStrategies k R O N)
        (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
        (hopt : IncidenceGap.parityValue g ω ≤ (4 : ℝ) / 5)
        (dimW rs : ℕ) (hcard : Fintype.card (Coefficient R) ≤ 2 ^ (dimW + rs)) :
        success k (IncidenceGap.slotLaw ω) g extraLaw β hβ₀ hβ₁ strategy ≤
          (1 - (β / (2 : ℝ) ^ (dimW + rs)) / 3600) ^ k := by
    …

    Mentions: OAI.UniqueGamesTheorem.Clean.IncidenceGap.parityValue, OAI.UniqueGamesTheorem.Clean.IncidenceGap.slotLaw

22. theorem OAI.UniqueGamesTheorem.Clean.Bound.native_clean_success_le_dimension line 252