LeanPool.TwoColoringOneRound.LowerBound.Defs

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.Sym (n : ℕ) : Type

Symbols.

Equations

• Distributed2Coloring.LowerBound.Sym n = Fin n

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.Tuple (k n : ℕ) : Type

Ordered k-tuples of symbols.

Equations

• Distributed2Coloring.LowerBound.Tuple k n = (Fin k → Distributed2Coloring.LowerBound.Sym n)

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.Vertex (n : ℕ) : Type

Vertices are injective triples of symbols.

Equations

• Distributed2Coloring.LowerBound.Vertex n = { v : Distributed2Coloring.LowerBound.Tuple 3 n // Function.Injective v }

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.Edge (n : ℕ) : Type

Edges are injective quadruples of symbols, encoding (a,b,c) → (b,c,d).

Equations

• Distributed2Coloring.LowerBound.Edge n = { e : Distributed2Coloring.LowerBound.Tuple 4 n // Function.Injective e }

def Distributed2Coloring.LowerBound.Vertex.a {n : ℕ} (v : Vertex n) : Sym n

First coordinate a of a vertex (a,b,c).

Equations

• v.a = ↑v ⟨0, Distributed2Coloring.LowerBound.Vertex.a._proof_1⟩

def Distributed2Coloring.LowerBound.Vertex.b {n : ℕ} (v : Vertex n) : Sym n

Second coordinate b of a vertex (a,b,c).

Equations

• v.b = ↑v ⟨1, Distributed2Coloring.LowerBound.Vertex.b._proof_1⟩

def Distributed2Coloring.LowerBound.Vertex.c {n : ℕ} (v : Vertex n) : Sym n

Third coordinate c of a vertex (a,b,c).

Equations

• v.c = ↑v ⟨2, Distributed2Coloring.LowerBound.Vertex.c._proof_1⟩

def Distributed2Coloring.LowerBound.Edge.srcIndex (i : Fin 3) : Fin 4

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

Equations

• Distributed2Coloring.LowerBound.Edge.srcIndex i = ⟨↑i, ⋯⟩

def Distributed2Coloring.LowerBound.Edge.dstIndex (i : Fin 3) : Fin 4

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

Equations

• Distributed2Coloring.LowerBound.Edge.dstIndex i = ⟨↑i + 1, ⋯⟩

@[simp]

theorem Distributed2Coloring.LowerBound.Edge.srcIndex_zero : srcIndex 0 = 0

@[simp]

theorem Distributed2Coloring.LowerBound.Edge.srcIndex_one : srcIndex 1 = 1

@[simp]

theorem Distributed2Coloring.LowerBound.Edge.srcIndex_two : srcIndex 2 = 2

@[simp]

theorem Distributed2Coloring.LowerBound.Edge.dstIndex_zero : dstIndex 0 = 1

@[simp]

theorem Distributed2Coloring.LowerBound.Edge.dstIndex_one : dstIndex 1 = 2

@[simp]

theorem Distributed2Coloring.LowerBound.Edge.dstIndex_two : dstIndex 2 = 3

def Distributed2Coloring.LowerBound.Edge.src {n : ℕ} (e : Edge n) : Vertex n

Source vertex of an edge (a,b,c,d), i.e. (a,b,c).

Equations

• e.src = ⟨fun (i : Fin 3) => ↑e (Distributed2Coloring.LowerBound.Edge.srcIndex i), ⋯⟩

def Distributed2Coloring.LowerBound.Edge.dst {n : ℕ} (e : Edge n) : Vertex n

Target vertex of an edge (a,b,c,d), i.e. (b,c,d).

Equations

• e.dst = ⟨fun (i : Fin 3) => ↑e (Distributed2Coloring.LowerBound.Edge.dstIndex i), ⋯⟩

def Distributed2Coloring.LowerBound.Edge.monochromatic {n : ℕ} (f : Vertex n → Bool) (e : Edge n) : Prop

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

Equations

• Distributed2Coloring.LowerBound.Edge.monochromatic f e = (f e.src = f e.dst)

@[implicit_reducible]

instance Distributed2Coloring.LowerBound.Edge.instDecidableMonochromatic {n : ℕ} (f : Vertex n → Bool) (e : Edge n) : Decidable (monochromatic f e)

Equations

• Distributed2Coloring.LowerBound.Edge.instDecidableMonochromatic f e = id inferInstance

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.Coloring (n : ℕ) : Type

A 2-coloring of the vertices.

Equations

• Distributed2Coloring.LowerBound.Coloring n = (Distributed2Coloring.LowerBound.Vertex n → Bool)

def Distributed2Coloring.LowerBound.edgeCount (n : ℕ) : ℕ

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

Equations

• Distributed2Coloring.LowerBound.edgeCount n = Fintype.card (Distributed2Coloring.LowerBound.Edge n)

def Distributed2Coloring.LowerBound.monoEdges {n : ℕ} (f : Coloring n) : Finset (Edge n)

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

Equations

• Distributed2Coloring.LowerBound.monoEdges f = Finset.filter (Distributed2Coloring.LowerBound.Edge.monochromatic f) Finset.univ

def Distributed2Coloring.LowerBound.monoCount {n : ℕ} (f : Coloring n) : ℕ

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

Equations

• Distributed2Coloring.LowerBound.monoCount f = (Distributed2Coloring.LowerBound.monoEdges f).card

def Distributed2Coloring.LowerBound.monoFraction {n : ℕ} (f : Coloring n) : ℚ

Fraction of monochromatic directed edges under f.

Equations

• Distributed2Coloring.LowerBound.monoFraction f = ↑(Distributed2Coloring.LowerBound.monoCount f) / ↑(Distributed2Coloring.LowerBound.edgeCount n)

def Distributed2Coloring.LowerBound.signOfColoring {n : ℕ} (f : Coloring n) : Vertex n → ℤ

Convert a coloring to a sign labeling ±1.

Equations

• Distributed2Coloring.LowerBound.signOfColoring f v = if f v = true then -1 else 1

def Distributed2Coloring.LowerBound.edgeCorrSum {n : ℕ} (f : Coloring n) : ℤ

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

Equations

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

def Distributed2Coloring.LowerBound.edgeCorrelation {n : ℕ} (f : Coloring n) : ℚ

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

Equations

• Distributed2Coloring.LowerBound.edgeCorrelation f = ↑(Distributed2Coloring.LowerBound.edgeCorrSum f) / ↑(Distributed2Coloring.LowerBound.edgeCount n)

theorem Distributed2Coloring.LowerBound.signOfColoring_sq {n : ℕ} (f : Coloring n) (v : Vertex n) : signOfColoring f v * signOfColoring f v = 1

theorem Distributed2Coloring.LowerBound.mono_iff_sign_mul_eq_one {n : ℕ} (f : Coloring n) (e : Edge n) : Edge.monochromatic f e ↔ signOfColoring f e.src * signOfColoring f e.dst = 1

On an edge, being monochromatic is equivalent to having product +1 in ±1.

theorem Distributed2Coloring.LowerBound.monoIndicator_eq_one_add_sign_mul_div_two {n : ℕ} (f : Coloring n) (e : Edge n) : (if Edge.monochromatic f e then 1 else 0) = (1 + ↑(signOfColoring f e.src * signOfColoring f e.dst)) / 2

theorem Distributed2Coloring.LowerBound.monoFraction_eq_one_add_edgeCorrelation_div_two {n : ℕ} (f : Coloring n) (hE : edgeCount n ≠ 0) : monoFraction f = (1 + edgeCorrelation f) / 2