Documentation

TauCeti.Combinatorics.DenseGraphLimits.HomDensity.Finite

Homomorphism densities in a finite graph #

Two densities of a finite pattern graph F in a finite host graph G:

These are the finite-graph front of the sampling theory. Nothing here is about graphons, and nothing here samples: these are the estimators the later sampling laws are estimators of.

The falling factorial, not the binomial coefficient #

injHomDensity divides by (Fintype.card W).descFactorial (Fintype.card V), the number of ordered injections of a |V(F)|-element set into V(G). Its numerator counts ordered injective homomorphisms, so the two agree as conventions. Dividing instead by Nat.choose would count unordered images against ordered maps and bias the sampling estimator by |V(F)|! — the later unbiasedness identity would read k! · t(F, W) rather than t(F, W). The convention is fixed here so that no downstream statement has to carry the correction.

One counting convention, not two #

injHomDensity_eq_labelledCopyCount_div rewrites the numerator of injHomDensity as Mathlib's SimpleGraph.labelledCopyCount, through the counting bridge SimpleGraph.card_injective_hom_eq_labelledCopyCount. Without it, injHomDensity would silently establish a second counting convention alongside Mathlib's. Note that Mathlib puts the host graph first, so the copy count of F inside G is G.labelledCopyCount F.

This settles the numerator. Mathlib has no hom-density primitive, so nothing here pins the descFactorial denominator; that convention is chosen here and is pinned later by the unbiasedness anchor integral_injHomDensity_sampleGraph.

Counting with Nat.card #

Both densities count with Nat.card, which is total: it returns 0 on an infinite type and needs no Fintype instance or decidability on the hom type, on G, or on G.Adj. The counted types are finite here, so no generality is lost — but the definitions can be stated and rewritten without carrying decidability hypotheses that the analytic statements downstream would then inherit.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.DenseGraphLimits.homDensityFin {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) :
ℝ

The homomorphism density t(F, G) = |Hom(F, G)| / |V(G)| ^ |V(F)| of a finite pattern graph F in a finite host graph G.

Counted with Nat.card, so no Fintype or decidability instance on the hom type or on G is required. Use homDensityFin_def to unfold.

Equations
Instances For
    source
    noncomputable def TauCeti.DenseGraphLimits.injHomDensity {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) :
    ℝ

    The injective homomorphism density t₀(F, G): ordered injective homomorphisms over the falling factorial (|V(G)|)_{|V(F)|}.

    The denominator counts ordered injections V ↪ W, matching the ordered numerator. Nat.choose would not: it counts unordered images, and would bias the sampling estimator by |V(F)|!. Use injHomDensity_def to unfold.

    Equations
    Instances For
      source
      theorem TauCeti.DenseGraphLimits.homDensityFin_def {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) :
      homDensityFin F G = ↑(Nat.card (F →g G)) / ↑(Fintype.card W) ^ Fintype.card V

      The defining equation of homDensityFin. The definition's body is not exposed, so this is the lemma downstream modules should rewrite with.

      source
      theorem TauCeti.DenseGraphLimits.injHomDensity_def {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) :
      injHomDensity F G = ↑(Nat.card { φ : F →g G // Function.Injective ⇑φ }) / ↑((Fintype.card W).descFactorial (Fintype.card V))

      The defining equation of injHomDensity. The definition's body is not exposed, so this is the lemma downstream modules should rewrite with.

      The bridge to Mathlib's counting primitive #

      source
      theorem TauCeti.DenseGraphLimits.injHomDensity_eq_labelledCopyCount_div {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) :
      injHomDensity F G = ↑(G.labelledCopyCount F) / ↑((Fintype.card W).descFactorial (Fintype.card V))

      The injective homomorphism density in terms of Mathlib's labelled copy count.

      Both densities lie in [0, 1] #

      source
      theorem TauCeti.DenseGraphLimits.homDensityFin_nonneg {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) :
      0 ≤ homDensityFin F G

      The homomorphism density is nonnegative.

      source
      theorem TauCeti.DenseGraphLimits.homDensityFin_le_one {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) :
      homDensityFin F G ≤ 1

      The homomorphism density is at most 1, since every homomorphism is in particular a function V(F) → V(G).

      No hypothesis is needed. When the host is empty and the pattern is not, numerator and denominator both vanish and x / 0 = 0 gives 0.

      source
      theorem TauCeti.DenseGraphLimits.injHomDensity_nonneg {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) :
      0 ≤ injHomDensity F G

      The injective homomorphism density is nonnegative.

      source
      theorem TauCeti.DenseGraphLimits.injHomDensity_le_one {V : Type u_1} {W : Type u_2} [Fintype V] [Fintype W] (F : SimpleGraph V) (G : SimpleGraph W) :
      injHomDensity F G ≤ 1

      The injective homomorphism density is at most 1, since every injective homomorphism is in particular an embedding V(F) ↪ V(G), and those are counted by the falling factorial.

      No hypothesis is needed; the degenerate cases behave as for homDensityFin_le_one.