Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000CorrAvgMatrixSymmDecompose

This file rewrites corrAvgMatrix into the symmetric orbital basis:

corrAvgMatrix = A id + ∑ i, xFromColoring i • ASymm (varOrbit i).

The key bookkeeping is a tiny (34-element) map from directed indices to the unique variable whose transpose-orbit contains it (with idDirIdx handled separately).

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

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

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

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

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

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

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

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

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

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

          Equations
          Instances For
            source
            theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixSymmDecompose.dirMask_swap_eq_maskAt_invDir {u v : V} (d : DirIdx) (h : N1000000PairTransitivity.dirMask u v = N1000000StructureConstants.maskAt d) :
            N1000000PairTransitivity.dirMask v u = N1000000StructureConstants.maskAt (N1000000BCompressionCompute.invDir d)
            source
            theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixSymmDecompose.coeff_invDir (f : Coloring n) (d : DirIdx) :
            N1000000CorrAvgMatrixDecompose.coeff f d = N1000000CorrAvgMatrixDecompose.coeff f (N1000000BCompressionCompute.invDir d)
            source
            theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixSymmDecompose.dirMask_baseVertex_baseVertex_eq_maskAt_idDirIdx :
            N1000000PairTransitivity.dirMask N1000000OrbitalBasis.baseVertex N1000000OrbitalBasis.baseVertex = N1000000StructureConstants.maskAt N1000000BCompressionCompute.idDirIdx
            source
            theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixSymmDecompose.coeff_idDirIdx_eq_one (f : Coloring n) :
            N1000000CorrAvgMatrixDecompose.coeff f N1000000BCompressionCompute.idDirIdx = 1
            source
            theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixSymmDecompose.varRepVertexU_eq_baseVertex (i : Var) :
            N1000000Relaxation.varRepVertexU i = N1000000OrbitalBasis.baseVertex
            source
            theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixSymmDecompose.dirMask_base_varRepVertexV_eq_varOrbit (i : Var) :
            N1000000PairTransitivity.dirMask N1000000OrbitalBasis.baseVertex (N1000000Relaxation.varRepVertexV i) = N1000000StructureConstants.maskAt (N1000000BCompressionCompute.varOrbit i)
            source
            theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixSymmDecompose.coeff_varOrbit_eq_xFromColoring (f : Coloring n) (i : Var) :
            N1000000CorrAvgMatrixDecompose.coeff f (N1000000BCompressionCompute.varOrbit i) = N1000000Relaxation.xFromColoring f i
            source
            def Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixSymmDecompose.dirToVar :
            Array (Option Var)

            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.N1000000CorrAvgMatrixSymmDecompose.varOfDirIdx (d : DirIdx) :
              Option Var

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

              Equations
              Instances For
                source
                theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixSymmDecompose.varOfDirIdx_eq_none_iff (d : DirIdx) :
                varOfDirIdx d = none ↔ d = N1000000BCompressionCompute.idDirIdx
                source
                theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixSymmDecompose.varOfDirIdx_eq_some_iff (d : DirIdx) (i : Var) :
                varOfDirIdx d = some i ↔ d = N1000000BCompressionCompute.varOrbit i ∨ d = N1000000BCompressionCompute.invDir (N1000000BCompressionCompute.varOrbit i)
                source
                theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixSymmDecompose.varOfDirIdx_spec (d : DirIdx) (hd : d ≠ N1000000BCompressionCompute.idDirIdx) :
                ∃ (i : Var), varOfDirIdx d = some i ∧ (d = N1000000BCompressionCompute.varOrbit i ∨ d = N1000000BCompressionCompute.invDir (N1000000BCompressionCompute.varOrbit i))
                source
                theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixSymmDecompose.corrAvgMatrix_eq_A_id_add_sum_var (f : Coloring n) :
                Correlation.corrAvgMatrix f = N1000000OrbitalBasis.A N1000000BCompressionCompute.idDirIdx + ∑ i : Var, N1000000Relaxation.xFromColoring f i • N1000000OrbitalBasis.ASymm (N1000000BCompressionCompute.varOrbit i)