LeanPool.TwoColoringOneRound.LowerBound.Correlation #

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.Correlation.Q :

Type

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

Distributed2Coloring.LowerBound.Correlation.Q = ℚ

Instances For

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.Correlation.G (n : ℕ) :

Type

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

Distributed2Coloring.LowerBound.Correlation.G n = Equiv.Perm (Distributed2Coloring.LowerBound.Sym n)

Instances For

source

@[implicit_reducible]

noncomputable instance Distributed2Coloring.LowerBound.Correlation.instFintypeG (n : ℕ) :

Fintype (G n)

Equations

Distributed2Coloring.LowerBound.Correlation.instFintypeG n = Fintype.ofFinite (Distributed2Coloring.LowerBound.Correlation.G n)

source

@[implicit_reducible]

instance Distributed2Coloring.LowerBound.Correlation.instMulActionGVertex (n : ℕ) :

MulAction (G n) (Vertex n)

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem Distributed2Coloring.LowerBound.Correlation.vertex_smul_apply {n : ℕ} (σ : G n) (v : Vertex n) (i : Fin 3) :

↑(σ • v) i = σ (↑v i)

source

@[implicit_reducible]

instance Distributed2Coloring.LowerBound.Correlation.instMulActionGEdge (n : ℕ) :

MulAction (G n) (Edge n)

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem Distributed2Coloring.LowerBound.Correlation.edge_smul_apply {n : ℕ} (σ : G n) (e : Edge n) (i : Fin 4) :

↑(σ • e) i = σ (↑e i)

source

def Distributed2Coloring.LowerBound.Correlation.spin (b : Bool) :

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

Distributed2Coloring.LowerBound.Correlation.spin b = if b = true then -1 else 1

Instances For

source

theorem Distributed2Coloring.LowerBound.Correlation.spin_mul_self (b : Bool) :

spin b * spin b = 1

source

def Distributed2Coloring.LowerBound.Correlation.corr {n : ℕ} (f : Coloring n) (u v : Vertex n) :

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

Distributed2Coloring.LowerBound.Correlation.corr f u v = Distributed2Coloring.LowerBound.Correlation.spin (f u) * Distributed2Coloring.LowerBound.Correlation.spin (f v)

Instances For

source

noncomputable def Distributed2Coloring.LowerBound.Correlation.corrAvg {n : ℕ} (f : Coloring n) (u v : Vertex n) :

Imported auxiliary declaration for the 2-coloring one-round formalization.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Distributed2Coloring.LowerBound.Correlation.cardG_pos (n : ℕ) :

0 < ↑(Fintype.card (G n))

source

theorem Distributed2Coloring.LowerBound.Correlation.corrAvg_smul {n : ℕ} (f : Coloring n) (τ : G n) (u v : Vertex n) :

corrAvg f (τ • u) (τ • v) = corrAvg f u v

source

theorem Distributed2Coloring.LowerBound.Correlation.corr_le_one (b0 b1 : Bool) :

spin b0 * spin b1 ≤ 1

source

theorem Distributed2Coloring.LowerBound.Correlation.neg_one_le_corr (b0 b1 : Bool) :

-1 ≤ spin b0 * spin b1

source

theorem Distributed2Coloring.LowerBound.Correlation.corrAvg_le_one {n : ℕ} (f : Coloring n) (u v : Vertex n) :

corrAvg f u v ≤ 1

source

theorem Distributed2Coloring.LowerBound.Correlation.neg_one_le_corrAvg {n : ℕ} (f : Coloring n) (u v : Vertex n) :

-1 ≤ corrAvg f u v

source

theorem Distributed2Coloring.LowerBound.Correlation.triangle_inequalities (b0 b1 b2 : Bool) :

-(spin b0 * spin b1 + spin b0 * spin b2 + spin b1 * spin b2) ≤ 1 ∧ spin b0 * spin b1 + spin b0 * spin b2 - spin b1 * spin b2 ≤ 1 ∧ spin b0 * spin b1 - spin b0 * spin b2 + spin b1 * spin b2 ≤ 1 ∧ -spin b0 * spin b1 + spin b0 * spin b2 + spin b1 * spin b2 ≤ 1

source

theorem Distributed2Coloring.LowerBound.Correlation.corrAvg_comm {n : ℕ} (f : Coloring n) (u v : Vertex n) :

corrAvg f u v = corrAvg f v u

source

theorem Distributed2Coloring.LowerBound.Correlation.corrAvg_triangle {n : ℕ} (f : Coloring n) (u v w : Vertex n) :

-(corrAvg f u v + corrAvg f u w + corrAvg f v w) ≤ 1 ∧ corrAvg f u v + corrAvg f u w - corrAvg f v w ≤ 1 ∧ corrAvg f u v - corrAvg f u w + corrAvg f v w ≤ 1 ∧ -corrAvg f u v + corrAvg f u w + corrAvg f v w ≤ 1