Documentation

LeanPool.TwoColoringOneRound.Definitions

Distributed2Coloring: Definitions #

This file exposes the key definitions intended for downstream use.

Most internal development lives under Distributed2Coloring.LowerBound and Distributed2Coloring.UpperBound; users should not need to import those files directly unless they want to follow the detailed proofs.

One-round classical algorithms #

Rand is the unit interval [0,1] (as a measurable space). A ClassicalAlgorithm is a measurable local rule f : Rand × Rand × Rand → Fin 2 applied to i.i.d. labels on the directed cycle.

The quantity ClassicalAlgorithm.p alg is the probability that an oriented edge is monochromatic: alg.f agrees on consecutive windows (x₀,x₁,x₂) and (x₁,x₂,x₃) under i.i.d. labels.

source
@[reducible, inline]
abbrev Distributed2Coloring.Rand :
Type

The source of local randomness for one-round algorithms: the unit interval [0,1].

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Distributed2Coloring.Color :
    Type

    The two output colors.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev Distributed2Coloring.Samples (n : ℕ) :
      Type

      A seed assignment of i.i.d. labels to n vertices.

      Equations
      Instances For
        source
        structure Distributed2Coloring.ClassicalAlgorithm :
        Type

        A one-round classical distributed algorithm for 2-coloring the directed cycle.

        It is a measurable local rule f that reads the three labels on a directed length-2 neighborhood and outputs one of two colors.

        Instances For
          source
          def Distributed2Coloring.ClassicalAlgorithm.pEvent (alg : ClassicalAlgorithm) :
          Set (Samples 4)

          The event that a fixed oriented edge is monochromatic.

          We represent an oriented edge by four consecutive i.i.d. labels x 0, x 1, x 2, x 3; the two endpoints apply the same local rule to the overlapping triples (x0,x1,x2) and (x1,x2,x3).

          Equations
          Instances For
            source
            noncomputable def Distributed2Coloring.ClassicalAlgorithm.p (alg : ClassicalAlgorithm) :
            ENNReal

            The monochromatic-edge probability of a one-round algorithm on the directed cycle.

            Equations
            Instances For
              source
              theorem Distributed2Coloring.ClassicalAlgorithm.measurable_fstTriple :
              Measurable fun (x : Samples 4) => (x 0, x 1, x 2)
              source
              theorem Distributed2Coloring.ClassicalAlgorithm.measurable_sndTriple :
              Measurable fun (x : Samples 4) => (x 1, x 2, x 3)
              source
              theorem Distributed2Coloring.ClassicalAlgorithm.measurable_nodeColor₀ (alg : ClassicalAlgorithm) :
              Measurable fun (x : Samples 4) => alg.f (x 0, x 1, x 2)
              source
              theorem Distributed2Coloring.ClassicalAlgorithm.measurable_nodeColor₁ (alg : ClassicalAlgorithm) :
              Measurable fun (x : Samples 4) => alg.f (x 1, x 2, x 3)
              source
              theorem Distributed2Coloring.ClassicalAlgorithm.measurableSet_pEvent (alg : ClassicalAlgorithm) :
              MeasurableSet alg.pEvent

              The finite digraph model for the lower bound #

              The lower bound reduces to a purely finite problem on a digraph G_n: