OAI/Computability/UniqueGames/Soundness/ZeroInformationLemmas.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Fibre line 20

   Source documentation

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

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

2. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Inside line 24

   Source documentation

   At hidden positions the draw is unconstrained.

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

3. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Outside line 27

   Source documentation

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

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

4. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.fibreInside line 30
5. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.fibreOutside line 33
6. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.assemble line 36
7. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.inside_assemble line 46
8. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.outside_assemble line 52
9. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.assemble_split line 59
10. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.fibre_product line 70

    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.UniqueGamesTheorem.Soundness.ZeroInformation.Fibre, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Inside, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Outside

11. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.mass line 81
12. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.mass_scale line 85
13. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.rectangular_mass line 92

    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.UniqueGamesTheorem.Soundness.ZeroInformation.mass

14. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.conditional_inside_identity line 106

    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.UniqueGamesTheorem.Soundness.ZeroInformation.mass

15. abbrev OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Bits line 119
16. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.zero line 121
17. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.add line 123
18. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.scale line 125
19. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.scale_zero line 128
20. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.rowSum line 133
21. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.rowSum_congr line 136
22. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.pullbackRow line 143

    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.UniqueGamesTheorem.Soundness.ZeroInformation.Bits

23. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.pullbackRow_index_independent line 152

    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.UniqueGamesTheorem.Soundness.ZeroInformation.Bits, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.zero, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.pullbackRow

24. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.pullbackRow_from_outside_names line 173

    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.UniqueGamesTheorem.Soundness.ZeroInformation.Bits, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.zero, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.pullbackRow

25. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.zero_third_bit line 189

    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.UniqueGamesTheorem.Soundness.ZeroInformation.scale, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.zero, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.Bits

26. abbrev OAI.UniqueGamesTheorem.Soundness.ZeroInformation.FirstRow line 197

    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.UniqueGamesTheorem.Soundness.ZeroInformation.Bits

27. abbrev OAI.UniqueGamesTheorem.Soundness.ZeroInformation.SecondRow line 200

    Source documentation

    A raw row function on ambient partner coordinates.

    abbrev SecondRow (P R : Type) :=
    …

28. structure OAI.UniqueGamesTheorem.Soundness.ZeroInformation.FirstInput line 203
29. structure OAI.UniqueGamesTheorem.Soundness.ZeroInformation.SecondInput line 209

    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.UniqueGamesTheorem.Soundness.ZeroInformation.partnerQuestion line 213
31. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.partnerRow line 217
32. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.partnerRow_pullback line 224

    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.UniqueGamesTheorem.Soundness.ZeroInformation.Bits, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.partnerRow, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.pullbackRow

33. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.firstInput line 231
34. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.secondInput line 236
35. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.decodeIndex line 244

    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.UniqueGamesTheorem.Soundness.ZeroInformation.decodeIndex_name line 249
37. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.reconstructQuestion line 258
38. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.reconstructQuestion_actual line 261
39. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.reconstructFirst line 271

    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.UniqueGamesTheorem.Soundness.ZeroInformation.Bits, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.FirstInput

40. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.first_input_reconstruction line 279
41. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.reconstructSecond line 305

    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.UniqueGamesTheorem.Soundness.ZeroInformation.Bits, OAI.UniqueGamesTheorem.Soundness.ZeroInformation.SecondInput

42. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.second_input_reconstruction line 311
43. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.FirstPoint line 336

    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.UniqueGamesTheorem.Soundness.ZeroInformation.SecondPoint line 343

    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.UniqueGamesTheorem.Soundness.ZeroInformation.FirstInput.suppliedMap line 351
46. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.SecondInput.suppliedMap line 355
47. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.projectFull line 359
48. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.projectSingles line 363
49. def OAI.UniqueGamesTheorem.Soundness.ZeroInformation.partnerProjection line 367
50. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.partnerRow_project line 379
51. theorem OAI.UniqueGamesTheorem.Soundness.ZeroInformation.supplied_map_pullback line 391
52. abbrev OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionInside line 408
53. abbrev OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionOutside line 409
54. abbrev OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.Draw line 410
55. abbrev OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.InsideDraw line 411
56. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.incidence line 413
57. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.insideDraw line 416
58. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.outsideRecord line 419
59. abbrev OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.ObservationFibre line 423
60. abbrev OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.OutsideFibre line 427
61. instance OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.observationFibreFintype line 432
62. instance OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.outsideFibreFintype line 436
63. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.observationFibreEquiv line 441

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionOutside, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.ObservationFibre, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.InsideDraw, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.OutsideFibre

64. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.average line 465
65. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.average_equiv line 468
66. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.average_product_left line 474

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.average

67. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.average_product_mul line 486

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.average

68. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.average_coordinate_product line 497

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.average

69. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.uniform_conditional_ratio line 507

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.average

70. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.conditional_inside_average line 523

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionOutside, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.ObservationFibre, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.InsideDraw, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.average, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.insideDraw

71. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.conditional_incidence_average line 545

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionOutside, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.ObservationFibre, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionInside, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.average, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.incidence, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.InsideDraw

72. abbrev OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawSlot line 559

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawCoefficients line 562
74. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.zeroSet line 564
75. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.mem_zeroSet line 568
76. abbrev OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawSample line 573
77. abbrev OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawObservationFibre line 578

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawCoefficients, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionOutside, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.zeroSet

78. instance OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.rawObservationFibreFintype line 584
79. def OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.rawObservationFibreEquiv line 590
80. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.raw_conditional_inside_average line 604

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawCoefficients, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionOutside, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.zeroSet, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawObservationFibre, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.InsideDraw, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.average, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.insideDraw

81. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.raw_conditional_ratio line 626

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawCoefficients, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionOutside, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.zeroSet, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawObservationFibre, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.InsideDraw, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.insideDraw, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawSample, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.average

82. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.raw_conditional_incidence_average line 641

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawCoefficients, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionOutside, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.zeroSet, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawObservationFibre, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionInside, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.average, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.incidence, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.InsideDraw

83. theorem OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.raw_conditional_product_incidence line 655

    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.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawCoefficients, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionOutside, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.zeroSet, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.RawObservationFibre, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.PositionInside, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.average, OAI.UniqueGamesTheorem.Soundness.ConditionalIncidences.incidence