CoefficientSampling.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Uniform raw advice coefficients obtained by discarding unused flat coordinates. The intercept, both full columns at every position, and one singleton column at every position are independent. For a fixed singleton set, selecting the used columns gives exactly the uniform law on the dynamic raw coefficient type. The identity holds for every joint test function, not merely for marginals.

def OAI.UniqueGamesTheorem.Clean.CoefficientSampling.selectCoefficients line 29
def OAI.UniqueGamesTheorem.Clean.CoefficientSampling.coefficientProductEquiv line 37
Source documentation
Splitting a raw coefficient tuple into its actual independent coordinates.
```
def coefficientProductEquiv (J : Finset P) :
    RawCoefficients J C ≃ C × ((PositionOutside J → C × C) × (PositionInside J → C)) where
…
```

theorem OAI.UniqueGamesTheorem.Clean.CoefficientSampling.expect_outside line 59

Source documentation

The complement restriction is also uniform, including an empty complement.

theorem expect_outside (J : Finset P) (f : (PositionOutside J → C) → ℝ) :
    (𝔼 full : P → C, f (fun j => full j.val)) =
      𝔼 outside : PositionOutside J → C, f outside := by
…

theorem OAI.UniqueGamesTheorem.Clean.CoefficientSampling.expect_rawCoefficients line 71
theorem OAI.UniqueGamesTheorem.Clean.CoefficientSampling.expect_selectCoefficients line 88
Source documentation
Sampling all columns and then discarding unused ones has exactly the uniform joint law on the coefficients used by this singleton set.
```
theorem expect_selectCoefficients (J : Finset P) (F : RawCoefficients J C → ℝ) :
    (𝔼 extra : C × (P → C × C), 𝔼 single : P → C,
      F (selectCoefficients J extra single)) =
      𝔼 gamma : RawCoefficients J C, F gamma := by
…
```
Mentions: OAI.UniqueGamesTheorem.Clean.CoefficientSampling.selectCoefficients
theorem OAI.UniqueGamesTheorem.Clean.CoefficientSampling.uniform_expectation_eq_expect line 115
theorem OAI.UniqueGamesTheorem.Clean.CoefficientSampling.uniform_selectCoefficients line 119

theorem OAI.UniqueGamesTheorem.Clean.CoefficientSampling.mask_average_selectCoefficients line 128

Source documentation

The fixed-mask identity may be averaged under any independent mask law.

theorem mask_average_selectCoefficients (maskLaw : FiniteDistribution (Finset P))
    (F : (J : Finset P) → RawCoefficients J C → ℝ) :
    maskLaw.expectation (fun J =>
      (FiniteDistribution.uniform (C × (P → C × C))).expectation (fun extra =>
        (FiniteDistribution.uniform (P → C)).expectation (fun single =>
          F J (selectCoefficients J extra single)))) =
      maskLaw.expectation (fun J =>
        (FiniteDistribution.uniform (RawCoefficients J C)).expectation (F J)) := by
…

Mentions: OAI.UniqueGamesTheorem.Clean.CoefficientSampling.selectCoefficients