FiniteIndependentSamples.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Coordinate independence in finite product samples

Uniformly sampling a finite function is the concrete probability space used for the independent left and right matrix unitaries. One- and two-coordinate expectations reduce to their actual finite averages.

theorem OAI.KadisonKastler.expect_sample_coordinate line 24
Source documentation
One coordinate of a uniformly sampled function has the uniform law.
```
theorem expect_sample_coordinate (i : I) (f : G → X) :
    (𝔼 ω : I → G, f (ω i)) = 𝔼 g : G, f g := by
…
```

theorem OAI.KadisonKastler.expect_sample_two_coordinates line 36

Source documentation

Distinct coordinates in the finite product are independent.

theorem expect_sample_two_coordinates {i j : I} (hij : i ≠ j) (f : G → G → X) :
    (𝔼 ω : I → G, f (ω i) (ω j)) = 𝔼 g : G, 𝔼 h : G, f g h := by
…

theorem OAI.KadisonKastler.expect_sample_pair_sum line 59

Source documentation

Summing the two-coordinate law separates the diagonal samples from the independent off-diagonal samples, with their exact multiplicities.

theorem expect_sample_pair_sum (f : G → G → ℝ) :
    (𝔼 ω : I → G, ∑ i, ∑ j, f (ω i) (ω j)) =
      (Fintype.card I : ℝ) * (𝔼 g : G, f g g) +
        (Fintype.card I : ℝ) * ((Fintype.card I : ℝ) - 1) *
          (𝔼 g : G, 𝔼 h : G, f g h) := by
…