OAI/Computability/MaxCut/Games/Information.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaxCutGames.Soundness.ZeroInformation.Fibre line 17

   Source documentation

   The complete draw, constrained only by the observations outside the hidden set.

   def Fibre := {sample : P → X //
   …

2. def OAI.MaxCutGames.Soundness.ZeroInformation.Inside line 21

   Source documentation

   At hidden positions the draw is unconstrained.

   def Inside := (j : P) → hidden j = true → X

3. def OAI.MaxCutGames.Soundness.ZeroInformation.Outside line 24

   Source documentation

   The remaining part of a draw, satisfying the outside observation.

   def Outside := {sample : (j : P) → hidden j = false → X //
   …

4. def OAI.MaxCutGames.Soundness.ZeroInformation.fibreInside line 27
5. def OAI.MaxCutGames.Soundness.ZeroInformation.fibreOutside line 30
6. def OAI.MaxCutGames.Soundness.ZeroInformation.assemble line 33
7. theorem OAI.MaxCutGames.Soundness.ZeroInformation.inside_assemble line 43
8. theorem OAI.MaxCutGames.Soundness.ZeroInformation.outside_assemble line 49
9. theorem OAI.MaxCutGames.Soundness.ZeroInformation.assemble_split line 56
10. theorem OAI.MaxCutGames.Soundness.ZeroInformation.fibre_product line 67

    Source documentation

    A fibre is in explicit bijection with the product of unrestricted inside draws and admissible outside draws. This assertion does not posit any independence axiom.

    theorem fibre_product (sample : Fibre hidden reveal observed) :
        ∃ inside : Inside (X := X) hidden, ∃ outside : Outside hidden reveal observed,
    …

    Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.Fibre, OAI.MaxCutGames.Soundness.ZeroInformation.Inside, OAI.MaxCutGames.Soundness.ZeroInformation.Outside

11. def OAI.MaxCutGames.Soundness.ZeroInformation.mass line 78
12. theorem OAI.MaxCutGames.Soundness.ZeroInformation.mass_scale line 82
13. theorem OAI.MaxCutGames.Soundness.ZeroInformation.rectangular_mass line 89

    Source documentation

    outsideWeight may already include the indicator of a fixed observation H=h.

    theorem rectangular_mass {A B : Type} (outside : List A) (inside : List B)
        (outsideWeight : A → Nat) (insideWeight : B → Nat) :
        mass outside (fun a => mass inside (fun b => outsideWeight a * insideWeight b)) =
          mass outside outsideWeight * mass inside insideWeight := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.mass

14. theorem OAI.MaxCutGames.Soundness.ZeroInformation.conditional_inside_identity line 103

    Source documentation

    The division-free conditional-probability identity. If the observation has positive mass, division by that mass gives the unchanged inside law.

    theorem conditional_inside_identity {A B : Type} (outside : List A) (inside : List B)
        (outsideWeight : A → Nat) (insideWeight : B → Nat) (event : B → Bool) :
        mass outside (fun a => mass inside (fun b =>
            outsideWeight a * (if event b then insideWeight b else 0))) *
          mass inside insideWeight =
        mass outside (fun a => mass inside (fun b => outsideWeight a * insideWeight b)) *
          mass inside (fun b => if event b then insideWeight b else 0) := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.mass

15. abbrev OAI.MaxCutGames.Soundness.ZeroInformation.Bits line 116
16. def OAI.MaxCutGames.Soundness.ZeroInformation.zero line 118
17. def OAI.MaxCutGames.Soundness.ZeroInformation.add line 120
18. def OAI.MaxCutGames.Soundness.ZeroInformation.scale line 122
19. theorem OAI.MaxCutGames.Soundness.ZeroInformation.scale_zero line 125
20. def OAI.MaxCutGames.Soundness.ZeroInformation.rowSum line 130
21. theorem OAI.MaxCutGames.Soundness.ZeroInformation.rowSum_congr line 133
22. def OAI.MaxCutGames.Soundness.ZeroInformation.pullbackRow line 140

    Source documentation

    Raw row application after pulling back the retained coordinates along π. single records J, and omega is indexed by positions, never by names.

    def pullbackRow {P R : Type} (positions : List P) (single : P → Bool)
        (zeta0 : Bits R) (zeta1 zeta2 omega : P → Bits R)
        (indices : P → Fin 3) (homogeneous : Bool) (x : P → Fin 3 → Bool) : Bits R :=
    …

    Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.Bits

23. theorem OAI.MaxCutGames.Soundness.ZeroInformation.pullbackRow_index_independent line 149

    Source documentation

    Changing an index where its position coefficient is zero does not change the entire row map. This is an equality for all ambient coordinates, so also on E_U.

    theorem pullbackRow_index_independent {P R : Type} (positions : List P)
        (single : P → Bool) (zeta0 : Bits R) (zeta1 zeta2 omega : P → Bits R)
        (i i' : P → Fin 3)
        (agrees : ∀ j, single j = true → omega j ≠ zero → i j = i' j)
        (homogeneous : Bool) (x : P → Fin 3 → Bool) :
        pullbackRow positions single zeta0 zeta1 zeta2 omega i homogeneous x =
          pullbackRow positions single zeta0 zeta1 zeta2 omega i' homogeneous x := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.Bits, OAI.MaxCutGames.Soundness.ZeroInformation.zero, OAI.MaxCutGames.Soundness.ZeroInformation.pullbackRow

24. theorem OAI.MaxCutGames.Soundness.ZeroInformation.pullbackRow_from_outside_names line 170

    Source documentation

    Distinct occurrence names recover the retained index at all nonzero positions. Consequently revealing outside (occurrence,name) pairs supplies exactly the indices needed by the first player; inside names and indices are unnecessary.

    theorem pullbackRow_from_outside_names {P R O N : Type} (positions : List P)
        (single : P → Bool) (zeta0 : Bits R) (zeta1 zeta2 omega : P → Bits R)
        (occurrences : P → O) (name : O → Fin 3 → N)
        (distinct : ∀ o i i', name o i = name o i' → i = i')
        (i i' : P → Fin 3)
        (sameNames : ∀ j, single j = true → omega j ≠ zero →
          name (occurrences j) (i j) = name (occurrences j) (i' j))
        (homogeneous : Bool) (x : P → Fin 3 → Bool) :
        pullbackRow positions single zeta0 zeta1 zeta2 omega i homogeneous x =
          pullbackRow positions single zeta0 zeta1 zeta2 omega i' homogeneous x := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.Bits, OAI.MaxCutGames.Soundness.ZeroInformation.zero, OAI.MaxCutGames.Soundness.ZeroInformation.pullbackRow

25. theorem OAI.MaxCutGames.Soundness.ZeroInformation.zero_third_bit line 186

    Source documentation

    In particular, substituting the equation for a retained third bit cannot leak the hidden right-hand side through a zero coefficient.

    theorem zero_third_bit {R : Type} (rhs homogeneous x1 x2 : Bool) :
        scale (zero : Bits R) ((rhs && homogeneous) ^^ x1 ^^ x2) = zero := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.scale, OAI.MaxCutGames.Soundness.ZeroInformation.zero, OAI.MaxCutGames.Soundness.ZeroInformation.Bits

26. abbrev OAI.MaxCutGames.Soundness.ZeroInformation.FirstRow line 194

    Source documentation

    A raw row function on ambient first-question coordinates. Restricting it to the equation subspace gives the supplied map Z_B π.

    abbrev FirstRow (P R : Type) := Bool → (P → Fin 3 → Bool) → Bits R

    Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.Bits

27. abbrev OAI.MaxCutGames.Soundness.ZeroInformation.SecondRow line 197

    Source documentation

    A raw row function on ambient partner coordinates.

    abbrev SecondRow (P R : Type) :=
    …

28. structure OAI.MaxCutGames.Soundness.ZeroInformation.FirstInput line 200
29. structure OAI.MaxCutGames.Soundness.ZeroInformation.SecondInput line 206

    Source documentation

    Sum.inl o records a full occurrence and Sum.inr n a single named bit. The summand tag preserves the set J without exposing any retained index.

    structure SecondInput (P R O N : Type) where
    …

30. def OAI.MaxCutGames.Soundness.ZeroInformation.partnerQuestion line 210
31. def OAI.MaxCutGames.Soundness.ZeroInformation.partnerRow line 214
32. theorem OAI.MaxCutGames.Soundness.ZeroInformation.partnerRow_pullback line 221

    Source documentation

    The raw formula really is the pullback under the retained-coordinate projection.

    theorem partnerRow_pullback {P R : Type} (positions : List P) (single : P → Bool)
        (zeta0 : Bits R) (zeta1 zeta2 omega : P → Bits R) (indices : P → Fin 3)
        (homogeneous : Bool) (x : P → Fin 3 → Bool) :
        partnerRow positions single zeta0 zeta1 zeta2 omega homogeneous x
            (fun j => x j (indices j)) =
          pullbackRow positions single zeta0 zeta1 zeta2 omega indices homogeneous x := rfl

    Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.Bits, OAI.MaxCutGames.Soundness.ZeroInformation.partnerRow, OAI.MaxCutGames.Soundness.ZeroInformation.pullbackRow

33. def OAI.MaxCutGames.Soundness.ZeroInformation.firstInput line 228
34. def OAI.MaxCutGames.Soundness.ZeroInformation.secondInput line 233
35. def OAI.MaxCutGames.Soundness.ZeroInformation.decodeIndex line 241

    Source documentation

    A total fixed decoder for a retained index. On supported (o,n) it is uniquely determined by the distinctness of the three names.

    noncomputable def decodeIndex {O N : Type} (name : O → Fin 3 → N)
        (occurrence : O) (n : N) : Fin 3 := by
    …

36. theorem OAI.MaxCutGames.Soundness.ZeroInformation.decodeIndex_name line 246
37. def OAI.MaxCutGames.Soundness.ZeroInformation.reconstructQuestion line 255
38. theorem OAI.MaxCutGames.Soundness.ZeroInformation.reconstructQuestion_actual line 258
39. def OAI.MaxCutGames.Soundness.ZeroInformation.reconstructFirst line 268

    Source documentation

    The first reconstruction receives only fixed outside occurrence/name data, the fixed raw coefficients, and the inside occurrence draw.

    noncomputable def reconstructFirst {P R O N : Type} (positions : List P)
        (single hidden : P → Bool) (zeta0 : Bits R) (zeta1 zeta2 omega : P → Bits R)
        (name : O → Fin 3 → N) (insideOccurrences outsideOccurrences : P → O)
        (outsideNames : P → N) : FirstInput P R O :=
    …

    Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.Bits, OAI.MaxCutGames.Soundness.ZeroInformation.FirstInput

40. theorem OAI.MaxCutGames.Soundness.ZeroInformation.first_input_reconstruction line 276
41. def OAI.MaxCutGames.Soundness.ZeroInformation.reconstructSecond line 302

    Source documentation

    The second reconstruction receives no inside occurrence: only inside names.

    def reconstructSecond {P R O N : Type} (positions : List P)
        (single hidden : P → Bool) (zeta0 : Bits R) (zeta1 zeta2 omega : P → Bits R)
        (outsideOccurrences : P → O) (insideNames outsideNames : P → N) : SecondInput P R O N :=
    …

    Mentions: OAI.MaxCutGames.Soundness.ZeroInformation.Bits, OAI.MaxCutGames.Soundness.ZeroInformation.SecondInput

42. theorem OAI.MaxCutGames.Soundness.ZeroInformation.second_input_reconstruction line 308
43. def OAI.MaxCutGames.Soundness.ZeroInformation.FirstPoint line 333

    Source documentation

    The first equation subspace is determined by its occurrence question alone.

    def FirstPoint {P O : Type} (rhs : O → Bool) (question : P → O) :=
    …

44. def OAI.MaxCutGames.Soundness.ZeroInformation.SecondPoint line 340

    Source documentation

    At single positions the partner space has a free bit and no occurrence or rhs. Unused ambient coordinates are fixed to zero, giving a canonical embedding of the position-dependent coordinate space rather than extra degrees of freedom.

    def SecondPoint {P O N : Type} (rhs : O → Bool) (question : P → Sum O N) :=
    …

45. def OAI.MaxCutGames.Soundness.ZeroInformation.FirstInput.suppliedMap line 348
46. def OAI.MaxCutGames.Soundness.ZeroInformation.SecondInput.suppliedMap line 352
47. def OAI.MaxCutGames.Soundness.ZeroInformation.projectFull line 356
48. def OAI.MaxCutGames.Soundness.ZeroInformation.projectSingles line 360
49. def OAI.MaxCutGames.Soundness.ZeroInformation.partnerProjection line 364
50. theorem OAI.MaxCutGames.Soundness.ZeroInformation.partnerRow_project line 376
51. theorem OAI.MaxCutGames.Soundness.ZeroInformation.supplied_map_pullback line 388
52. abbrev OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionInside line 405
53. abbrev OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionOutside line 406
54. abbrev OAI.MaxCutGames.Soundness.ConditionalIncidences.Draw line 407
55. abbrev OAI.MaxCutGames.Soundness.ConditionalIncidences.InsideDraw line 408
56. def OAI.MaxCutGames.Soundness.ConditionalIncidences.incidence line 410
57. def OAI.MaxCutGames.Soundness.ConditionalIncidences.insideDraw line 413
58. def OAI.MaxCutGames.Soundness.ConditionalIncidences.outsideRecord line 416
59. abbrev OAI.MaxCutGames.Soundness.ConditionalIncidences.ObservationFibre line 420
60. abbrev OAI.MaxCutGames.Soundness.ConditionalIncidences.OutsideFibre line 424
61. instance OAI.MaxCutGames.Soundness.ConditionalIncidences.observationFibreFintype line 429
62. instance OAI.MaxCutGames.Soundness.ConditionalIncidences.outsideFibreFintype line 433
63. def OAI.MaxCutGames.Soundness.ConditionalIncidences.observationFibreEquiv line 438

    Source documentation

    The actual observation fibre, not an assumed rectangular probability law.

    def observationFibreEquiv {P O N : Type} [DecidableEq P]
        (K : Finset P) (name : O → Fin 3 → N)
        (observed : PositionOutside K → O × N) :
        ObservationFibre K name observed ≃ InsideDraw K O × OutsideFibre K name observed where
    …

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionOutside, OAI.MaxCutGames.Soundness.ConditionalIncidences.ObservationFibre, OAI.MaxCutGames.Soundness.ConditionalIncidences.InsideDraw, OAI.MaxCutGames.Soundness.ConditionalIncidences.OutsideFibre

64. def OAI.MaxCutGames.Soundness.ConditionalIncidences.average line 462
65. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.average_equiv line 465
66. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.average_product_left line 471

    Source documentation

    Cancelling the finite nonempty outside fibre gives a normalized equality.

    theorem average_product_left {A B : Type} [Fintype A] [Fintype B]
        (hB : Fintype.card B ≠ 0) (f : A → ℚ) :
        average (fun ab : A × B => f ab.1) = average f := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.average

67. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.average_product_mul line 483

    Source documentation

    Uniform sampling from the actual finite product is independent sampling.

    theorem average_product_mul {A B : Type} [Fintype A] [Fintype B]
        (f : A → ℚ) (g : B → ℚ) :
        average (fun ab : A × B => f ab.1 * g ab.2) = average f * average g := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.average

68. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.average_coordinate_product line 494

    Source documentation

    The uniform function sample is the product of its uniform coordinate laws.

    theorem average_coordinate_product {A X : Type} [Fintype A] [DecidableEq A] [Fintype X]
        (f : A → X → ℚ) :
        average (fun sample : A → X => ∏ a, f a (sample a)) = ∏ a, average (f a) := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.average

69. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.uniform_conditional_ratio line 504

    Source documentation

    This is the usual conditional-expectation ratio in a uniform finite space: the numerator and event probability are both divided by the full sample count.

    theorem uniform_conditional_ratio {A : Type} [Fintype A]
        (p : A → Prop) [Fintype {a // p a}]
        (hpos : 0 < Fintype.card {a // p a}) (f : {a // p a} → ℚ) :
        ((∑ a, f a) / (Fintype.card A : ℚ)) /
            ((Fintype.card {a // p a} : ℚ) / Fintype.card A) = average f := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.average

70. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.conditional_inside_average line 520

    Source documentation

    Exact finite conditional expectation for every function of inside draws. The denominator is the cardinality of the supported observation fibre.

    theorem conditional_inside_average (K : Finset P) (name : O → Fin 3 → N)
        (observed : PositionOutside K → O × N)
        (hpos : 0 < Fintype.card (ObservationFibre K name observed))
        (f : InsideDraw K O → ℚ) :
        average (fun sample : ObservationFibre K name observed => f (insideDraw K sample.val)) =
          average f := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionOutside, OAI.MaxCutGames.Soundness.ConditionalIncidences.ObservationFibre, OAI.MaxCutGames.Soundness.ConditionalIncidences.InsideDraw, OAI.MaxCutGames.Soundness.ConditionalIncidences.average, OAI.MaxCutGames.Soundness.ConditionalIncidences.insideDraw

71. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.conditional_incidence_average line 542

    Source documentation

    Pushing the fresh occurrence/slot draws through (o,i) ↦ (o,vᵢ(o)) gives exactly the repeated incidence law, with no distinct-name assumption needed.

    theorem conditional_incidence_average (K : Finset P) (name : O → Fin 3 → N)
        (observed : PositionOutside K → O × N)
        (hpos : 0 < Fintype.card (ObservationFibre K name observed))
        (f : (PositionInside K → O × N) → ℚ) :
        average (fun sample : ObservationFibre K name observed =>
          f (fun j => incidence name (sample.val j.val))) =
        average (fun fresh : InsideDraw K O => f (fun j => incidence name (fresh j))) := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionOutside, OAI.MaxCutGames.Soundness.ConditionalIncidences.ObservationFibre, OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionInside, OAI.MaxCutGames.Soundness.ConditionalIncidences.average, OAI.MaxCutGames.Soundness.ConditionalIncidences.incidence, OAI.MaxCutGames.Soundness.ConditionalIncidences.InsideDraw

72. abbrev OAI.MaxCutGames.Soundness.ConditionalIncidences.RawSlot line 556

    Source documentation

    None is ζ₀; the left summand gives two coefficients per full position; the right summand gives one coefficient per single position.

    abbrev RawSlot {P : Type} (J : Finset P) :=
    …

73. abbrev OAI.MaxCutGames.Soundness.ConditionalIncidences.RawCoefficients line 559
74. def OAI.MaxCutGames.Soundness.ConditionalIncidences.zeroSet line 561
75. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.mem_zeroSet line 565
76. abbrev OAI.MaxCutGames.Soundness.ConditionalIncidences.RawSample line 570
77. abbrev OAI.MaxCutGames.Soundness.ConditionalIncidences.RawObservationFibre line 575

    Source documentation

    H fixes gamma and the outside incidence pairs. K is a deterministic function of gamma, so including K explicitly in H gives precisely this same event.

    abbrev RawObservationFibre {P D O N : Type} [DecidableEq P] [Zero D] [DecidableEq D]
        (J : Finset P) (name : O → Fin 3 → N) (gamma : RawCoefficients J D)
        (observed : PositionOutside (zeroSet J gamma) → O × N) :=
    …

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.RawCoefficients, OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionOutside, OAI.MaxCutGames.Soundness.ConditionalIncidences.zeroSet

78. instance OAI.MaxCutGames.Soundness.ConditionalIncidences.rawObservationFibreFintype line 581
79. def OAI.MaxCutGames.Soundness.ConditionalIncidences.rawObservationFibreEquiv line 587
80. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.raw_conditional_inside_average line 601

    Source documentation

    Lemma 6.7's conditional product law in the actual independent raw sampling space, with normalized rational expectations. No independence is a hypothesis.

    theorem raw_conditional_inside_average {P D O N : Type} [Fintype P] [DecidableEq P]
        [Fintype D] [Zero D] [DecidableEq D] [Fintype O] [DecidableEq O] [DecidableEq N]
        (J : Finset P) (name : O → Fin 3 → N) (gamma : RawCoefficients J D)
        (observed : PositionOutside (zeroSet J gamma) → O × N)
        (hpos : 0 < Fintype.card (RawObservationFibre J name gamma observed))
        (f : InsideDraw (zeroSet J gamma) O → ℚ) :
        average (fun sample : RawObservationFibre J name gamma observed =>
          f (insideDraw (zeroSet J gamma) sample.val.2)) = average f := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.RawCoefficients, OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionOutside, OAI.MaxCutGames.Soundness.ConditionalIncidences.zeroSet, OAI.MaxCutGames.Soundness.ConditionalIncidences.RawObservationFibre, OAI.MaxCutGames.Soundness.ConditionalIncidences.InsideDraw, OAI.MaxCutGames.Soundness.ConditionalIncidences.average, OAI.MaxCutGames.Soundness.ConditionalIncidences.insideDraw

81. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.raw_conditional_ratio line 623

    Source documentation

    The same exact law expressed as the conditional expectation ratio in the whole raw sample space. Positive probability is represented by a nonempty fibre.

    theorem raw_conditional_ratio {P D O N : Type} [Fintype P] [DecidableEq P]
        [Fintype D] [Zero D] [DecidableEq D] [Fintype O] [DecidableEq O] [DecidableEq N]
        (J : Finset P) (name : O → Fin 3 → N) (gamma : RawCoefficients J D)
        (observed : PositionOutside (zeroSet J gamma) → O × N)
        (hpos : 0 < Fintype.card (RawObservationFibre J name gamma observed))
        (f : InsideDraw (zeroSet J gamma) O → ℚ) :
        ((∑ sample : RawObservationFibre J name gamma observed,
            f (insideDraw (zeroSet J gamma) sample.val.2)) / Fintype.card (RawSample J D O)) /
          ((Fintype.card (RawObservationFibre J name gamma observed) : ℚ) /
            Fintype.card (RawSample J D O)) = average f := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.RawCoefficients, OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionOutside, OAI.MaxCutGames.Soundness.ConditionalIncidences.zeroSet, OAI.MaxCutGames.Soundness.ConditionalIncidences.RawObservationFibre, OAI.MaxCutGames.Soundness.ConditionalIncidences.InsideDraw, OAI.MaxCutGames.Soundness.ConditionalIncidences.insideDraw, OAI.MaxCutGames.Soundness.ConditionalIncidences.RawSample, OAI.MaxCutGames.Soundness.ConditionalIncidences.average

82. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.raw_conditional_incidence_average line 638

    Source documentation

    The pushed-forward product incidence law at K, stated for an arbitrary joint observable, rather than only individual coordinate marginals.

    theorem raw_conditional_incidence_average {P D O N : Type} [Fintype P] [DecidableEq P]
        [Fintype D] [Zero D] [DecidableEq D] [Fintype O] [DecidableEq O] [DecidableEq N]
        (J : Finset P) (name : O → Fin 3 → N) (gamma : RawCoefficients J D)
        (observed : PositionOutside (zeroSet J gamma) → O × N)
        (hpos : 0 < Fintype.card (RawObservationFibre J name gamma observed))
        (f : (PositionInside (zeroSet J gamma) → O × N) → ℚ) :
        average (fun sample : RawObservationFibre J name gamma observed =>
          f (fun j => incidence name (sample.val.2 j.val))) =
        average (fun fresh : InsideDraw (zeroSet J gamma) O => f (fun j => incidence name (fresh j))) := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.RawCoefficients, OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionOutside, OAI.MaxCutGames.Soundness.ConditionalIncidences.zeroSet, OAI.MaxCutGames.Soundness.ConditionalIncidences.RawObservationFibre, OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionInside, OAI.MaxCutGames.Soundness.ConditionalIncidences.average, OAI.MaxCutGames.Soundness.ConditionalIncidences.incidence, OAI.MaxCutGames.Soundness.ConditionalIncidences.InsideDraw

83. theorem OAI.MaxCutGames.Soundness.ConditionalIncidences.raw_conditional_product_incidence line 652

    Source documentation

    Factorization for arbitrary per-position test functions makes the product claim explicit. Repeated names across different positions are fully permitted.

    theorem raw_conditional_product_incidence {P D O N : Type} [Fintype P] [DecidableEq P]
        [Fintype D] [Zero D] [DecidableEq D] [Fintype O] [DecidableEq O] [DecidableEq N]
        (J : Finset P) (name : O → Fin 3 → N) (gamma : RawCoefficients J D)
        (observed : PositionOutside (zeroSet J gamma) → O × N)
        (hpos : 0 < Fintype.card (RawObservationFibre J name gamma observed))
        (f : PositionInside (zeroSet J gamma) → O × N → ℚ) :
        average (fun sample : RawObservationFibre J name gamma observed =>
          ∏ j, f j (incidence name (sample.val.2 j.val))) =
        ∏ j, average (fun fresh : O × Fin 3 => f j (incidence name fresh)) := by
    …

    Mentions: OAI.MaxCutGames.Soundness.ConditionalIncidences.RawCoefficients, OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionOutside, OAI.MaxCutGames.Soundness.ConditionalIncidences.zeroSet, OAI.MaxCutGames.Soundness.ConditionalIncidences.RawObservationFibre, OAI.MaxCutGames.Soundness.ConditionalIncidences.PositionInside, OAI.MaxCutGames.Soundness.ConditionalIncidences.average, OAI.MaxCutGames.Soundness.ConditionalIncidences.incidence

84. def OAI.MaxCutGames.Soundness.PartnerMapCoordinates.activeOf line 690
85. def OAI.MaxCutGames.Soundness.PartnerMapCoordinates.inactiveOfOutside line 692
86. def OAI.MaxCutGames.Soundness.PartnerMapCoordinates.activeOfInside line 695
87. def OAI.MaxCutGames.Soundness.PartnerMapCoordinates.outsideOfInactive line 698
88. def OAI.MaxCutGames.Soundness.PartnerMapCoordinates.insideOfActive line 701
89. def OAI.MaxCutGames.Soundness.PartnerMapCoordinates.tupleToRaw line 704
90. def OAI.MaxCutGames.Soundness.PartnerMapCoordinates.tupleFromRaw line 711
91. def OAI.MaxCutGames.Soundness.PartnerMapCoordinates.tupleRawEquiv line 717
92. def OAI.MaxCutGames.Soundness.PartnerMapCoordinates.pointEquiv line 748

    Source documentation

    Free coordinates of the actual partner, indexed by the exact raw coefficient slots.

    def pointEquiv : PartnerPoint rhs (activeOf J) ≃ₗ[F2] (RawSlot J → F2) :=
    …

    Mentions: OAI.MaxCutGames.Soundness.PartnerMapCoordinates.activeOf

93. theorem OAI.MaxCutGames.Soundness.PartnerMapCoordinates.pointEquiv_none line 751
94. theorem OAI.MaxCutGames.Soundness.PartnerMapCoordinates.pointEquiv_full_first line 754
95. theorem OAI.MaxCutGames.Soundness.PartnerMapCoordinates.pointEquiv_full_second line 758
96. theorem OAI.MaxCutGames.Soundness.PartnerMapCoordinates.pointEquiv_single line 762
97. def OAI.MaxCutGames.Soundness.PartnerMapCoordinates.partnerBasis line 768
98. def OAI.MaxCutGames.Soundness.PartnerMapCoordinates.mapEquiv line 774

    Source documentation

    Arbitrary independent raw coefficients bijectively specify an actual linear map.

    def mapEquiv : RawCoefficients J R ≃ₗ[F2] (PartnerPoint rhs (activeOf J) →ₗ[F2] R) :=
    …

    Mentions: OAI.MaxCutGames.Soundness.PartnerMapCoordinates.activeOf

99. def OAI.MaxCutGames.Soundness.PartnerMapCoordinates.coefficients line 777
100. theorem OAI.MaxCutGames.Soundness.PartnerMapCoordinates.map_coefficients line 780
101. theorem OAI.MaxCutGames.Soundness.PartnerMapCoordinates.coefficients_map line 784
102. theorem OAI.MaxCutGames.Soundness.PartnerMapCoordinates.mapEquiv_apply line 788
103. theorem OAI.MaxCutGames.Soundness.PartnerMapCoordinates.mapEquiv_expansion line 794

     Source documentation

     The raw-coefficient formula for every partner point.

     theorem mapEquiv_expansion (gamma : RawCoefficients J R) (y : PartnerPoint rhs (activeOf J)) :
         mapEquiv rhs J R gamma y =
           ofBit y.homogeneous • gamma none +
             (∑ j : PositionOutside J,
               (ofBit (y.full j.val).first • gamma (some (.inl (j, 0))) +
                 ofBit (y.full j.val).second • gamma (some (.inl (j, 1))))) +
             ∑ j : PositionInside J, ofBit (y.single j.val) • gamma (some (.inr j)) := by
     …

     Mentions: OAI.MaxCutGames.Soundness.PartnerMapCoordinates.activeOf, OAI.MaxCutGames.Soundness.PartnerMapCoordinates.mapEquiv

104. theorem OAI.MaxCutGames.Soundness.PartnerMapCoordinates.every_map_expansion line 806
105. theorem OAI.MaxCutGames.Soundness.PartnerMapCoordinates.pullback_expansion line 811
106. instance OAI.MaxCutGames.Soundness.PartnerMapCoordinates.partnerMapsFintype line 830
107. theorem OAI.MaxCutGames.Soundness.PartnerMapCoordinates.uniform_coefficients_maps line 836

     Source documentation

     Uniform independent coefficient tuples give exactly the uniform law on all maps.

     theorem uniform_coefficients_maps [Fintype R]
         (H : (PartnerPoint rhs (activeOf J) →ₗ[F2] R) → ℚ) :
         average (fun gamma : RawCoefficients J R => H (mapEquiv rhs J R gamma)) = average H :=
     …

     Mentions: OAI.MaxCutGames.Soundness.PartnerMapCoordinates.activeOf, OAI.MaxCutGames.Soundness.PartnerMapCoordinates.mapEquiv

108. theorem OAI.MaxCutGames.Soundness.PartnerMapCoordinates.uniform_map_coefficients_product line 842

     Source documentation

     For a uniformly sampled actual map, all raw coefficients have the product uniform law.

     theorem uniform_map_coefficients_product [Fintype R]
         (H : RawSlot J → R → ℚ) :
         average (fun Y : PartnerPoint rhs (activeOf J) →ₗ[F2] R =>
           ∏ s, H s (coefficients rhs J R Y s)) = ∏ s, average (H s) := by
     …

     Mentions: OAI.MaxCutGames.Soundness.PartnerMapCoordinates.activeOf, OAI.MaxCutGames.Soundness.PartnerMapCoordinates.coefficients