OAI/Computability/MaxCut/Games/ActualAdviceStochasticBridge.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Actual randomized point policies are transported locally into Boolean answer kernels. Complete response tables are selected only after public advice is fixed and before the remaining questions. No global deterministic policy independent of public advice is asserted or needed for this upper bound.

  1. instance OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.sourceAnswerNonempty line 25
  2. instance OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.targetAnswerNonempty line 26
  3. structure OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.Policies line 29
  4. def OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.extendTargetKernel line 36
  5. theorem OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.extendTargetKernel_apply line 46
  6. def OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.firstResponse line 55
  7. def OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.secondResponse line 63
  8. theorem OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.decodeFirstMap_actual line 73
  9. theorem OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.decodeSecondMap_actual line 93
  10. theorem OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.firstResponse_actual line 104
  11. theorem OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.secondResponse_actual line 116
  12. def OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.fixedMapSuccess line 129

    Source documentation

    Two private finite answer draws, after receiving the respective actual question and linear row map. Acceptance is equality under the real projection.

    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.ActualAdviceStochasticBridge.Policies

  13. theorem OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.fixedMapSuccess_le line 138
  14. def OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.responses line 182
  15. def OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.success line 190
  16. theorem OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.success_le_native_stochastic line 198
  17. theorem OAI.MaxCutGames.Clean.ActualAdviceStochasticBridge.success_le_some_native line 222
  18. def OAI.MaxCutGames.Soundness.LinearMapDensity.uniformMean line 251
  19. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.uniformMean_eq_sum_div_card line 254
  20. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.uniformMean_comm line 258
  21. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.uniformMean_const_mul line 264
  22. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.uniformMean_const line 268
  23. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.restriction_surjective line 273
  24. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.restriction_zero_iff line 280
  25. def OAI.MaxCutGames.Soundness.LinearMapDensity.pullbackMap line 291

    Source documentation

    Pulling back a map along a projection produces a map annihilating its kernel.

    def pullbackMap {V : Type*} [AddCommGroup V] [Module (ZMod 2) V]
    (π : E →ₗ[ZMod 2] V) (B : V →ₗ[ZMod 2] R) :
    {M : E →ₗ[ZMod 2] R // π.ker ≤ M.ker} :=
…
  26. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.pullbackMap_bijective line 303

    Source documentation

    The pullback map is a bijection onto the genuine kernel-annihilator event. This connects the density calculation to uniform maps on the partner space.

    theorem pullbackMap_bijective {V : Type*} [AddCommGroup V] [Module (ZMod 2) V]
    (π : E →ₗ[ZMod 2] V) (hπ : Function.Surjective π) :
    Function.Bijective (pullbackMap (R := R) π) := by
…

    Mentions: OAI.MaxCutGames.Soundness.LinearMapDensity.pullbackMap

  27. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.annihilator_count line 326
  28. def OAI.MaxCutGames.Soundness.LinearMapDensity.kernelDensity line 341
  29. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.kernelDensity_mean line 347
  30. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.kernelDensity_product line 365

    Source documentation

    Pointwise overlap formula, using the actual dimension formula for subspaces.

    theorem kernelDensity_product (K L : Submodule (ZMod 2) E)
    (M : E →ₗ[ZMod 2] R) :
    kernelDensity K M * kernelDensity L M =
      (2 : ℝ) ^ (Module.finrank (ZMod 2) R * Module.finrank (ZMod 2) ↥(K ⊓ L : Submodule (ZMod 2) E)) *
        kernelDensity (K ⊔ L) M := by
…

    Mentions: OAI.MaxCutGames.Soundness.LinearMapDensity.kernelDensity

  31. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.kernelDensity_pair_mean line 390

    Source documentation

    The two-kernel second-moment identity for the uniform law on all genuine linear maps E→R. No annihilator probability is a hypothesis.

    theorem kernelDensity_pair_mean [Fintype (E →ₗ[ZMod 2] R)]
    (K L : Submodule (ZMod 2) E) :
    uniformMean (fun M : E →ₗ[ZMod 2] R => kernelDensity K M * kernelDensity L M) =
      (2 : ℝ) ^ (Module.finrank (ZMod 2) R * Module.finrank (ZMod 2) ↥(K ⊓ L : Submodule (ZMod 2) E)) := by
…

    Mentions: OAI.MaxCutGames.Soundness.LinearMapDensity.uniformMean, OAI.MaxCutGames.Soundness.LinearMapDensity.kernelDensity

  32. def OAI.MaxCutGames.Soundness.LinearMapDensity.mixtureDensity line 397
  33. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.mixtureDensity_mean line 401
  34. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.mixtureDensity_second_moment line 412

    Source documentation

    Lemma 6.3's exact second-moment identity for an arbitrary finite uniform list of genuine kernel subspaces. The two partner indices are independent because the right side is an iterated uniform expectation.

    theorem mixtureDensity_second_moment {Partner : Type w} [Fintype Partner]
    [Fintype (E →ₗ[ZMod 2] R)] (kernels : Partner → Submodule (ZMod 2) E) :
    uniformMean (fun M : E →ₗ[ZMod 2] R => (mixtureDensity kernels M) ^ 2) =
      uniformMean (fun p => uniformMean (fun q => (2 : ℝ) ^
        (Module.finrank (ZMod 2) R * Module.finrank (ZMod 2) ↥(kernels p ⊓ kernels q : Submodule (ZMod 2) E)))) := by
…

    Mentions: OAI.MaxCutGames.Soundness.LinearMapDensity.uniformMean, OAI.MaxCutGames.Soundness.LinearMapDensity.mixtureDensity

  35. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.kernelDensity_weighted_mean line 431
  36. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.pullback_uniformMean line 462
  37. theorem OAI.MaxCutGames.Soundness.LinearMapDensity.mixture_pullback_uniformMean line 473
  38. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.density_variance_identity line 506

    Source documentation

    Centering a normalized density subtracts exactly one from its second moment.

    theorem density_variance_identity (s : Finset ι) (hs : s.Nonempty)
    (d : ι → ℝ) (hd : (𝔼 i ∈ s, d i) = 1) :
    (𝔼 i ∈ s, (d i - 1) ^ 2) = (𝔼 i ∈ s, d i ^ 2) - 1 := by
…
  39. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.density_variance_le line 520
  40. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.bounded_test_second_moment line 527
  41. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.bounded_test_centered_square line 535

    Source documentation

    Cauchy--Schwarz for an arbitrary whole-map test, in squared form.

    theorem bounded_test_centered_square (s : Finset ι) (hs : s.Nonempty)
    (d H : ι → ℝ) (ε : ℝ) (hd : (𝔼 i ∈ s, d i) = 1)
    (hsecond : (𝔼 i ∈ s, d i ^ 2) ≤ 1 + ε)
    (hH : ∀ i ∈ s, |H i| ≤ 1) :
    (𝔼 i ∈ s, H i * (d i - 1)) ^ 2 ≤ ε := by
…
  42. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.bounded_test_expectation_comparison line 549

    Source documentation

    The actual difference of the two normalized finite expectations.

    theorem bounded_test_expectation_comparison (s : Finset ι) (hs : s.Nonempty)
    (d H : ι → ℝ) (ε : ℝ) (hd : (𝔼 i ∈ s, d i) = 1)
    (hsecond : (𝔼 i ∈ s, d i ^ 2) ≤ 1 + ε)
    (hH : ∀ i ∈ s, |H i| ≤ 1) :
    |(𝔼 i ∈ s, H i * d i) - (𝔼 i ∈ s, H i)| ≤ Real.sqrt ε := by
…
  43. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.comparison_error_le_quarter line 564

    Source documentation

    The squared parameter inequality implies error at most θ/4.

    theorem comparison_error_le_quarter (ε θ : ℝ) (hθ : 0 ≤ θ)
    (hε : ε ≤ (θ / 4) ^ 2) : Real.sqrt ε ≤ θ / 4 := by
…
  44. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.parameter_error_le_quarter line 569

    Source documentation

    The real inequality selected by equation (4.4) gives its stated error.

    theorem parameter_error_le_quarter (t k cap θ : ℝ) (hk : 0 < k)
    (hθ : 0 < θ) (hsize : 16 * t ^ 2 * cap / θ ^ 2 ≤ k) :
    Real.sqrt (t ^ 2 / k * cap) ≤ θ / 4 := by
…
  45. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.map_law_parameter_error line 579
  46. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.bounded_test_expectation_quarter line 586
  47. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.transferred_signal_lower line 596

    Source documentation

    A signal at least θ under the uniform law stays at least θ/2 after transfer.

    theorem transferred_signal_lower (s : Finset ι) (hs : s.Nonempty)
    (d H : ι → ℝ) (ε θ : ℝ) (hθ : 0 ≤ θ)
    (hε : ε ≤ (θ / 4) ^ 2) (hd : (𝔼 i ∈ s, d i) = 1)
    (hsecond : (𝔼 i ∈ s, d i ^ 2) ≤ 1 + ε)
    (hH : ∀ i ∈ s, |H i| ≤ 1) (hsignal : θ ≤ (𝔼 i ∈ s, H i)) :
    θ / 2 ≤ (𝔼 i ∈ s, H i * d i) := by
…
  48. def OAI.MaxCutGames.Soundness.ExpectationComparison.wholeMapTest line 607

    Source documentation

    Equation (6.10), allowing the chosen index and sign to depend on the row.

    def wholeMapTest {Map Row Column Index : Type*} (row : Map → Row)
    (column : Map → Column) (sign : Row → ℝ) (value : Row → Column → ℝ)
    (chosen : Row → Index) (character : Index → Column → ℝ) (M : Map) : ℝ :=
…
  49. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.wholeMapTest_abs_le_one line 612
  50. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.wholeMapTest_comparison line 630

    Source documentation

    Instantiate comparison with equation (6.10), including its row-dependent index.

    theorem wholeMapTest_comparison {Map Row Column Index : Type*}
    (s : Finset Map) (hs : s.Nonempty) (d : Map → ℝ) (ε : ℝ)
    (row : Map → Row) (column : Map → Column) (sign : Row → ℝ)
    (value : Row → Column → ℝ) (chosen : Row → Index)
    (character : Index → Column → ℝ)
    (hd : (𝔼 M ∈ s, d M) = 1)
    (hsecond : (𝔼 M ∈ s, d M ^ 2) ≤ 1 + ε)
    (hsign : ∀ r, |sign r| ≤ 1) (hvalue : ∀ r c, |value r c| ≤ 1)
    (hcharacter : ∀ t c, |character t c| ≤ 1) :
    |(𝔼 M ∈ s, wholeMapTest row column sign value chosen character M * d M) -
      (𝔼 M ∈ s, wholeMapTest row column sign value chosen character M)|
      ≤ Real.sqrt ε := by
…

    Mentions: OAI.MaxCutGames.Soundness.ExpectationComparison.wholeMapTest

  51. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.averaged_expectation_comparison line 648

    Source documentation

    Average a uniform per-U error, allowing the map sample space to depend on U.

    theorem averaged_expectation_comparison {U : Type*} (Map : U → Type*)
    (us : Finset U) (hus : us.Nonempty) (maps : (u : U) → Finset (Map u))
    (hmaps : ∀ u ∈ us, (maps u).Nonempty)
    (d H : (u : U) → Map u → ℝ) (ε : ℝ)
    (hd : ∀ u ∈ us, (𝔼 M ∈ maps u, d u M) = 1)
    (hsecond : ∀ u ∈ us, (𝔼 M ∈ maps u, d u M ^ 2) ≤ 1 + ε)
    (hH : ∀ u ∈ us, ∀ M ∈ maps u, |H u M| ≤ 1) :
    |(𝔼 u ∈ us, 𝔼 M ∈ maps u, H u M * d u M) -
      (𝔼 u ∈ us, 𝔼 M ∈ maps u, H u M)| ≤ Real.sqrt ε := by
…
  52. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.averaged_transferred_signal_lower line 669

    Source documentation

    Equation (6.11): only the signal averaged over U is assumed large.

    theorem averaged_transferred_signal_lower {U : Type*} (Map : U → Type*)
    (us : Finset U) (hus : us.Nonempty) (maps : (u : U) → Finset (Map u))
    (hmaps : ∀ u ∈ us, (maps u).Nonempty)
    (d H : (u : U) → Map u → ℝ) (ε θ : ℝ) (hθ : 0 ≤ θ)
    (hε : ε ≤ (θ / 4) ^ 2)
    (hd : ∀ u ∈ us, (𝔼 M ∈ maps u, d u M) = 1)
    (hsecond : ∀ u ∈ us, (𝔼 M ∈ maps u, d u M ^ 2) ≤ 1 + ε)
    (hH : ∀ u ∈ us, ∀ M ∈ maps u, |H u M| ≤ 1)
    (hsignal : θ ≤ (𝔼 u ∈ us, 𝔼 M ∈ maps u, H u M)) :
    θ / 2 ≤ (𝔼 u ∈ us, 𝔼 M ∈ maps u, H u M * d u M) := by
…
  53. theorem OAI.MaxCutGames.Soundness.ExpectationComparison.uniform_expect_eq_sum_div_card line 686

    Source documentation

    Uniform finite means in the quotient-of-sums convention.

    theorem uniform_expect_eq_sum_div_card [Fintype ι] (f : ι → ℝ) :
    (𝔼 i, f i) = (∑ i, f i) / (Fintype.card ι : ℝ) :=
…