LeanPool.TwoColoringOneRound.LowerBound.CorrAvgMatrix

def Distributed2Coloring.LowerBound.Correlation.corrMatrix {n : ℕ} (f : Coloring n) : Matrix (Vertex n) (Vertex n) Q

The rank-1 correlation kernel as a matrix indexed by vertices.

Equations

• Distributed2Coloring.LowerBound.Correlation.corrMatrix f u v = Distributed2Coloring.LowerBound.Correlation.corr f u v

noncomputable def Distributed2Coloring.LowerBound.Correlation.corrAvgMatrix {n : ℕ} (f : Coloring n) : Matrix (Vertex n) (Vertex n) Q

The orbit-averaged correlation kernel as a matrix indexed by vertices.

Equations

• Distributed2Coloring.LowerBound.Correlation.corrAvgMatrix f u v = Distributed2Coloring.LowerBound.Correlation.corrAvg f u v

theorem Distributed2Coloring.LowerBound.Correlation.corrMatrix_posSemidef {n : ℕ} (f : Coloring n) : (corrMatrix f).PosSemidef

theorem Distributed2Coloring.LowerBound.Correlation.corrAvgMatrix_posSemidef {n : ℕ} (f : Coloring n) : (corrAvgMatrix f).PosSemidef