Finite subgraph densities: t, t_inj, t_ind (#94, PR 1)

The three classical labeled subgraph densities of a finite target graph (Lovász, Large networks and graph limits, §5.2), with their normalization conventions, and the direct bridges to this repo's finite graphon-sampling formulas:

• SimpleGraph.homCount / SimpleGraph.t — adjacency-preserving vertex maps, normalized by all n ^ k maps (the homomorphism density);
• SimpleGraph.injHomCount / SimpleGraph.tInj — injective adjacency-preserving maps, normalized by the n.descFactorial k injective maps;
• SimpleGraph.indCount / SimpleGraph.tInd — injective maps pulling the target back to exactly F (labeled induced copies), same normalizer;
• SimpleGraph.pullbackCount — the all-maps exact-pullback count, the combinatorial content of the sampling mass; the analytic bridges to the empirical-graphon formulas live in Graphon.SubgraphDensityBridges (keeping this file's import closure to pure combinatorics).

Small-host convention: for n < k there are no injective maps, n.descFactorial k = 0, and (division by zero being zero) tInj and tInd are zero — recorded as tInj_eq_zero_of_lt / tInd_eq_zero_of_lt, which is what makes the Möbius sum identity unconditional.

PR 2 of #94 adds, still in the pure closure (source crosswalk: Lovász, Large networks and graph limits, §5.2.3): tInj_eq_sum_tInd — the zeta identity (5.19), t_inj(F, ·) = ∑_{F' ⊇ F} t_ind(F', ·); tInd_eq_sum_neg_one_pow_tInj — the inverse Möbius identity (5.20), t_ind(F, ·) = ∑_{F' ⊇ F} (−1)^{|E(F') ∖ E(F)|} t_inj(F', ·); and the collision comparisons (5.21) abs_t_sub_tInj_le / abs_pullbackCount_div_sub_tInd_le (≤ k²/n), whose empirical-graphon forms live in Graphon.SubgraphDensityBridges.

noncomputable def SimpleGraph.homCount {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : ℕ

The labeled homomorphism count: vertex maps carrying every edge of F to an edge of H.

Equations

• F.homCount H = {f : Fin k → Fin n | F ≤ SimpleGraph.comap f H}.card

noncomputable def SimpleGraph.injHomCount {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : ℕ

The injective homomorphism count.

Equations

• F.injHomCount H = {f : Fin k → Fin n | Function.Injective f ∧ F ≤ SimpleGraph.comap f H}.card

noncomputable def SimpleGraph.indCount {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : ℕ

The labeled induced-copy count: injective vertex maps pulling H back to exactly F.

Equations

• F.indCount H = {f : Fin k → Fin n | Function.Injective f ∧ SimpleGraph.comap f H = F}.card

noncomputable def SimpleGraph.pullbackCount {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : ℕ

The all-maps exact-pullback count — the combinatorial content of the sampling mass of the empirical graphon (no injectivity; collisions allowed).

Equations

• F.pullbackCount H = {f : Fin k → Fin n | SimpleGraph.comap f H = F}.card

noncomputable def SimpleGraph.t {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : ℝ

The homomorphism density t(F, H): the proportion of all n ^ k vertex maps that are homomorphisms.

Equations

• F.t H = ↑(F.homCount H) / ↑n ^ k

noncomputable def SimpleGraph.tInj {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : ℝ

The injective homomorphism density t_inj(F, H): the proportion of the n.descFactorial k injective vertex maps that are homomorphisms. For n < k there are no injective maps and the convention is tInj = 0 (division by the zero descending factorial).

Equations

• F.tInj H = ↑(F.injHomCount H) / ↑(n.descFactorial k)

noncomputable def SimpleGraph.tInd {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : ℝ

The induced density t_ind(F, H): the proportion of the n.descFactorial k injective vertex maps that induce exactly F. For n < k there are no injective maps and the convention is tInd = 0 (division by the zero descending factorial).

Equations

• F.tInd H = ↑(F.indCount H) / ↑(n.descFactorial k)

Normalization sanity

theorem SimpleGraph.homCount_le {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : F.homCount H ≤ n ^ k

theorem SimpleGraph.injHomCount_le {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : F.injHomCount H ≤ n.descFactorial k

theorem SimpleGraph.indCount_le {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : F.indCount H ≤ n.descFactorial k

theorem SimpleGraph.t_nonneg {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : 0 ≤ F.t H

theorem SimpleGraph.t_le_one {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : F.t H ≤ 1

theorem SimpleGraph.tInj_nonneg {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : 0 ≤ F.tInj H

theorem SimpleGraph.tInj_le_one {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : F.tInj H ≤ 1

theorem SimpleGraph.tInd_nonneg {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : 0 ≤ F.tInd H

theorem SimpleGraph.tInd_le_one {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : F.tInd H ≤ 1

The Möbius sum identity and the collision comparison (#94, PR 2)

theorem SimpleGraph.injHomCount_eq_sum_indCount {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : F.injHomCount H = ∑ F' : SimpleGraph (Fin k) with F ≤ F', F'.indCount H

Fiberwise classification: an injective homomorphism pulls the host back to a unique supergraph of F, so the injective homomorphism count is the sum of the induced-copy counts over the supergraphs of F.

theorem SimpleGraph.tInj_eq_sum_tInd {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : F.tInj H = ∑ F' : SimpleGraph (Fin k) with F ≤ F', F'.tInd H

The Möbius sum identity: the injective density is the upper sum of the induced densities over the supergraphs of F — unconditional, thanks to the small-host zero convention on both sides.

theorem SimpleGraph.tInd_eq_sum_neg_one_pow_tInj {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : F.tInd H = ∑ F' : SimpleGraph (Fin k) with F ≤ F', (-1) ^ (F'.edgeFinset \ F.edgeFinset).card * F'.tInj H

The inverse Möbius identity (Lovász (5.20)): the induced density is the signed sum of the injective densities over the supergraphs, with sign the parity of the added edges — unconditional, by the small-host zero convention.

theorem SimpleGraph.abs_t_sub_tInj_le {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : |F.t H - F.tInj H| ≤ ↑k ^ 2 / ↑n

The collision comparison (Lovász, Large networks and graph limits, (5.21)-style): the homomorphism density and the injective homomorphism density differ by at most k²/n — both sides of the decomposition are bounded by the non-injective proportion, which the birthday bound controls.

theorem SimpleGraph.abs_pullbackCount_div_sub_tInd_le {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) : |↑(F.pullbackCount H) / ↑n ^ k - F.tInd H| ≤ ↑k ^ 2 / ↑n

The collision comparison for exact pullbacks: the all-maps exact-pullback proportion (the sampling mass of the empirical graphon) and the induced density differ by at most k²/n.

theorem SimpleGraph.tInj_eq_zero_of_lt {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) (h : n < k) : F.tInj H = 0

Small-host convention: tInj vanishes when the host is smaller than the pattern.

theorem SimpleGraph.tInd_eq_zero_of_lt {k n : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin n)) (h : n < k) : F.tInd H = 0

Small-host convention: tInd vanishes when the host is smaller than the pattern.