OAI/Computability/MaxCut/Encoding/ActualAdviceUpper.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

The clean-coordinate upper bound for the actual private-decoding policies. At every fixed public map A, the visible coefficient space is Vector d × A.range. Its cardinality is at most 2^(d+rs), including when A is rank deficient. The true independent uniform maps T,M, the Bernoulli mask, and all iid occurrence/position draws are retained by the proved sampling equality, before averaging over the uniform public map.

  1. instance OAI.MaxCutGames.Decoder.ActualAdviceUpper.publicMapFintype line 32
  2. def OAI.MaxCutGames.Decoder.ActualAdviceUpper.sourceIncidence line 37

    Source documentation

    The ordinary game uses actual occurrence IDs and actual variable names.

    def sourceIncidence (S : Source) :
    IncidenceExtraction.Incidence (Fin S.occurrences) (Fin S.«variables») where
…
  3. abbrev OAI.MaxCutGames.Decoder.ActualAdviceUpper.Visible line 42
  4. def OAI.MaxCutGames.Decoder.ActualAdviceUpper.complementMap line 44
  5. def OAI.MaxCutGames.Decoder.ActualAdviceUpper.rowMap line 49
  6. def OAI.MaxCutGames.Decoder.ActualAdviceUpper.fullInput line 55

    Source documentation

    Decode only the data visible to the first player.

    def fullInput (S : Source) (A : Alphabet s →ₗ[F2] Vector rs)
    (occ : Fin k → Fin S.occurrences)
    (Y : ActualHomogeneous.E k →ₗ[F2] Visible d A) :
    VisiblePolicies.LeftInput S k s d (Vector rs) where
…

    Mentions: OAI.MaxCutGames.Decoder.ActualAdviceUpper.Visible, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput

  7. def OAI.MaxCutGames.Decoder.ActualAdviceUpper.projectedInput line 65

    Source documentation

    Decode only the displayed question and the visible row/complement maps.

    def projectedInput (S : Source) (A : Alphabet s →ₗ[F2] Vector rs)
    (J : Finset (Fin k)) (O : RawPrivateTable.SupportedV J (ActualGame.names S))
    (Y : RawPartnerTarget.RawPoint J →ₗ[F2] Visible d A) :
    VisiblePolicies.RightInput S J s d (Vector rs) where
…

    Mentions: OAI.MaxCutGames.Decoder.ActualAdviceUpper.Visible, OAI.MaxCutGames.Decoder.VisiblePolicies.RightInput

  8. def OAI.MaxCutGames.Decoder.ActualAdviceUpper.policies line 76

    Source documentation

    Actual observation-local stochastic policies, in the exact advice space used by the clean-coordinate experiment. Public A is fixed before questions.

    def policies (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector rs) →
      VisiblePolicies.ResponseWitness k → Prop)
    (A : Alphabet s →ₗ[F2] Vector rs) :
    Clean.ActualAdviceStochasticBridge.Policies k (sourceIncidence S) (Visible d A) where
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.Policies, OAI.MaxCutGames.Decoder.ActualAdviceUpper.sourceIncidence, OAI.MaxCutGames.Decoder.ActualAdviceUpper.Visible

  9. def OAI.MaxCutGames.Decoder.ActualAdviceUpper.actualDraw line 87

    Source documentation

    The real draw corresponding to a fixed mask and the independently sampled complement and hidden matrices.

    def actualDraw (S : Source) (A : Alphabet s →ₗ[F2] Vector rs)
    (J : Finset (Fin k)) (occ : Fin k → Fin S.occurrences)
    (slot : Fin k → PartnerProjection.Slot)
    (T : RawPartnerTarget.RawPoint J →ₗ[F2] Vector d)
    (M : RawPartnerTarget.RawPoint J →ₗ[F2] Alphabet s) :
    AdviceExperiment.Draw k (Fin S.occurrences) (Alphabet s) (Vector d) (Vector rs) where
…

    Mentions: OAI.MaxCutGames.Decoder.AdviceExperiment.Draw

  10. theorem OAI.MaxCutGames.Decoder.ActualAdviceUpper.fullInput_actual line 100
  11. theorem OAI.MaxCutGames.Decoder.ActualAdviceUpper.projectedInput_actual line 110
  12. theorem OAI.MaxCutGames.Decoder.ActualAdviceUpper.policyAgreement_actual line 123

    Source documentation

    The product of the two local policy kernels is literally the private decoder's observed agreement probability, before any expectations are taken.

    theorem policyAgreement_actual (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector rs) →
      VisiblePolicies.ResponseWitness k → Prop)
    (A : Alphabet s →ₗ[F2] Vector rs) (J : Finset (Fin k))
    (occ : Fin k → Fin S.occurrences) (slot : Fin k → PartnerProjection.Slot)
    (T : RawPartnerTarget.RawPoint J →ₗ[F2] Vector d)
    (M : RawPartnerTarget.RawPoint J →ₗ[F2] Alphabet s) :
    (((policies S labeling good A).first J occ
        ((AdviceLaw.visibleMap A T M).comp
          (RawPrivateTable.projection J (ActualGame.rhs S) occ slot))).product
      ((policies S labeling good A).second J
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Decoder.ActualAdviceUpper.policies, OAI.MaxCutGames.Decoder.AdviceLaw.visibleMap

  13. theorem OAI.MaxCutGames.Decoder.ActualAdviceUpper.source_projection_eq line 147

    Source documentation

    The clean experiment's indexed slot is exactly the actual bit projection; this includes the third-position parity intercept.

    theorem source_projection_eq (S : Source) (J : Finset (Fin k))
    (draw : Fin k → Fin S.occurrences × Fin 3) :
    Clean.ActualAdviceBridge.projection (sourceIncidence S) J draw =
      RawPrivateTable.projection J (ActualGame.rhs S) (fun j => (draw j).1)
        (fun j => Clean.ActualAdviceBridge.indexSlot (draw j).2) := by
…

    Mentions: OAI.MaxCutGames.Clean.ActualAdviceBridge.projection, OAI.MaxCutGames.Decoder.ActualAdviceUpper.sourceIncidence, OAI.MaxCutGames.Clean.ActualAdviceBridge.indexSlot

  14. theorem OAI.MaxCutGames.Decoder.ActualAdviceUpper.fixed_public_map_bound line 155
  15. theorem OAI.MaxCutGames.Decoder.ActualAdviceUpper.public_map_average_bound line 170

    Source documentation

    Rank deficiency is allowed separately at every public-map outcome.

    theorem public_map_average_bound
    {O N : Type} [Fintype O] [DecidableEq O] [Fintype N] [DecidableEq N]
    (g : IncidenceExtraction.Incidence O N) (ω : FiniteDistribution O)
    (policy : (A : Alphabet s →ₗ[F2] Vector rs) →
      Clean.ActualAdviceStochasticBridge.Policies k g (Visible d A))
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j)
    (hopt : Clean.IncidenceGap.parityValue g ω ≤ (4 : ℝ) / 5) :
    (FiniteDistribution.uniform (Alphabet s →ₗ[F2] Vector rs)).expectation
        (fun A => AdviceLaw.actualSuccess (Clean.IncidenceGap.slotLaw ω) g A
          (policy A) β hβ₀ hβ₁) ≤
      (1 - (β / (2 : ℝ) ^ (d + rs)) / 3600) ^ k := by
…

    Mentions: OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.Policies, OAI.MaxCutGames.Decoder.ActualAdviceUpper.Visible, OAI.MaxCutGames.Clean.IncidenceGap.parityValue, OAI.MaxCutGames.Decoder.AdviceLaw.actualSuccess, OAI.MaxCutGames.Clean.IncidenceGap.slotLaw

  16. theorem OAI.MaxCutGames.Decoder.ActualAdviceUpper.actual_source_average_bound line 193

    Source documentation

    The actual policies selected from the two separate observations obey the bound under uniform occurrence IDs and every independent private response.

    theorem actual_source_average_bound (S : Source)
    (labeling : Fin (TableKeysGame.vertexCount S k s d) → Fin (2 ^ s))
    (good : VisiblePolicies.LeftInput S k s d (Vector rs) →
      VisiblePolicies.ResponseWitness k → Prop)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (distinct : ∀ o i j, (sourceIncidence S).name o i =
      (sourceIncidence S).name o j → i = j)
    (hopt : Clean.IncidenceGap.parityValue (sourceIncidence S)
      (FiniteDistribution.uniform (Fin S.occurrences)) ≤ (4 : ℝ) / 5) :
    (FiniteDistribution.uniform (Alphabet s →ₗ[F2] Vector rs)).expectation
        (fun A => AdviceLaw.actualSuccess
          (Clean.IncidenceGap.slotLaw (FiniteDistribution.uniform (Fin S.occurrences)))
…

    Mentions: OAI.MaxCutGames.Decoder.TableKeysGame.vertexCount, OAI.MaxCutGames.Decoder.VisiblePolicies.LeftInput, OAI.MaxCutGames.Decoder.VisiblePolicies.ResponseWitness, OAI.MaxCutGames.Decoder.ActualAdviceUpper.sourceIncidence, OAI.MaxCutGames.Clean.IncidenceGap.parityValue, OAI.MaxCutGames.Decoder.AdviceLaw.actualSuccess, OAI.MaxCutGames.Clean.IncidenceGap.slotLaw