PartnerMapCoordinates.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

Every partner linear map has independent raw coefficient coordinates

The coefficient index is exactly ConditionalIncidences.RawSlot: one global coefficient, two coefficients at every full position, and one at every single position. The coordinate bijection below is for every actual partner linear map, and its finite-uniform-law theorem has no distributional hypothesis.

def OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.activeOf line 31
def OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.inactiveOfOutside line 33
def OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.activeOfInside line 36
def OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.outsideOfInactive line 39
def OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.insideOfActive line 42
def OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.tupleToRaw line 45
def OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.tupleFromRaw line 52
def OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.tupleRawEquiv line 58
def OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.pointEquiv line 89
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.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.activeOf
theorem OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.pointEquiv_none line 92
theorem OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.pointEquiv_full_first line 95
theorem OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.pointEquiv_full_second line 99
theorem OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.pointEquiv_single line 103
def OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.partnerBasis line 109
def OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.mapEquiv line 115
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.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.activeOf
def OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.coefficients line 118
theorem OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.map_coefficients line 121
theorem OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.coefficients_map line 125
theorem OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.mapEquiv_apply line 129

theorem OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.mapEquiv_expansion line 135

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.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.activeOf, OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.mapEquiv

theorem OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.every_map_expansion line 147
theorem OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.pullback_expansion line 152
instance OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.partnerMapsFintype line 171
theorem OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.uniform_coefficients_maps line 177
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.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.activeOf, OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.mapEquiv
theorem OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.uniform_map_coefficients_product line 183
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.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.activeOf, OAI.UniqueGamesTheorem.Soundness.PartnerMapCoordinates.coefficients