OAI/Computability/MaxCut/Games/PartnerFullSampling.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Full slot indices and the actual partner law

Uniform indices at all positions restrict to uniform indices on an active set. The explicit restriction/complement equivalence proves this sampling fact. The dependent partner average then equals sampling the active set followed by all slot indices, including unused indices outside the active set. Finally, the coordinatewise occurrence/slot draw is related to that same law.

  1. def OAI.MaxCutGames.Soundness.PartnerFullSampling.restrictIndices line 24
  2. def OAI.MaxCutGames.Soundness.PartnerFullSampling.restrictionProductEquiv line 28

    Source documentation

    The values inside and outside a finite set reconstruct the full tuple.

    def restrictionProductEquiv {P X : Type*} [DecidableEq P] (J : Finset P) :
    (P → X) ≃ ((↥J → X) × ({j : P // j ∉ J} → X)) where
…
  3. theorem OAI.MaxCutGames.Soundness.PartnerFullSampling.expect_restrictIndices line 45

    Source documentation

    Marginalizing the nonempty complement tuple gives the exact uniform law on the active coordinates. This includes an empty active set or complement.

    theorem expect_restrictIndices {P X : Type*} [Fintype P] [DecidableEq P]
    [Fintype X] [Nonempty X] (J : Finset P) (h : (↥J → X) → ℝ) :
    (𝔼 indices : P → X, h (restrictIndices J indices)) =
      𝔼 activeIndices : ↥J → X, h activeIndices := by
…

    Mentions: OAI.MaxCutGames.Soundness.PartnerFullSampling.restrictIndices

  4. def OAI.MaxCutGames.Soundness.PartnerFullSampling.fromFullIndices line 59
  5. theorem OAI.MaxCutGames.Soundness.PartnerFullSampling.fixed_active_expect_fullIndices line 63

    Source documentation

    Fixed-active-set form of the actual three-way slot sampling identity.

    theorem fixed_active_expect_fullIndices {k t : ℕ} (a : ActiveSet k t)
    (h : (↥a.val → Fin 3) → ℝ) :
    (𝔼 indices : Fin k → Fin 3, h (restrictIndices a.val indices)) =
      𝔼 activeIndices : ↥a.val → Fin 3, h activeIndices :=
…

    Mentions: OAI.MaxCutGames.Soundness.PartnerFullSampling.restrictIndices

  6. theorem OAI.MaxCutGames.Soundness.PartnerFullSampling.partner_expect_active_slots line 71

    Source documentation

    All active-set fibers have 3^t elements, so the uniform dependent-pair average is the active-set average of the uniform slot average.

    theorem partner_expect_active_slots (k t : ℕ) (f : Partner k t → ℝ) :
    (𝔼 p : Partner k t, f p) =
      𝔼 a : ActiveSet k t, 𝔼 indices : ↥a.val → Fin 3, f ⟨a, indices⟩ := by
…
  7. theorem OAI.MaxCutGames.Soundness.PartnerFullSampling.partner_expect_fullIndices line 83

    Source documentation

    The full-index experiment has exactly the existing Partner law. No independence or equality of probability laws is assumed.

    theorem partner_expect_fullIndices (k t : ℕ) (f : Partner k t → ℝ) :
    (𝔼 p : Partner k t, f p) =
      𝔼 a : ActiveSet k t, 𝔼 indices : Fin k → Fin 3,
        f (fromFullIndices a indices) := by
…

    Mentions: OAI.MaxCutGames.Soundness.PartnerFullSampling.fromFullIndices

  8. theorem OAI.MaxCutGames.Soundness.PartnerFullSampling.projection_eq_of_slots_eq_on_active line 93

    Source documentation

    Slots outside active positions have no effect on the genuine projection.

    theorem projection_eq_of_slots_eq_on_active {P : Type}
    (rhs active : P → Bool) (slot slot' : P → PartnerProjection.Slot)
    (hslot : ∀ j, active j = true → slot j = slot' j) :
    PartnerLinear.projection rhs active slot =
      PartnerLinear.projection rhs active slot' := by
…

    Mentions: OAI.MaxCutGames.Soundness.PartnerProjection.Slot, OAI.MaxCutGames.Soundness.PartnerLinear.projection

  9. theorem OAI.MaxCutGames.Soundness.PartnerFullSampling.projection_fromFullIndices line 112

    Source documentation

    Defaulting inactive slots to .first gives the same map as retaining all the independently sampled full indices.

    theorem projection_fromFullIndices {k t : ℕ} (rhs : Fin k → Bool)
    (a : ActiveSet k t) (indices : Fin k → Fin 3) :
    PartnerLinear.projection rhs (active (fromFullIndices a indices))
        (slots (fromFullIndices a indices)) =
      PartnerLinear.projection rhs (active (fromFullIndices a indices))
        (fun j => decodeSlot (indices j)) := by
…

    Mentions: OAI.MaxCutGames.Soundness.PartnerLinear.projection, OAI.MaxCutGames.Soundness.PartnerFullSampling.fromFullIndices

  10. def OAI.MaxCutGames.Soundness.PartnerFullSampling.drawProductEquiv line 127

    Source documentation

    Drawing an occurrence and a slot at each position is the same finite sample space as drawing the occurrence tuple and the slot tuple separately.

    def drawProductEquiv {P Id : Type*} :
    (P → Id × Fin 3) ≃ ((P → Id) × (P → Fin 3)) where
…
  11. theorem OAI.MaxCutGames.Soundness.PartnerFullSampling.fixed_active_rawDraw_expect line 137

    Source documentation

    The raw occurrence/slot draw induces independent uniform occurrences and uniform active slots, with all unused slot choices marginalized exactly.

    theorem fixed_active_rawDraw_expect {k t : ℕ} {Id : Type*} [Fintype Id]
    (a : ActiveSet k t)
    (f : (Fin k → Id) → (↥a.val → Fin 3) → ℝ) :
    (𝔼 draw : Fin k → Id × Fin 3,
      f (fun j => (draw j).1)
        (restrictIndices a.val (fun j => (draw j).2))) =
      𝔼 occurrence : Fin k → Id, 𝔼 indices : ↥a.val → Fin 3,
        f occurrence indices := by
…

    Mentions: OAI.MaxCutGames.Soundness.PartnerFullSampling.restrictIndices

  12. theorem OAI.MaxCutGames.Soundness.PartnerFullSampling.occurrence_partner_expect_eq_rawDraw line 166

    Source documentation

    The actual raw draw, including indices outside the active set, agrees with the occurrence-then-partner experiment for every real test function.

    theorem occurrence_partner_expect_eq_rawDraw (k t : ℕ)
    {Id : Type*} [Fintype Id] (f : (Fin k → Id) → Partner k t → ℝ) :
    (𝔼 occurrence : Fin k → Id, 𝔼 p : Partner k t, f occurrence p) =
      𝔼 a : ActiveSet k t, 𝔼 draw : Fin k → Id × Fin 3,
        f (fun j => (draw j).1) (fromFullIndices a (fun j => (draw j).2)) := by
…

    Mentions: OAI.MaxCutGames.Soundness.PartnerFullSampling.fromFullIndices

  13. def OAI.MaxCutGames.Clean.CoefficientSampling.selectCoefficients line 211
  14. def OAI.MaxCutGames.Clean.CoefficientSampling.coefficientProductEquiv line 219

    Source documentation

    Splitting a raw coefficient tuple into its actual independent coordinates.

    def coefficientProductEquiv (J : Finset P) :
    RawCoefficients J C ≃ C × ((PositionOutside J → C × C) × (PositionInside J → C)) where
…
  15. theorem OAI.MaxCutGames.Clean.CoefficientSampling.expect_outside line 241

    Source documentation

    The complement restriction is also uniform, including an empty complement.

    theorem expect_outside (J : Finset P) (f : (PositionOutside J → C) → ℝ) :
    (𝔼 full : P → C, f (fun j => full j.val)) =
      𝔼 outside : PositionOutside J → C, f outside := by
…
  16. theorem OAI.MaxCutGames.Clean.CoefficientSampling.expect_rawCoefficients line 253
  17. theorem OAI.MaxCutGames.Clean.CoefficientSampling.expect_selectCoefficients line 270

    Source documentation

    Sampling all columns and then discarding unused ones has exactly the uniform joint law on the coefficients used by this singleton set.

    theorem expect_selectCoefficients (J : Finset P) (F : RawCoefficients J C → ℝ) :
    (𝔼 extra : C × (P → C × C), 𝔼 single : P → C,
      F (selectCoefficients J extra single)) =
      𝔼 gamma : RawCoefficients J C, F gamma := by
…

    Mentions: OAI.MaxCutGames.Clean.CoefficientSampling.selectCoefficients

  18. theorem OAI.MaxCutGames.Clean.CoefficientSampling.uniform_expectation_eq_expect_inline_CoefficientSampling line 297
  19. theorem OAI.MaxCutGames.Clean.CoefficientSampling.uniform_selectCoefficients line 301
  20. theorem OAI.MaxCutGames.Clean.CoefficientSampling.mask_average_selectCoefficients line 310

    Source documentation

    The fixed-mask identity may be averaged under any independent mask law.

    theorem mask_average_selectCoefficients (maskLaw : FiniteDistribution (Finset P))
    (F : (J : Finset P) → RawCoefficients J C → ℝ) :
    maskLaw.expectation (fun J =>
      (FiniteDistribution.uniform (C × (P → C × C))).expectation (fun extra =>
        (FiniteDistribution.uniform (P → C)).expectation (fun single =>
          F J (selectCoefficients J extra single)))) =
      maskLaw.expectation (fun J =>
        (FiniteDistribution.uniform (RawCoefficients J C)).expectation (F J)) := by
…

    Mentions: OAI.MaxCutGames.Clean.CoefficientSampling.selectCoefficients

  21. theorem OAI.MaxCutGames.Clean.NativeExperiment.expectation_transport_inline_NativeExperiment line 335
  22. theorem OAI.MaxCutGames.Clean.NativeExperiment.iid_product_split line 341
  23. theorem OAI.MaxCutGames.Clean.NativeExperiment.expectation_iid_product line 351
  24. def OAI.MaxCutGames.Clean.NativeExperiment.maskSet line 365
  25. abbrev OAI.MaxCutGames.Clean.NativeExperiment.MaskStrategy line 368
  26. def OAI.MaxCutGames.Clean.NativeExperiment.liftStrategy line 372
  27. def OAI.MaxCutGames.Clean.NativeExperiment.success line 378

    Source documentation

    The actual law: independent singleton choices followed by one independent uniform coefficient at the intercept and each surviving partner coordinate.

    def success (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (strategy : MaskStrategy k R O N) : ℝ :=
…

    Mentions: OAI.MaxCutGames.Clean.NativeExperiment.MaskStrategy

  28. theorem OAI.MaxCutGames.Clean.NativeExperiment.success_eq_flat line 388
  29. def OAI.MaxCutGames.Clean.ActualAdviceBridge.indexSlot line 453
  30. theorem OAI.MaxCutGames.Clean.ActualAdviceBridge.slotIndex_indexSlot line 456
  31. structure OAI.MaxCutGames.Clean.ActualAdviceBridge.Policies line 460
  32. def OAI.MaxCutGames.Clean.ActualAdviceBridge.projection line 467
  33. def OAI.MaxCutGames.Clean.ActualAdviceBridge.displayedQuestion line 472
  34. def OAI.MaxCutGames.Clean.ActualAdviceBridge.agrees line 476
  35. def OAI.MaxCutGames.Clean.ActualAdviceBridge.strategy line 482
  36. def OAI.MaxCutGames.Clean.ActualAdviceBridge.encodedMapCoefficients line 488
  37. theorem OAI.MaxCutGames.Clean.ActualAdviceBridge.sample_question line 493
  38. theorem OAI.MaxCutGames.Clean.ActualAdviceBridge.agrees_implies_actualWin line 504

    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.MaxCutGames.Clean.ActualAdviceBridge.Policies, OAI.MaxCutGames.Clean.ActualAdviceBridge.agrees, OAI.MaxCutGames.Clean.ActualAdviceBridge.encodedMapCoefficients, OAI.MaxCutGames.Clean.ActualAdviceBridge.strategy

  39. def OAI.MaxCutGames.Clean.ActualAdviceBridge.fixedMapSuccess line 545

    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.MaxCutGames.Clean.ActualAdviceBridge.Policies

  40. theorem OAI.MaxCutGames.Clean.ActualAdviceBridge.fixedMapSuccess_le line 552
  41. def OAI.MaxCutGames.Clean.ActualAdviceBridge.mapBitsEquiv line 564
  42. theorem OAI.MaxCutGames.Clean.ActualAdviceBridge.uniform_maps_to_bits line 568
  43. def OAI.MaxCutGames.Clean.ActualAdviceBridge.nativeStrategy line 576
  44. def OAI.MaxCutGames.Clean.ActualAdviceBridge.success line 583

    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.MaxCutGames.Clean.ActualAdviceBridge.Policies

  45. theorem OAI.MaxCutGames.Clean.ActualAdviceBridge.expectation_mono line 590
  46. theorem OAI.MaxCutGames.Clean.ActualAdviceBridge.success_le_native line 598

    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.MaxCutGames.Clean.ActualAdviceBridge.Policies, OAI.MaxCutGames.Clean.ActualAdviceBridge.success, OAI.MaxCutGames.Clean.NativeExperiment.success, OAI.MaxCutGames.Clean.ActualAdviceBridge.nativeStrategy

  47. def OAI.MaxCutGames.Clean.StochasticBound.actualGame line 648

    Source documentation

    The common weighted-game interface for the actual fixed-advice experiment.

    def actualGame (μ : FiniteDistribution (O × Fin 3)) (J : Finset P)
    (g : IncidenceExtraction.Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R)) :
    Game (ZeroInformation.FirstInput P R O) (ZeroInformation.SecondInput P R O N)
      (ActualProjection.FirstAnswer P) (ActualProjection.SecondAnswer P) :=
…
  48. abbrev OAI.MaxCutGames.Clean.StochasticBound.fixedAdviceGame line 657
  49. theorem OAI.MaxCutGames.Clean.StochasticBound.success_eq_fixedAdviceSuccess line 662

    Source documentation

    The two deterministic strategy representations have exactly the same winning probability under the explicitly constructed question law.

    theorem success_eq_fixedAdviceSuccess
    (μ : FiniteDistribution (O × Fin 3)) (J : Finset P)
    (g : IncidenceExtraction.Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R))
    (strategy : Strategy (ZeroInformation.FirstInput P R O)
      (ZeroInformation.SecondInput P R O N)
      (ActualProjection.FirstAnswer P) (ActualProjection.SecondAnswer P)) :
    (actualGame μ J g gamma).success strategy =
      UpperBound.fixedAdviceSuccess μ J g gamma ⟨strategy.1, strategy.2⟩ := by
…

    Mentions: OAI.MaxCutGames.Clean.StochasticBound.actualGame, OAI.MaxCutGames.Clean.UpperBound.fixedAdviceSuccess

  50. theorem OAI.MaxCutGames.Clean.StochasticBound.exists_deterministic_ge_stochastic line 679

    Source documentation

    Each stochastic local response has a deterministic complete response table with at least its success probability. The table is chosen before the questions.

    theorem exists_deterministic_ge_stochastic
    (μ : FiniteDistribution (O × Fin 3)) (J : Finset P)
    (g : IncidenceExtraction.Incidence O N)
    (gamma : RawCoefficients J (ZeroInformation.Bits R))
    (responses₁ : ZeroInformation.FirstInput P R O →
      FiniteDistribution (ActualProjection.FirstAnswer P))
    (responses₂ : ZeroInformation.SecondInput P R O N →
      FiniteDistribution (ActualProjection.SecondAnswer P)) :
    ∃ strategy : OuterStrategy (P := P) (R := R) (O := O) (N := N),
…
  51. theorem OAI.MaxCutGames.Clean.StochasticBound.fixed_advice_stochastic_le_repeated_value line 698
  52. abbrev OAI.MaxCutGames.Clean.StochasticBound.Responses line 714

    Source documentation

    A pair of response kernels, each indexed only by its own complete input.

    abbrev Responses (P R O N : Type) [Fintype P] [DecidableEq P] :=
…
  53. def OAI.MaxCutGames.Clean.StochasticBound.nativeStochasticSuccess line 720

    Source documentation

    The native experiment samples a mask, then the actual coefficient tuple. The kernels may depend on these public choices but not on an opposite input.

    def nativeStochasticSuccess (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (responses : (mask : Fin k → Bool) →
      RawCoefficients (NativeExperiment.maskSet mask) (ZeroInformation.Bits R) →
      Responses (Fin k) R O N) : ℝ :=
…

    Mentions: OAI.MaxCutGames.Clean.NativeExperiment.maskSet, OAI.MaxCutGames.Clean.StochasticBound.Responses

  54. theorem OAI.MaxCutGames.Clean.StochasticBound.expectation_mono_inline_StochasticBound line 732
  55. theorem OAI.MaxCutGames.Clean.StochasticBound.native_stochastic_le_deterministic line 741

    Source documentation

    The deterministic witness family is indexed by the pre-question public data only. No single global deterministic strategy is claimed here.

    theorem native_stochastic_le_deterministic
    (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (responses : (mask : Fin k → Bool) →
      RawCoefficients (NativeExperiment.maskSet mask) (ZeroInformation.Bits R) →
      Responses (Fin k) R O N) :
    ∃ strategy : NativeExperiment.MaskStrategy k R O N,
      nativeStochasticSuccess k μ g β hβ₀ hβ₁ responses ≤
        NativeExperiment.success k μ g β hβ₀ hβ₁ strategy := by
…

    Mentions: OAI.MaxCutGames.Clean.NativeExperiment.maskSet, OAI.MaxCutGames.Clean.StochasticBound.Responses, OAI.MaxCutGames.Clean.NativeExperiment.MaskStrategy, OAI.MaxCutGames.Clean.StochasticBound.nativeStochasticSuccess, OAI.MaxCutGames.Clean.NativeExperiment.success

  56. theorem OAI.MaxCutGames.Clean.StochasticBound.native_stochastic_le_mask_moment line 766

    Source documentation

    Stochastic kernels satisfy the same exact clean-mask moment as deterministic ones. The only supplied rate is for the actual ordinary repeated incidence game.

    theorem native_stochastic_le_mask_moment
    (k : ℕ) (μ : FiniteDistribution (O × Fin 3))
    (g : IncidenceExtraction.Incidence O N)
    (β : ℝ) (hβ₀ : 0 ≤ β) (hβ₁ : β ≤ 1)
    (responses : (mask : Fin k → Bool) →
      RawCoefficients (NativeExperiment.maskSet mask) (ZeroInformation.Bits R) →
      Responses (Fin k) R O N)
    (distinct : ∀ o i j, g.name o i = g.name o j → i = j) (ρ : ℝ)
    (rate : ∀ n, ((incidenceGame g (μ.pushforward (incidence g.name))).repetition n).value ≤ ρ ^ n) :
    nativeStochasticSuccess k μ g β hβ₀ hβ₁ responses ≤
      (1 - cleanProbability β (ZeroInformation.Bits R) * (1 - ρ)) ^ k := by
…

    Mentions: OAI.MaxCutGames.Clean.NativeExperiment.maskSet, OAI.MaxCutGames.Clean.StochasticBound.Responses, OAI.MaxCutGames.Clean.StochasticBound.nativeStochasticSuccess, OAI.MaxCutGames.Clean.cleanProbability