LeanPool.TwoColoringOneRound.LowerBound.N1000000Objective

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Objective.n : ℕ

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

Equations

• Distributed2Coloring.LowerBound.N1000000Objective.n = Distributed2Coloring.LowerBound.N1000000Data.n

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Objective.Q : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000Objective.Q = ℚ

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Objective.G : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000Objective.G = Distributed2Coloring.LowerBound.Correlation.G Distributed2Coloring.LowerBound.N1000000Objective.n

@[implicit_reducible]

noncomputable instance Distributed2Coloring.LowerBound.N1000000Objective.instFintypeG : Fintype G

Equations

• Distributed2Coloring.LowerBound.N1000000Objective.instFintypeG = inferInstance

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Objective.Emb4 : Type

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

Equations

• Distributed2Coloring.LowerBound.N1000000Objective.Emb4 = (Fin 4 ↪ Distributed2Coloring.LowerBound.Sym Distributed2Coloring.LowerBound.N1000000Objective.n)

@[implicit_reducible]

noncomputable instance Distributed2Coloring.LowerBound.N1000000Objective.instFintypeEmb4 : Fintype Emb4

Equations

• Distributed2Coloring.LowerBound.N1000000Objective.instFintypeEmb4 = inferInstance

noncomputable def Distributed2Coloring.LowerBound.N1000000Objective.edgeOfEmb (x : Emb4) : Edge n

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

Equations

• Distributed2Coloring.LowerBound.N1000000Objective.edgeOfEmb x = ⟨⇑x, ⋯⟩

noncomputable def Distributed2Coloring.LowerBound.N1000000Objective.embOfEdge (e : Edge n) : Emb4

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

Equations

• Distributed2Coloring.LowerBound.N1000000Objective.embOfEdge e = { toFun := ↑e, inj' := ⋯ }

noncomputable def Distributed2Coloring.LowerBound.N1000000Objective.edgeEquivEmb : Edge n ≃ Emb4

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

Equations

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

noncomputable def Distributed2Coloring.LowerBound.N1000000Objective.corrEdge (f : Coloring n) (e : Edge n) : Q

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

Equations

• Distributed2Coloring.LowerBound.N1000000Objective.corrEdge f e = Distributed2Coloring.LowerBound.Correlation.corr f e.src e.dst

noncomputable def Distributed2Coloring.LowerBound.N1000000Objective.corrEmb (f : Coloring n) (x : Emb4) : Q

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

Equations

• Distributed2Coloring.LowerBound.N1000000Objective.corrEmb f x = Distributed2Coloring.LowerBound.N1000000Objective.corrEdge f (Distributed2Coloring.LowerBound.N1000000Objective.edgeOfEmb x)

theorem Distributed2Coloring.LowerBound.N1000000Objective.xEdge_xFromColoring_eq_edgeCorrelation (f : Coloring n) : N1000000WeakDuality.xEdge (N1000000Relaxation.xFromColoring f) = edgeCorrelation f