OAI/Computability/MaxCut/Games/BaseDetection.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

From full character lifts to linear-map detection

If a target linear map is injective on the logical alphabet, a linear left inverse of that restriction turns all logical characters into a full lift. Detection by this lift implies that the target map does not annihilate the noise. The left inverse is proved to exist by the vector-space splitting theorem; it is not an additional premise.

  1. def OAI.MaxCutGames.Gadget.BaseDetection.logicalCharacters line 19

    Source documentation

    Turn the fixed generic vector subspace into its actual logical characters.

    def logicalCharacters (S : Submodule (ZMod 2) (Vec F)) :
    Submodule (ZMod 2) (BinaryDual (F := F)) :=
…
  2. theorem OAI.MaxCutGames.Gadget.BaseDetection.traceSpace_logicalCharacters line 24
  3. theorem OAI.MaxCutGames.Gadget.BaseDetection.logicalCharacters_finrank line 29
  4. theorem OAI.MaxCutGames.Gadget.BaseDetection.theta_pos line 34
  5. theorem OAI.MaxCutGames.Gadget.BaseDetection.full_lift_detection line 42

    Source documentation

    All probabilities concern the actual recursive noise choices. The field and generic top space satisfy separately proved finite-field properties; no probability estimate for the whole recursive gadget is an input.

    theorem full_lift_detection :
    let J : BlockOrientationIndex F → Vec F →ₗ[ZMod 2] Vec F × Vec F :=
…
  6. def OAI.MaxCutGames.Gadget.Quotient.shiftKernel line 99

    Source documentation

    The logical kernel viewed as a submodule of the ambient input space.

    def shiftKernel (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B) : Submodule 𝕜 P :=
…
  7. abbrev OAI.MaxCutGames.Gadget.Quotient.Space line 102
  8. def OAI.MaxCutGames.Gadget.Quotient.projection line 104
  9. theorem OAI.MaxCutGames.Gadget.Quotient.projection_surjective line 107
  10. theorem OAI.MaxCutGames.Gadget.Quotient.mem_shiftKernel line 110
  11. theorem OAI.MaxCutGames.Gadget.Quotient.projection_eq_zero line 113
  12. def OAI.MaxCutGames.Gadget.Quotient.quotientShift line 125

    Source documentation

    Inclusion of the quotient shift space into the ambient quotient.

    def quotientShift (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B) :
    (R ⧸ LinearMap.ker lam) →ₗ[𝕜] Space R lam :=
…

    Mentions: OAI.MaxCutGames.Gadget.Quotient.Space

  13. theorem OAI.MaxCutGames.Gadget.Quotient.quotientShift_mk line 131
  14. def OAI.MaxCutGames.Gadget.Quotient.logicalShift line 135

    Source documentation

    The logical alphabet is realized as actual linear shifts of the quotient.

    noncomputable def logicalShift (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (hlam : Function.Surjective lam) : B →ₗ[𝕜] Space R lam :=
…

    Mentions: OAI.MaxCutGames.Gadget.Quotient.Space

  15. theorem OAI.MaxCutGames.Gadget.Quotient.logicalShift_lambda line 139
  16. theorem OAI.MaxCutGames.Gadget.Quotient.logicalShift_injective line 144
  17. def OAI.MaxCutGames.Gadget.Quotient.Equivariant line 157

    Source documentation

    Equivariance under every allowed shift; no linearity of C is assumed.

    def Equivariant (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B) (C : P → B) : Prop :=
…
  18. theorem OAI.MaxCutGames.Gadget.Quotient.difference_shift line 161

    Source documentation

    An output difference is unchanged by every logical shift.

    theorem difference_shift (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (C : P → B) (hC : Equivariant R lam C) (u a : P) (h : R) :
    C (u + (h : P) + a) - C (u + (h : P)) = C (u + a) - C u := by
…

    Mentions: OAI.MaxCutGames.Gadget.Quotient.Equivariant

  19. def OAI.MaxCutGames.Gadget.Quotient.conditionedShiftEquiv line 170

    Source documentation

    Translating by a logical shift bijects output fibers even after conditioning on an arbitrary shift-invariant event.

    def conditionedShiftEquiv (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (C : P → B) (hC : Equivariant R lam C) (D : P → Prop)
    (hD : ∀ (u : P) (h : R), D (u + (h : P)) ↔ D u) (b : B) (h : R) :
    {u : P // C u = b ∧ D u} ≃ {u : P // C u = b + lam h ∧ D u} where
…

    Mentions: OAI.MaxCutGames.Gadget.Quotient.Equivariant

  20. def OAI.MaxCutGames.Gadget.Quotient.conditionedFiberEquiv line 186

    Source documentation

    Surjectivity makes all output fibers equally large inside an invariant event, without assuming that this event has positive probability.

    noncomputable def conditionedFiberEquiv (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (hlam : Function.Surjective lam) (C : P → B) (hC : Equivariant R lam C)
    (D : P → Prop) (hD : ∀ (u : P) (h : R), D (u + (h : P)) ↔ D u)
    (b c : B) : {u : P // C u = b ∧ D u} ≃ {u : P // C u = c ∧ D u} := by
…

    Mentions: OAI.MaxCutGames.Gadget.Quotient.Equivariant

  21. theorem OAI.MaxCutGames.Gadget.Quotient.conditioned_fiber_card line 196
  22. theorem OAI.MaxCutGames.Gadget.Quotient.output_fiber_card line 203
  23. theorem OAI.MaxCutGames.Gadget.Quotient.difference_fiber_card line 211

    Source documentation

    Fixing the additive perturbation and the observed difference leaves the initial output uniform: the joint fibers have equal cardinality for all outputs.

    theorem difference_fiber_card (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (hlam : Function.Surjective lam) (C : P → B) (hC : Equivariant R lam C)
    (a : P) (d b c : B) :
    Nat.card {u : P // C u = b ∧ C (u + a) - C u = d} =
      Nat.card {u : P // C u = c ∧ C (u + a) - C u = d} := by
…

    Mentions: OAI.MaxCutGames.Gadget.Quotient.Equivariant

  24. def OAI.MaxCutGames.Gadget.Quotient.conditionedSigmaEquiv line 221

    Source documentation

    Splitting an invariant event into its output fibers.

    def conditionedSigmaEquiv (C : P → B) (D : P → Prop) :
    {u : P // D u} ≃ Σ b : B, {u : P // C u = b ∧ D u} where
…
  25. def OAI.MaxCutGames.Gadget.Quotient.conditionedProductEquiv line 229

    Source documentation

    An invariant event factors as an independent logical output and one fiber.

    noncomputable def conditionedProductEquiv (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (hlam : Function.Surjective lam) (C : P → B) (hC : Equivariant R lam C)
    (D : P → Prop) (hD : ∀ (u : P) (h : R), D (u + (h : P)) ↔ D u) (b : B) :
    {u : P // D u} ≃ B × {u : P // C u = b ∧ D u} :=
…

    Mentions: OAI.MaxCutGames.Gadget.Quotient.Equivariant

  26. theorem OAI.MaxCutGames.Gadget.Quotient.conditionedProductEquiv_fst line 237
  27. theorem OAI.MaxCutGames.Gadget.Quotient.conditioned_card_factorization line 244

    Source documentation

    Exact counting factorization underlying the conditional uniform law.

    theorem conditioned_card_factorization [Finite P] [Finite B]
    (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (hlam : Function.Surjective lam) (C : P → B) (hC : Equivariant R lam C)
    (D : P → Prop) (hD : ∀ (u : P) (h : R), D (u + (h : P)) ↔ D u) (b : B) :
    Nat.card {u : P // D u} = Nat.card B * Nat.card {u : P // C u = b ∧ D u} := by
…

    Mentions: OAI.MaxCutGames.Gadget.Quotient.Equivariant

  28. theorem OAI.MaxCutGames.Gadget.Quotient.difference_card_factorization line 252
  29. theorem OAI.MaxCutGames.Gadget.Quotient.output_constant_on_fibers line 262
  30. def OAI.MaxCutGames.Gadget.Quotient.output line 270
  31. theorem OAI.MaxCutGames.Gadget.Quotient.output_projection line 275
  32. theorem OAI.MaxCutGames.Gadget.Quotient.output_equivariant line 279
  33. theorem OAI.MaxCutGames.Gadget.Quotient.change_iff line 289

    Source documentation

    Noise pushforward preserves the change event pointwise, before averaging.

    theorem change_iff (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (C : P → B) (hC : Equivariant R lam C) (u a : P) :
    (output R lam C hC (projection R lam u + projection R lam a) ≠
      output R lam C hC (projection R lam u)) ↔ C (u + a) ≠ C u := by
…

    Mentions: OAI.MaxCutGames.Gadget.Quotient.Equivariant, OAI.MaxCutGames.Gadget.Quotient.output, OAI.MaxCutGames.Gadget.Quotient.projection

  34. theorem OAI.MaxCutGames.Gadget.Quotient.character_pullback_shift line 296

    Source documentation

    Pulling a quotient character back recovers its prescribed logical value.

    theorem character_pullback_shift (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (hlam : Function.Surjective lam) (g : Space R lam →ₗ[𝕜] 𝕜) (h : R) :
    (g.comp (projection R lam)) (h : P) =
      (g.comp (logicalShift R lam hlam)) (lam h) := by
…

    Mentions: OAI.MaxCutGames.Gadget.Quotient.Space, OAI.MaxCutGames.Gadget.Quotient.projection, OAI.MaxCutGames.Gadget.Quotient.logicalShift

  35. theorem OAI.MaxCutGames.Gadget.Quotient.detection_iff line 304

    Source documentation

    Pullback preserves the detection event of an already selected family of quotient characters, including a section of the logical restriction map.

    theorem detection_iff {I : Type*} (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B)
    (family : I → Space R lam →ₗ[𝕜] 𝕜) (a : P) :
    (∃ i, family i (projection R lam a) ≠ 0) ↔
      ∃ i, (family i).comp (projection R lam) a ≠ 0 := Iff.rfl

    Mentions: OAI.MaxCutGames.Gadget.Quotient.Space, OAI.MaxCutGames.Gadget.Quotient.projection

  36. def OAI.MaxCutGames.Gadget.Quotient.fiberMap line 310

    Source documentation

    Translation by the logical kernel parametrizes a quotient fiber.

    def fiberMap (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B) (a : P) :
    shiftKernel R lam → {u : P // projection R lam u = projection R lam a} :=
…

    Mentions: OAI.MaxCutGames.Gadget.Quotient.shiftKernel, OAI.MaxCutGames.Gadget.Quotient.projection

  37. theorem OAI.MaxCutGames.Gadget.Quotient.fiberMap_bijective line 317
  38. theorem OAI.MaxCutGames.Gadget.Quotient.fiber_card line 331

    Source documentation

    Every fiber has the same cardinality, justifying uniform-input pushforward.

    theorem fiber_card (R : Submodule 𝕜 P) (lam : R →ₗ[𝕜] B) (x : Space R lam) :
    Nat.card {u : P // projection R lam u = x} = Nat.card (shiftKernel R lam) := by
…

    Mentions: OAI.MaxCutGames.Gadget.Quotient.Space, OAI.MaxCutGames.Gadget.Quotient.projection, OAI.MaxCutGames.Gadget.Quotient.shiftKernel

  39. def OAI.MaxCutGames.Gadget.StageQuotient.shifts line 345
  40. def OAI.MaxCutGames.Gadget.StageQuotient.shiftEquiv line 347
  41. theorem OAI.MaxCutGames.Gadget.StageQuotient.shiftEquiv_coe line 350
  42. theorem OAI.MaxCutGames.Gadget.StageQuotient.embed_shiftEquiv_symm line 353
  43. def OAI.MaxCutGames.Gadget.StageQuotient.logical line 357
  44. theorem OAI.MaxCutGames.Gadget.StageQuotient.logical_shiftEquiv line 360
  45. theorem OAI.MaxCutGames.Gadget.StageQuotient.logical_surjective line 364
  46. theorem OAI.MaxCutGames.Gadget.StageQuotient.equivariant line 369
  47. abbrev OAI.MaxCutGames.Gadget.StageQuotient.Space line 376
  48. def OAI.MaxCutGames.Gadget.StageQuotient.projection line 378
  49. theorem OAI.MaxCutGames.Gadget.StageQuotient.projection_surjective line 381
  50. instance OAI.MaxCutGames.Gadget.StageQuotient.spaceFinite line 384
  51. def OAI.MaxCutGames.Gadget.StageQuotient.shift line 387
  52. theorem OAI.MaxCutGames.Gadget.StageQuotient.shift_injective line 390
  53. theorem OAI.MaxCutGames.Gadget.StageQuotient.shift_logical line 393
  54. def OAI.MaxCutGames.Gadget.StageQuotient.output line 399
  55. theorem OAI.MaxCutGames.Gadget.StageQuotient.output_projection line 402
  56. theorem OAI.MaxCutGames.Gadget.StageQuotient.output_equivariant line 405
  57. def OAI.MaxCutGames.Gadget.StageQuotient.noise line 411

    Source documentation

    Original finite noise choices, pushed through the actual quotient map.

    noncomputable def noise (s : Stage k B) : s.Noise → Space s :=
…

    Mentions: OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.StageQuotient.Space

  58. theorem OAI.MaxCutGames.Gadget.StageQuotient.noise_change_iff line 414
  59. theorem OAI.MaxCutGames.Gadget.StageQuotient.character_logical line 419
  60. theorem OAI.MaxCutGames.Gadget.StageQuotient.noise_detection_iff line 423
  61. def OAI.MaxCutGames.Gadget.StageQuotient.toStage line 429

    Source documentation

    The quotient is again a finite stage; its logical map is now the identity.

    noncomputable def toStage [Finite B] (s : Stage k B) : Stage k B where
…

    Mentions: OAI.MaxCutGames.Gadget.Stage

  62. def OAI.MaxCutGames.Gadget.DetectionBridge.IsFullLift line 462

    Source documentation

    Every logical character is extended to the ambient input space.

    def IsFullLift (ι : B →ₗ[K] V)
    (ψ : Module.Dual K B →ₗ[K] Module.Dual K V) : Prop :=
…
  63. def OAI.MaxCutGames.Gadget.DetectionBridge.characterDetection line 468

    Source documentation

    Detection by any member of a character family. Classical decidability only selects an event indicator on the finite noise sample space.

    noncomputable def characterDetection (noise : Ω → V)
    (ψ : Module.Dual K B →ₗ[K] Module.Dual K V) : ℚ := by
…
  64. theorem OAI.MaxCutGames.Gadget.DetectionBridge.exists_leftInverse_of_logical_injective line 473
  65. theorem OAI.MaxCutGames.Gadget.DetectionBridge.fullLift_of_leftInverse line 479

    Source documentation

    The left inverse supplies an actual full character lift through T.

    theorem fullLift_of_leftInverse (ι : B →ₗ[K] V) (T : V →ₗ[K] E)
    (l : E →ₗ[K] B) (hleft : l.comp (T.comp ι) = LinearMap.id) :
    IsFullLift ι (l.comp T).dualMap := by
…

    Mentions: OAI.MaxCutGames.Gadget.DetectionBridge.IsFullLift

  66. theorem OAI.MaxCutGames.Gadget.DetectionBridge.target_detection_of_full_lift_bound line 489

    Source documentation

    A full-lift detection guarantee transfers to every target map injective on the logical alphabet.

    theorem target_detection_of_full_lift_bound [DecidableEq E]
    (noise : Ω → V) (ι : B →ₗ[K] V) (T : V →ₗ[K] E) (q : ℚ)
    (hfull : ∀ ψ : Module.Dual K B →ₗ[K] Module.Dual K V,
      IsFullLift ι ψ → q ≤ characterDetection noise ψ)
    (hinjective : Function.Injective (T.comp ι)) :
    q ≤ probability (fun ω => T (noise ω) ≠ 0) := by
…

    Mentions: OAI.MaxCutGames.Gadget.DetectionBridge.IsFullLift, OAI.MaxCutGames.Gadget.DetectionBridge.characterDetection

  67. theorem OAI.MaxCutGames.Gadget.DetectionBridge.target_detection_of_retraction_bound line 510

    Source documentation

    Equivalent useful interface when the recursive calculation already gives detection of every vector-valued linear retraction of the logical inclusion.

    theorem target_detection_of_retraction_bound [DecidableEq B] [DecidableEq E]
    (noise : Ω → V) (ι : B →ₗ[K] V) (T : V →ₗ[K] E) (q : ℚ)
    (hretract : ∀ L : V →ₗ[K] B, L.comp ι = LinearMap.id →
      q ≤ probability (fun ω => L (noise ω) ≠ 0))
    (hinjective : Function.Injective (T.comp ι)) :
    q ≤ probability (fun ω => T (noise ω) ≠ 0) := by
…
  68. def OAI.MaxCutGames.Gadget.QuotientDetection.pullbackFullLift line 548
  69. theorem OAI.MaxCutGames.Gadget.QuotientDetection.pullback_detection_iff line 563
  70. theorem OAI.MaxCutGames.Gadget.QuotientDetection.full_detection_after_quotient line 577

    Source documentation

    Any checked full-lift probability bound before quotienting applies to every full family on the actual quotient, on the same noise sampler.

    theorem full_detection_after_quotient (s : Stage k B) [Fintype s.Noise] (q : ℚ)
    (hfull : ∀ L : Lift s (⊤ : Submodule k (Module.Dual k B)),
      q ≤ probability (fun n => ∃ z, L.family z (s.noise n) ≠ 0))
    (ψ : Module.Dual k B →ₗ[k] Module.Dual k (StageQuotient.Space s))
    (hψ : IsFullLift (StageQuotient.shift s) ψ) :
    q ≤ characterDetection (StageQuotient.noise s) ψ := by
…

    Mentions: OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.Lift, OAI.MaxCutGames.Gadget.StageQuotient.Space, OAI.MaxCutGames.Gadget.StageQuotient.shift, OAI.MaxCutGames.Gadget.StageQuotient.noise

  71. theorem OAI.MaxCutGames.Gadget.QuotientDetection.target_detection_after_quotient line 590

    Source documentation

    The form consumed by the injection enlargement: injectivity on the base logical alphabet suffices for the same detection probability.

    theorem target_detection_after_quotient (s : Stage k B) [Fintype s.Noise]
    {E : Type*} [AddCommGroup E] [Module k E] [DecidableEq E]
    (T : StageQuotient.Space s →ₗ[k] E) (q : ℚ)
    (hfull : ∀ L : Lift s (⊤ : Submodule k (Module.Dual k B)),
      q ≤ probability (fun n => ∃ z, L.family z (s.noise n) ≠ 0))
    (hinj : Function.Injective (T.comp (StageQuotient.shift s))) :
    q ≤ probability (fun n => T (StageQuotient.noise s n) ≠ 0) := by
…

    Mentions: OAI.MaxCutGames.Gadget.Stage, OAI.MaxCutGames.Gadget.StageQuotient.Space, OAI.MaxCutGames.Gadget.Lift, OAI.MaxCutGames.Gadget.StageQuotient.shift, OAI.MaxCutGames.Gadget.StageQuotient.noise

  72. theorem OAI.MaxCutGames.Gadget.EmbeddedConditional.expect_uniform_output_embedded line 614

    Source documentation

    Exact conditional uniformity for an embedded carrier of logical shifts. No injectivity of the embedding is needed for this averaging statement.

    theorem expect_uniform_output_embedded (e : R →ₗ[k] P) (lam : R →ₗ[k] B)
    (hlam : Function.Surjective lam) (C : P → B)
    (hC : ∀ u h, C (u + e h) = C u + lam h)
    (D : P → Z) (hD : ∀ u h, D (u + e h) = D u)
    (f : B → Z → M) :
    (𝔼 u, f (C u) (D u)) = 𝔼 u, 𝔼 b : B, f b (D u) := by
…
  73. theorem OAI.MaxCutGames.Gadget.EmbeddedConditional.expect_equivariant_output line 639

    Source documentation

    Unconditional uniformity is the constant-observable instance.

    theorem expect_equivariant_output (e : R →ₗ[k] P) (lam : R →ₗ[k] B)
    (hlam : Function.Surjective lam) (C : P → B)
    (hC : ∀ u h, C (u + e h) = C u + lam h) (f : B → M) :
    (𝔼 u, f (C u)) = 𝔼 b : B, f b := by
…
  74. theorem OAI.MaxCutGames.Gadget.EmbeddedConditional.expect_linear_surjective line 648

    Source documentation

    Surjective linear maps send uniform finite input to uniform output.

    theorem expect_linear_surjective (f : P →ₗ[k] B) (hf : Function.Surjective f)
    (test : B → M) : (𝔼 u, test (f u)) = 𝔼 b : B, test b := by
…
  75. theorem OAI.MaxCutGames.Gadget.EmbeddedConditional.expect_uniform_difference_embedded line 655

    Source documentation

    Fixed-perturbation conditional uniformity without a range conversion.

    theorem expect_uniform_difference_embedded (e : R →ₗ[k] P) (lam : R →ₗ[k] B)
    (hlam : Function.Surjective lam) (C : P → B)
    (hC : ∀ u h, C (u + e h) = C u + lam h) (a : P) (f : B → B → M) :
    (𝔼 u, f (C u) (C (u + a) - C u)) =
      𝔼 u, 𝔼 b : B, f b (C (u + a) - C u) := by
…
  76. def OAI.MaxCutGames.Gadget.NonlinearRecurrence.change line 679
  77. theorem OAI.MaxCutGames.Gadget.NonlinearRecurrence.change_zero line 683
  78. theorem OAI.MaxCutGames.Gadget.NonlinearRecurrence.compLeft_surjective line 687
  79. theorem OAI.MaxCutGames.Gadget.NonlinearRecurrence.aggregate_single line 694
  80. theorem OAI.MaxCutGames.Gadget.NonlinearRecurrence.child_outputs_perturb line 702
  81. theorem OAI.MaxCutGames.Gadget.NonlinearRecurrence.parent_output_perturb line 714
  82. theorem OAI.MaxCutGames.Gadget.NonlinearRecurrence.expect_change_at_index line 722

    Source documentation

    The exact conditional-uniform and coordinate-marginal law for a fixed selected index and fixed child perturbation.

    theorem expect_change_at_index (J : I → B →ₗ[k] X × B)
    (hJ : Function.Surjective (aggregate J)) (e : R →ₗ[k] P) (lam : R →ₗ[k] B)
    (hlam : Function.Surjective lam) (C : P → B)
    (hC : ∀ u h, C (u + e h) = C u + lam h)
    (F : X × B → B) (i : I) (a : P) :
    (𝔼 u : I → P,
      change F (aggregate J (fun j => C (u j))) (J i (C (u i + a) - C (u i)))) =
      𝔼 x : P, 𝔼 z : X × B, change F z (J i (C (x + a) - C x)) := by
…

    Mentions: OAI.MaxCutGames.Gadget.aggregate, OAI.MaxCutGames.Gadget.NonlinearRecurrence.change

  83. theorem OAI.MaxCutGames.Gadget.NonlinearRecurrence.kernel_all line 766

    Source documentation

    The averaged block kernel includes zero differences by multiplication with their nonzero indicator.

    theorem kernel_all (J : I → B →ₗ[k] X × B) (F : X × B → B) (ρ : ℚ)
    (hk : ∀ d : B, d ≠ 0 → (𝔼 i, 𝔼 z : X × B, change F z (J i d)) = ρ)
    (d : B) :
    (𝔼 i, 𝔼 z : X × B, change F z (J i d)) = ρ * (if d ≠ 0 then 1 else 0) := by
…

    Mentions: OAI.MaxCutGames.Gadget.NonlinearRecurrence.change

  84. theorem OAI.MaxCutGames.Gadget.NonlinearRecurrence.parent_change_recurrence line 778

    Source documentation

    One exact nonlinear recurrence on the actual product input and the actual single-coordinate noise. The only remaining block obligation is hk.

    theorem parent_change_recurrence {N : Type*} [Fintype N]
    (J : I → B →ₗ[k] X × B) (hJ : Function.Surjective (aggregate J))
    (e : R →ₗ[k] P) (lam : R →ₗ[k] B) (hlam : Function.Surjective lam)
    (C : P → B) (hC : ∀ u h, C (u + e h) = C u + lam h)
    (F : X × B → B) (noise : N → P) (ρ : ℚ)
    (hk : ∀ d : B, d ≠ 0 → (𝔼 i, 𝔼 z : X × B, change F z (J i d)) = ρ) :
    (𝔼 i, 𝔼 n : N, 𝔼 u : I → P,
      if F (aggregate J (fun j => C ((u + (Pi.single i (noise n) : I → P)) j))) ≠
        F (aggregate J (fun j => C (u j))) then (1 : ℚ) else 0) =
      ρ * (𝔼 n : N, 𝔼 x : P, if C (x + noise n) ≠ C x then (1 : ℚ) else 0) := by
…

    Mentions: OAI.MaxCutGames.Gadget.aggregate, OAI.MaxCutGames.Gadget.NonlinearRecurrence.change