PairAverage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.MUB6.injectiveMoment_empty line 11
theorem OAI.MUB6.averagedRowProducts_eq_pairAverage line 27
Source documentation
A uniform injection of all six row indices is a uniform permutation. This identifies the general partition theorem with the paper's pair average.
```
theorem averagedRowProducts_eq_pairAverage {n : ℕ} (H : CMatrix)
    (A : Matrix Coord (Fin n) ℤ) :
    averagedRowProducts H A =
      pairAverage H (fun K => (∏ j, g K (fun i => A i j)).re) := by
…
```
Mentions: OAI.MUB6.CMatrix, OAI.MUB6.Coord, OAI.MUB6.averagedRowProducts, OAI.MUB6.pairAverage, OAI.MUB6.g
theorem OAI.MUB6.pairAverage_products_partition line 40