LeanPool.TwoColoringOneRound.LowerBound.N1000000WeakDuality #

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000WeakDuality.Q :

Type

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

Equations

Distributed2Coloring.LowerBound.N1000000WeakDuality.Q = ℚ

Instances For

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000WeakDuality.Var :

Type

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

Equations

Distributed2Coloring.LowerBound.N1000000WeakDuality.Var = Fin Distributed2Coloring.LowerBound.N1000000Data.numVars

Instances For

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000WeakDuality.Block :

Type

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

Equations

Distributed2Coloring.LowerBound.N1000000WeakDuality.Block = Fin 7

Instances For

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000WeakDuality.Mu :

Type

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

Equations

Distributed2Coloring.LowerBound.N1000000WeakDuality.Mu = Fin Distributed2Coloring.LowerBound.N1000000Data.muSupport.size

Instances For

source

def Distributed2Coloring.LowerBound.N1000000WeakDuality.xEdge (x : Var → Q) :

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

Equations

Distributed2Coloring.LowerBound.N1000000WeakDuality.xEdge x = x ⟨Distributed2Coloring.LowerBound.N1000000Data.edgeVar, Distributed2Coloring.LowerBound.N1000000WeakDuality.xEdge._proof_1 ⟩

Instances For

source

def Distributed2Coloring.LowerBound.N1000000WeakDuality.muNumD (k : Mu) :

ℤ

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

def Distributed2Coloring.LowerBound.N1000000WeakDuality.muVal (k : Mu) :

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

Equations

Distributed2Coloring.LowerBound.N1000000WeakDuality.muVal k = ↑(Distributed2Coloring.LowerBound.N1000000WeakDuality.muNumD k) / ↑Distributed2Coloring.LowerBound.N1000000Data.D

Instances For

source

def Distributed2Coloring.LowerBound.N1000000WeakDuality.aVec (k : Mu) :

Array ℤ

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

def Distributed2Coloring.LowerBound.N1000000WeakDuality.aCoeffInt (k : Mu) (i : Var) :

ℤ

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

Equations

Distributed2Coloring.LowerBound.N1000000WeakDuality.aCoeffInt k i = Distributed2Coloring.LowerBound.N1000000.coeffAt (Distributed2Coloring.LowerBound.N1000000WeakDuality.aVec k) ↑i

Instances For

source

def Distributed2Coloring.LowerBound.N1000000WeakDuality.aCoeff (k : Mu) (i : Var) :

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

Equations

Distributed2Coloring.LowerBound.N1000000WeakDuality.aCoeff k i = ↑(Distributed2Coloring.LowerBound.N1000000WeakDuality.aCoeffInt k i)

Instances For

source

def Distributed2Coloring.LowerBound.N1000000WeakDuality.aDot (k : Mu) (x : Var → Q) :

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

def Distributed2Coloring.LowerBound.N1000000WeakDuality.muSum :

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

Equations

Distributed2Coloring.LowerBound.N1000000WeakDuality.muSum = ∑ k : Distributed2Coloring.LowerBound.N1000000WeakDuality.Mu, Distributed2Coloring.LowerBound.N1000000WeakDuality.muVal k

Instances For

source

def Distributed2Coloring.LowerBound.N1000000WeakDuality.S0Num (r : Block) :

Array (Array ℤ)

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

Equations

Distributed2Coloring.LowerBound.N1000000WeakDuality.S0Num r = Distributed2Coloring.LowerBound.N1000000Data.S0Blocks.getD ↑r #[]

Instances For

source

def Distributed2Coloring.LowerBound.N1000000WeakDuality.SiNum (r : Block) (i : Var) :

Array (Array ℤ)

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

Equations

Distributed2Coloring.LowerBound.N1000000WeakDuality.SiNum r i = (Distributed2Coloring.LowerBound.N1000000Data.SiBlocks.getD ↑r #[]).getD ↑i #[]

Instances For

source

def Distributed2Coloring.LowerBound.N1000000WeakDuality.S0 (r : Block) :

Matrix (Fin 3) (Fin 3) Q

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

def Distributed2Coloring.LowerBound.N1000000WeakDuality.Si (r : Block) (i : Var) :

Matrix (Fin 3) (Fin 3) Q

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

def Distributed2Coloring.LowerBound.N1000000WeakDuality.S (x : Var → Q) (r : Block) :

Matrix (Fin 3) (Fin 3) Q

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

def Distributed2Coloring.LowerBound.N1000000WeakDuality.frobInner (A B : Matrix (Fin 3) (Fin 3) Q) :

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

Equations

Distributed2Coloring.LowerBound.N1000000WeakDuality.frobInner A B = (A * B.transpose).trace

Instances For

source

def Distributed2Coloring.LowerBound.N1000000WeakDuality.zSum0 :

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

def Distributed2Coloring.LowerBound.N1000000WeakDuality.zCoeff (i : Var) :

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

def Distributed2Coloring.LowerBound.N1000000WeakDuality.dualObjective :

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

def Distributed2Coloring.LowerBound.N1000000WeakDuality.PrimalFeasibleForCertificate (x : Var → Q) :

Prop

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.N1000000WeakDuality.muVal_nonneg (k : Mu) :

0 ≤ muVal k

source

theorem Distributed2Coloring.LowerBound.N1000000WeakDuality.weakDuality (x : Var → Q) (hx : PrimalFeasibleForCertificate x) :

dualObjective ≤ xEdge x