Documentation

TauCeti.Combinatorics.DenseGraphLimits.StepGraphon.FiniteGraph.Basic

A finite graph as a graphon #

finiteGraphGraphon G is the graphon W_G of a finite graph G on Fin m: the step graphon on the m equal cells of (I, volume) taking the value 1 on the rectangle cell i × cell j when i ~ j in G, and 0 otherwise.

Its defining property is finite-graph compatibility: the graphon homomorphism density of a finite pattern F in W_G is the finite homomorphism density of F in G,

t(F, W_G) = hom(F, G) / m ^ |V(F)|,

which is homDensity_finiteGraphGraphon. That is what makes the graphon theory an extension of the finite theory rather than a parallel one: every finite graph sits in the graphon world with its densities unchanged, and the sampling and mixture layers read a sampled finite graph back as a point of the graphon space along this map.

Why the definition goes through ℕ #

finiteGraphGraphon has to be total in m, and there is no map I → Fin 0. The value is therefore read off G.map Fin.valEmbedding, the transport of G to a graph on ℕ in which every vertex outside [0, m) is isolated, evaluated at the ℕ-valued cell index unitInterval.cellIdx. At m = 0 that graph has no edges and finiteGraphGraphon G is the zero graphon — which is why homDensity_finiteGraphGraphon carries 0 < m: for a nonempty vertex type and a pattern with no edges the graphon density is 1, while there is no map V → Fin 0, so the finite density is 0 / 0 ^ |V(F)| = 0 / 0 = 0. (For an empty vertex type both sides are 1 even at m = 0.)

Symmetry of the value is then the symmetry of an adjacency relation, with no case analysis on m, and measurability is a composition through the countable discrete space ℕ × ℕ.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.DenseGraphLimits.finiteGraphGraphon {m : ℕ} (G : SimpleGraph (Fin m)) :
Graphon (↑unitInterval) MeasureTheory.volume

The graphon of a finite graph G on Fin m: the step graphon on the m equal cells of (I, volume) whose value on cell i × cell j is 1 if i ~ j in G and 0 otherwise.

The adjacency is read off G.map Fin.valEmbedding, the transport of G to ℕ, so that the definition is total in m; see the module docstring. Use finiteGraphGraphon_apply_fin and the rectangle lemmas finiteGraphGraphon_apply_of_adj, finiteGraphGraphon_apply_of_not_adj to evaluate in terms of the adjacency of G on Fin m.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.DenseGraphLimits.finiteGraphGraphon_apply {m : ℕ} (G : SimpleGraph (Fin m)) (x y : ↑unitInterval) :
    (finiteGraphGraphon G) x y = if (SimpleGraph.map (⇑Fin.valEmbedding) G).Adj (unitInterval.cellIdx m x) (unitInterval.cellIdx m y) then 1 else 0

    The defining value of finiteGraphGraphon, at the level of the ℕ-valued cell indices and the transported graph G.map Fin.valEmbedding.

    The lemmas below state the same value in terms of the adjacency of G on Fin m, which is the form callers should use.

    source
    @[simp]
    theorem TauCeti.DenseGraphLimits.finiteGraphGraphon_eq_const_zero (G : SimpleGraph (Fin 0)) :
    finiteGraphGraphon G = Graphon.const MeasureTheory.volume 0

    The graphon of the unique graph on the empty vertex type is the constant-zero graphon.

    source
    theorem TauCeti.DenseGraphLimits.finiteGraphGraphon_apply_of_adj {m : ℕ} {G : SimpleGraph (Fin m)} {x y : ↑unitInterval} {i j : Fin m} (hij : G.Adj i j) (hx : unitInterval.cellIdx m x = ↑i) (hy : unitInterval.cellIdx m y = ↑j) :
    (finiteGraphGraphon G) x y = 1

    On a rectangle cell i × cell j spanned by an edge of G, the graphon takes the value 1.

    source
    theorem TauCeti.DenseGraphLimits.finiteGraphGraphon_apply_of_not_adj {m : ℕ} {G : SimpleGraph (Fin m)} {x y : ↑unitInterval} {i j : Fin m} (hij : ¬G.Adj i j) (hx : unitInterval.cellIdx m x = ↑i) (hy : unitInterval.cellIdx m y = ↑j) :
    (finiteGraphGraphon G) x y = 0

    On a rectangle cell i × cell j spanned by a non-edge of G, the graphon takes the value 0.

    source
    theorem TauCeti.DenseGraphLimits.finiteGraphGraphon_apply_of_cellIdx_eq {m : ℕ} {G : SimpleGraph (Fin m)} {x y : ↑unitInterval} {i j : Fin m} [DecidableRel G.Adj] (hx : unitInterval.cellIdx m x = ↑i) (hy : unitInterval.cellIdx m y = ↑j) :
    (finiteGraphGraphon G) x y = if G.Adj i j then 1 else 0

    Evaluating the graphon of a finite graph on a rectangle of cells, in if-form.

    source
    @[simp]
    theorem TauCeti.DenseGraphLimits.finiteGraphGraphon_apply_fin {m : ℕ} (G : SimpleGraph (Fin m)) [DecidableRel G.Adj] (hm : 0 < m) (x y : ↑unitInterval) :
    (finiteGraphGraphon G) x y = if G.Adj ⟨unitInterval.cellIdx m x, ⋯⟩ ⟨unitInterval.cellIdx m y, ⋯⟩ then 1 else 0

    The value of finiteGraphGraphon at an arbitrary pair of points, in terms of the adjacency of G between the cells containing them.

    source
    noncomputable def TauCeti.DenseGraphLimits.finiteGraphGraphonOnFin {m : ℕ} [NeZero m] (G : SimpleGraph (Fin m)) :
    Graphon (Fin m) (ProbabilityTheory.uniformOn Set.univ)

    A graph on Fin m as a graphon on its uniform finite carrier.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.DenseGraphLimits.finiteGraphGraphonOnFin_apply {m : ℕ} [NeZero m] (G : SimpleGraph (Fin m)) (i j : Fin m) :
      (finiteGraphGraphonOnFin G) i j = if G.Adj i j then 1 else 0

      The uniform finite-carrier graphon is the adjacency indicator of G.

      source
      theorem TauCeti.DenseGraphLimits.finiteGraphGraphon_eq_comap {m : ℕ} [NeZero m] (G : SimpleGraph (Fin m)) :
      finiteGraphGraphon G = (finiteGraphGraphonOnFin G).comap (unitInterval.cellFin m) ⋯ MeasureTheory.volume

      The graphon of a finite graph is the pullback of its uniform-carrier graphon along the cells of the unit interval.

      source
      theorem TauCeti.DenseGraphLimits.prod_edgeFactor_finiteGraphGraphon {m : ℕ} {V : Type u_1} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (G : SimpleGraph (Fin m)) (x : V → ↑unitInterval) :
      ∏ e ∈ F.edgeFinset, edgeFactor (finiteGraphGraphon G) x e = if ∀ (a b : V), F.Adj a b → (SimpleGraph.map (⇑Fin.valEmbedding) G).Adj (unitInterval.cellIdx m (x a)) (unitInterval.cellIdx m (x b)) then 1 else 0

      The edge product is an adjacency-preservation indicator. For the graphon of a finite graph G, the product of edgeFactor over the edges of F is 1 exactly when every edge of F is carried to an edge of G by the cell index, and 0 otherwise.

      This is the pointwise identity that makes homDensity_finiteGraphGraphon a counting argument: it replaces the integrand of the graphon homomorphism density by an indicator, whose integral is then the proportion of cell-index tuples that are graph homomorphisms. Use it whenever the edge product of a finite-graph graphon has to be evaluated at a fixed tuple.

      source
      @[simp]
      theorem TauCeti.DenseGraphLimits.homDensity_finiteGraphGraphon {m : ℕ} {V : Type u_1} [Fintype V] (F : SimpleGraph V) [DecidableRel F.Adj] (hm : 0 < m) (G : SimpleGraph (Fin m)) :
      homDensity F (finiteGraphGraphon G) = homDensityFin F G

      Finite-graph compatibility. The graphon homomorphism density of F in the graphon of a finite graph G on Fin m is the finite homomorphism density of F in G:

      t(F, W_G) = hom(F, G) / m ^ |V(F)|.

      Positivity of m is needed when V is nonempty: at m = 0 and a pattern with no edges the left-hand side is 1, while the right-hand side is 0 / 0 = 0.