LeanPool.TwoColoringOneRound.LowerBound.N1000000Z #

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Z.Q :

Type

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

Equations

Distributed2Coloring.LowerBound.N1000000Z.Q = ℚ

Instances For

source

@[reducible, inline]

abbrev Distributed2Coloring.LowerBound.N1000000Z.Block :

Type

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

Equations

Distributed2Coloring.LowerBound.N1000000Z.Block = Fin 7

Instances For

source

def Distributed2Coloring.LowerBound.N1000000Z.matGet (M : Array (Array ℤ)) (i j : ℕ) :

ℤ

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

Equations

Distributed2Coloring.LowerBound.N1000000Z.matGet M i j = (M.getD i #[]).getD j 0

Instances For

source

def Distributed2Coloring.LowerBound.N1000000Z.toMat3Scaled (den : ℕ) (M : Array (Array ℤ)) :

Matrix (Fin 3) (Fin 3) Q

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

Equations

Distributed2Coloring.LowerBound.N1000000Z.toMat3Scaled den M i j = ↑(Distributed2Coloring.LowerBound.N1000000Z.matGet M ↑i ↑j) / ↑den

Instances For

source

def Distributed2Coloring.LowerBound.N1000000Z.toVec3Scaled (den : ℕ) (v : Array ℤ) :

Fin 3 → Q

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

Equations

Distributed2Coloring.LowerBound.N1000000Z.toVec3Scaled den v i = ↑(v.getD (↑i) 0) / ↑den

Instances For

source

def Distributed2Coloring.LowerBound.N1000000Z.Z (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.N1000000Z.den (r : Block) :

ℕ

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

Equations

Distributed2Coloring.LowerBound.N1000000Z.den r = Distributed2Coloring.LowerBound.N1000000ZData.ZldlDen.getD (↑r) 1

Instances For

source

def Distributed2Coloring.LowerBound.N1000000Z.LNum (r : Block) :

Array (Array ℤ)

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

Equations

Distributed2Coloring.LowerBound.N1000000Z.LNum r = Distributed2Coloring.LowerBound.N1000000ZData.ZldlLNum.getD ↑r #[#[], #[], #[]]

Instances For

source

def Distributed2Coloring.LowerBound.N1000000Z.DNum (r : Block) :

Array ℤ

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

Equations

Distributed2Coloring.LowerBound.N1000000Z.DNum r = Distributed2Coloring.LowerBound.N1000000ZData.ZldlDNum.getD ↑r #[]

Instances For

source

def Distributed2Coloring.LowerBound.N1000000Z.L (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.N1000000Z.Dvec (r : Block) :

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

theorem Distributed2Coloring.LowerBound.N1000000Z.Z_eq_LDL (r : Block) :

Z r = L r * Matrix.diagonal (Dvec r) * (L r).transpose

source

theorem Distributed2Coloring.LowerBound.N1000000Z.Dvec_nonneg (r : Block) (i : Fin 3) :

0 ≤ Dvec r i

source

theorem Distributed2Coloring.LowerBound.N1000000Z.Z_posSemidef (r : Block) :

(Z r).PosSemidef

source

theorem Distributed2Coloring.LowerBound.N1000000Z.trace_mul_nonneg_of_Z_posSemidef {r : Block} {S : Matrix (Fin 3) (Fin 3) Q} (hS : S.PosSemidef) :

0 ≤ (Z r * S).trace