Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionForB

LeanPool.TwoColoringOneRound.LowerBound.N1000000BCompressionForB #

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

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

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

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

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

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

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

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

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

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

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

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

            Equations
            Instances For
              source
              @[implicit_reducible]
              noncomputable instance Distributed2Coloring.LowerBound.N1000000BCompressionForB.instFintypeGN :
              Fintype (Correlation.G n)
              Equations
              source
              noncomputable def Distributed2Coloring.LowerBound.N1000000BCompressionForB.B (r : Block) :
              Matrix V (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
                noncomputable def Distributed2Coloring.LowerBound.N1000000BCompressionForB.vertexSigmaEquiv :
                V ≃ (k : DirIdx) × N1000000OrbitCounting.BaseOrbit k

                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.N1000000BCompressionForB.congr_A_eq_compBasis (r : Block) (d : DirIdx) :
                  (B r).conjTranspose * N1000000OrbitalBasis.A d * B r = N1000000BCompressionCompute.compBasis r d
                  source
                  theorem Distributed2Coloring.LowerBound.N1000000BCompressionForB.congr_ASymm_eq_compBasisSymm (r : Block) (d : DirIdx) :
                  (B r).conjTranspose * N1000000OrbitalBasis.ASymm d * B r = N1000000BCompressionCompute.compBasisSymm r d
                  source
                  theorem Distributed2Coloring.LowerBound.N1000000BCompressionForB.compressionHypScaledForB (f : Coloring n) (r : Block) :
                  N1000000WedderburnData.blockScales[↑r]! • N1000000WeakDuality.S (N1000000Relaxation.xFromColoring f) r = (B r).conjTranspose * Correlation.corrAvgMatrix f * B r
                  source
                  theorem Distributed2Coloring.LowerBound.N1000000BCompressionForB.compressionHypScaled :
                  N1000000RelaxationPsdSoundness.CompressionHypScaled