Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000Bound

LeanPool.TwoColoringOneRound.LowerBound.N1000000Bound #

source
@[reducible, inline]
abbrev Distributed2Coloring.LowerBound.N1000000Bound.n :
ℕ

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

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Distributed2Coloring.LowerBound.N1000000Bound.Q :
    Type

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

    Equations
    Instances For
      source
      theorem Distributed2Coloring.LowerBound.N1000000Bound.dualObjective_ge_target :
      -26121 / 50000 ≤ N1000000WeakDuality.dualObjective
      source
      theorem Distributed2Coloring.LowerBound.N1000000Bound.monoFraction_ge_23879_of_psd (f : Coloring n) (hpsd : ∀ (r : N1000000WeakDuality.Block), (N1000000WeakDuality.S (N1000000Relaxation.xFromColoring f) r).PosSemidef) :
      23879 / 100000 ≤ monoFraction f