Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000MuLinear

LeanPool.TwoColoringOneRound.LowerBound.N1000000MuLinear #

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

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

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

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

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

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

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

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

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

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

          Equations
          Instances For
            source
            @[implicit_reducible]
            noncomputable instance Distributed2Coloring.LowerBound.N1000000MuLinear.instFintypeG :
            Fintype G
            Equations
            source
            instance Distributed2Coloring.LowerBound.N1000000MuLinear.instNeZeroNatNumVars :
            NeZero N1000000Data.numVars
            source
            @[implicit_reducible]
            instance Distributed2Coloring.LowerBound.N1000000MuLinear.instInhabitedPairMapData :
            Inhabited N1000000MuWitness.PairMapData
            Equations
            • One or more equations did not get rendered due to their size.
            source
            def Distributed2Coloring.LowerBound.N1000000MuLinear.vertexOfLabels (t : N1000000MuWitness.LabelTriple) :
            Vertex n

            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.N1000000MuLinear.PairMapOk (i : Var) (pm : N1000000MuWitness.PairMapData) :
              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
                @[implicit_reducible]
                instance Distributed2Coloring.LowerBound.N1000000MuLinear.instDecidablePairMapOk (i : Var) (pm : N1000000MuWitness.PairMapData) :
                Decidable (PairMapOk i pm)
                Equations
                source
                theorem Distributed2Coloring.LowerBound.N1000000MuLinear.xFromColoring_muLinear (f : Coloring n) (k : Mu) :
                N1000000WeakDuality.aDot k (N1000000Relaxation.xFromColoring f) ≤ 1