CayleySampling.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.FalseFiber line 19
Source documentation
The common fiber left after separating a Boolean character's sign.
```
abbrev FalseFiber (χ : V → Bool) := {x : V // χ x = false}
```
def OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.falseRepresentative line 21
def OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.booleanSplitEquiv line 26
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.booleanSplitEquiv_fst line 42
def OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.sampleSplitEquiv line 46
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.sampleSplitEquiv_fst line 52
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.card_boolean_split line 56
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.expect_boolean_samples line 61
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.exists_true_of_ne_zero line 83
theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.expect_parity_samples line 94
Source documentation
Actual parity words from independently indexed uniform cube vectors have exactly the uniform Boolean-word distribution.
```
theorem expect_parity_samples (s : Cube I) (hs : s ≠ fun _ => false)
    (F : (D → Bool) → ℝ) :
    (𝔼 g : D → Cube I, F (fun d => AssignmentTester.parity s (g d))) =
      𝔼 b : D → Bool, F b := by
…
```
Mentions: OAI.UniqueGamesTheorem.Foundations.PCP.AssignmentTester.parity

theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.expect_walsh_samples line 104

Source documentation

The same joint law expressed with the actual real Walsh character values.

theorem expect_walsh_samples (s : Cube I) (hs : s ≠ fun _ => false)
    (F : (D → ℝ) → ℝ) :
    (𝔼 g : D → Cube I, F (fun d => walsh s (g d))) =
      𝔼 b : D → Bool, F (fun d => bitSign (b d)) := by
…

theorem OAI.UniqueGamesTheorem.Foundations.PCP.CayleySampling.expect_walsh_mean line 113
Source documentation
In particular, any test of the empirical Walsh bias has the corresponding uniform Boolean-word average. This is the eigenvalue sampling law.
```
theorem expect_walsh_mean (s : Cube I) (hs : s ≠ fun _ => false) (F : ℝ → ℝ) :
    (𝔼 g : D → Cube I, F (𝔼 d, walsh s (g d))) =
      𝔼 b : D → Bool, F (𝔼 d, bitSign (b d)) :=
…
```