Documentation

LeanPool.TwoColoringOneRound.LowerBound.N1000000Transitivity

LeanPool.TwoColoringOneRound.LowerBound.N1000000Transitivity #

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

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

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

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

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

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

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

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

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

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

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

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

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

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

              Equations
              Instances For
                source
                @[implicit_reducible]
                noncomputable instance Distributed2Coloring.LowerBound.N1000000Transitivity.instFintypeG :
                Fintype G
                Equations
                source
                theorem Distributed2Coloring.LowerBound.N1000000Transitivity.dirMask_smul (σ : G) (u v : V) :
                N1000000PairTransitivity.dirMask (σ • u) (σ • v) = N1000000PairTransitivity.dirMask u v
                source
                theorem Distributed2Coloring.LowerBound.N1000000Transitivity.dirMask_isPartialPermMask (u v : V) :
                IsPartialPermMask (N1000000PairTransitivity.dirMask u v)
                source
                theorem Distributed2Coloring.LowerBound.N1000000Transitivity.exists_dirIdx_of_dirMask (u v : V) :
                ∃ (d : DirIdx), N1000000StructureConstants.maskAt d = N1000000PairTransitivity.dirMask u v
                source
                noncomputable def Distributed2Coloring.LowerBound.N1000000Transitivity.dirIdxOfDirMask (u v : V) :
                DirIdx

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

                Equations
                Instances For
                  source
                  theorem Distributed2Coloring.LowerBound.N1000000Transitivity.maskAt_dirIdxOfDirMask (u v : V) :
                  N1000000StructureConstants.maskAt (dirIdxOfDirMask u v) = N1000000PairTransitivity.dirMask u v
                  source
                  noncomputable def Distributed2Coloring.LowerBound.N1000000Transitivity.dirIdxBase (u : V) :
                  DirIdx

                  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.N1000000Transitivity.maskAt_dirIdxBase (u : V) :
                    N1000000StructureConstants.maskAt (dirIdxBase u) = N1000000PairTransitivity.dirMask N1000000OrbitalBasis.baseVertex u
                    source
                    theorem Distributed2Coloring.LowerBound.N1000000Transitivity.exists_perm_send_to_base (u : V) :
                    ∃ (σ : G), σ • u = N1000000OrbitalBasis.baseVertex
                    source
                    theorem Distributed2Coloring.LowerBound.N1000000Transitivity.exists_perm_fixing_base_of_baseOrbit (k : DirIdx) (w w' : N1000000OrbitCounting.BaseOrbit k) :
                    ∃ (τ : G), τ • N1000000OrbitalBasis.baseVertex = N1000000OrbitalBasis.baseVertex ∧ τ • ↑w = ↑w'
                    source
                    theorem Distributed2Coloring.LowerBound.N1000000Transitivity.exists_perm_of_dirMask_eq {u v u' v' : V} (h : N1000000PairTransitivity.dirMask u v = N1000000PairTransitivity.dirMask u' v') :
                    ∃ (σ : G), σ • u = u' ∧ σ • v = v'
                    source
                    theorem Distributed2Coloring.LowerBound.N1000000Transitivity.corrAvg_eq_of_dirMask_eq (f : Coloring n) {u v u' v' : V} (h : N1000000PairTransitivity.dirMask u v = N1000000PairTransitivity.dirMask u' v') :
                    Correlation.corrAvg f u v = Correlation.corrAvg f u' v'