Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000RelaxationPsdSoundness

LeanPool.TwoColoringOneRound.LowerBound.N1000000RelaxationPsdSoundness #

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

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

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

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

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

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

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

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

        Equations
        Instances For
          source
          def Distributed2Coloring.LowerBound.N1000000RelaxationPsdSoundness.CompressionHypScaled :
          Prop

          Scaled compression hypothesis: each reduced PSD block, after multiplying by its positive scale factor, is a congruence transform of corrAvgMatrix f.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Distributed2Coloring.LowerBound.N1000000RelaxationPsdSoundness.psd_of_compressionHypScaled (h : CompressionHypScaled) (f : Coloring n) (r : Block) :
            (N1000000WeakDuality.S (N1000000Relaxation.xFromColoring f) r).PosSemidef