Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000CorrAvgMatrixDecompose

LeanPool.TwoColoringOneRound.LowerBound.N1000000CorrAvgMatrixDecompose #

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

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

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

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

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

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

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

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

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

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

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

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

            Equations
            Instances For
              source
              @[implicit_reducible]
              noncomputable instance Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixDecompose.instFintypeGN :
              Fintype (Correlation.G n)
              Equations
              source
              noncomputable def Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixDecompose.repEmb (k : DirIdx) :
              N1000000OrbitCounting.FreeCol k ↪ AvailFrom3

              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.N1000000CorrAvgMatrixDecompose.repVertex (d : DirIdx) :
                V

                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.N1000000CorrAvgMatrixDecompose.dirMask_base_repVertex (d : DirIdx) :
                  N1000000PairTransitivity.dirMask N1000000OrbitalBasis.baseVertex (repVertex d) = N1000000StructureConstants.maskAt d
                  source
                  noncomputable def Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixDecompose.coeff (f : Coloring n) (d : DirIdx) :
                  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
                    theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixDecompose.corrAvg_eq_coeff_of_dirMask_eq (f : Coloring n) {u v : V} (d : DirIdx) (h : N1000000PairTransitivity.dirMask u v = N1000000StructureConstants.maskAt d) :
                    Correlation.corrAvg f u v = coeff f d
                    source
                    theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixDecompose.corrAvg_symmetric (f : Coloring n) (u v : V) :
                    Correlation.corrAvg f u v = Correlation.corrAvg f v u
                    source
                    theorem Distributed2Coloring.LowerBound.N1000000CorrAvgMatrixDecompose.corrAvgMatrix_eq_sum_coeff_A (f : Coloring n) :
                    Correlation.corrAvgMatrix f = ∑ d : DirIdx, coeff f d • N1000000OrbitalBasis.A d