Homomorphism densities of the smallest graphs

The two homomorphism densities that the rest of the theory quotes by name:

t(K₂, W) = ∫∫ W(x, y)                              the edge density
t(K₃, W) = ∫∫∫ W(x, y) W(x, z) W(y, z)             the triangle density

Each is given twice: once as an integral against a product measure, and once in the iterated form above. The two are related by integral_prod, which needs the integrand to be integrable, so those integrability lemmas are part of the public interface rather than hidden inside a proof. They are proved for an arbitrary graph by transporting integrable_homDensity_integrand along the same equivalence that transports the density, so no measurability or boundedness argument is repeated.

The transport is separated from the graph. homDensity integrates over the function space Fin n → Ω, and moving to Ω × ⋯ × Ω is independent of which graph is being counted. That step is therefore proved once, for an arbitrary graph, as homDensity_fin_two, homDensity_fin_three, and homDensity_fin_four; each concrete value below is then just its edge set (computed by decide) substituted into the general statement. A further entry in this catalogue — a single edge on three vertices, a path, the empty graph — costs only that substitution.

Where the transports come from. For two vertices it is Mathlib's MeasurableEquiv.finTwoArrow with measurePreserving_finTwoArrow. Mathlib supplies no (Fin 3 → Ω) ≃ᵐ Ω × Ω × Ω, so the three-vertex one is composed here as finThreeArrow, out of MeasurableEquiv.piFinSuccAbove and finTwoArrow, with measure preservation assembled from the corresponding two Mathlib lemmas. It sends x to (x 0, x 1, x 2) definitionally; finThreeArrow_apply records that by rfl so the coordinate matching in the proofs is an explicit rewrite rather than a silent unfolding. The four-vertex transport similarly pairs the coordinates as ((x 0, x 2), (x 1, x 3)) for the four-cycle formulas.

Main results

• homDensity_fin_two, homDensity_fin_three, homDensity_fin_four — the graph-independent transports;
• homDensity_top_fin_two and homDensity_top_fin_two_eq_integral_integral — the edge density;
• homDensity_top_fin_three and homDensity_top_fin_three_eq_integral_integral_integral — the triangle density;
• homDensity_cycleGraph_four, integrable_cycleGraph_four — the 4-cycle density and its integrability;
• integrable_prod_edgeFactor_fin_two, integrable_prod_edgeFactor_fin_three, integrable_prod_edgeFactor_fin_four — integrability of the transported integrand, again for an arbitrary graph;
• integrable_edge_integrand, integrable_triangle_integrand — the same for the two expanded integrands, so a consumer of either iterated form has the hypothesis integral_prod needs.

References

• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 1 — the explicit small-graph integrals, and the Layer 1 acceptance criteria "a one-edge graph" and "triangle density". Disjoint-union multiplicativity, finite-graph compatibility, and the counting lemmas are separate targets and are not built here.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §7.2.

theorem TauCeti.DenseGraphLimits.homDensity_fin_two {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph (Fin 2)) [DecidableRel F.Adj] (W : Graphon Ω μ) : homDensity F W = ∫ (p : Ω × Ω), ∏ e ∈ F.edgeFinset, edgeFactor W ![p.1, p.2] e ∂μ.prod μ

The two-vertex transport. For any graph on Fin 2, the homomorphism density is an integral over Ω × Ω. This is independent of the graph; the concrete values below only substitute an edge set into it.

theorem TauCeti.DenseGraphLimits.homDensity_fin_three {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph (Fin 3)) [DecidableRel F.Adj] (W : Graphon Ω μ) : homDensity F W = ∫ (p : Ω × Ω × Ω), ∏ e ∈ F.edgeFinset, edgeFactor W ![p.1, p.2.1, p.2.2] e ∂μ.prod (μ.prod μ)

The three-vertex transport. For any graph on Fin 3, the homomorphism density is an integral over Ω × Ω × Ω.

theorem TauCeti.DenseGraphLimits.integrable_prod_edgeFactor_fin_two {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph (Fin 2)) [DecidableRel F.Adj] (W : Graphon Ω μ) : MeasureTheory.Integrable (fun (p : Ω × Ω) => ∏ e ∈ F.edgeFinset, edgeFactor W ![p.1, p.2] e) (μ.prod μ)

Transported integrability, two vertices. For any graph on Fin 2, the transported integrand is integrable — obtained from integrable_homDensity_integrand along the same equivalence that transports the density, so no measurability or bound is re-argued.

theorem TauCeti.DenseGraphLimits.integrable_prod_edgeFactor_fin_three {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph (Fin 3)) [DecidableRel F.Adj] (W : Graphon Ω μ) : MeasureTheory.Integrable (fun (p : Ω × Ω × Ω) => ∏ e ∈ F.edgeFinset, edgeFactor W ![p.1, p.2.1, p.2.2] e) (μ.prod (μ.prod μ))

Transported integrability, three vertices.

theorem TauCeti.DenseGraphLimits.homDensity_fin_four {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph (Fin 4)) [DecidableRel F.Adj] (W : Graphon Ω μ) : homDensity F W = ∫ (p : (Ω × Ω) × Ω × Ω), ∏ e ∈ F.edgeFinset, edgeFactor W ![p.1.1, p.2.1, p.1.2, p.2.2] e ∂(μ.prod μ).prod (μ.prod μ)

The four-vertex transport. For any graph on Fin 4, the homomorphism density is an integral over two copies of Ω × Ω, with the coordinates paired for the four-cycle formulas.

theorem TauCeti.DenseGraphLimits.integrable_prod_edgeFactor_fin_four {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (F : SimpleGraph (Fin 4)) [DecidableRel F.Adj] (W : Graphon Ω μ) : MeasureTheory.Integrable (fun (p : (Ω × Ω) × Ω × Ω) => ∏ e ∈ F.edgeFinset, edgeFactor W ![p.1.1, p.2.1, p.1.2, p.2.2] e) ((μ.prod μ).prod (μ.prod μ))

Transported integrability, four vertices. For any graph on Fin 4, the transported integrand is integrable on the paired product space.

theorem TauCeti.DenseGraphLimits.integrable_cycleGraph_four {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : MeasureTheory.Integrable (fun (p : (Ω × Ω) × Ω × Ω) => W p.1.1 p.2.1 * W p.2.1 p.1.2 * W p.1.2 p.2.2 * W p.2.2 p.1.1) ((μ.prod μ).prod (μ.prod μ))

The four-cycle integrand is integrable on the paired product space.

theorem TauCeti.DenseGraphLimits.homDensity_cycleGraph_four {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : homDensity (SimpleGraph.cycleGraph 4) W = ∫ (p : (Ω × Ω) × Ω × Ω), W p.1.1 p.2.1 * W p.2.1 p.1.2 * W p.1.2 p.2.2 * W p.2.2 p.1.1 ∂(μ.prod μ).prod (μ.prod μ)

The four-cycle density. The homomorphism density of C₄ is the integral of its four edge product over the paired product space.

theorem TauCeti.DenseGraphLimits.integrable_edge_integrand {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : MeasureTheory.Integrable (fun (p : Ω × Ω) => W p.1 p.2) (μ.prod μ)

The edge integrand is integrable, by transport from integrable_prod_edgeFactor_fin_two.

theorem TauCeti.DenseGraphLimits.integrable_triangle_integrand {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : MeasureTheory.Integrable (fun (p : Ω × Ω × Ω) => W p.1 p.2.1 * W p.1 p.2.2 * W p.2.1 p.2.2) (μ.prod (μ.prod μ))

The triangle integrand is integrable, by transport from integrable_prod_edgeFactor_fin_three.

theorem TauCeti.DenseGraphLimits.homDensity_top_fin_two {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : homDensity ⊤ W = ∫ (p : Ω × Ω), W p.1 p.2 ∂μ.prod μ

The edge density. The homomorphism density of the one-edge graph K₂ is the integral of the graphon over the whole square.

theorem TauCeti.DenseGraphLimits.homDensity_top_fin_two_eq_integral_integral {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : homDensity ⊤ W = ∫ (x : Ω), ∫ (y : Ω), W x y ∂μ ∂μ

The edge density as an iterated integral.

theorem TauCeti.DenseGraphLimits.homDensity_top_fin_three {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : homDensity ⊤ W = ∫ (p : Ω × Ω × Ω), W p.1 p.2.1 * W p.1 p.2.2 * W p.2.1 p.2.2 ∂μ.prod (μ.prod μ)

The triangle density. The homomorphism density of K₃ is the integral of the product of the graphon over the three edges of a triple of points.

theorem TauCeti.DenseGraphLimits.homDensity_top_fin_three_eq_integral_integral_integral {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : homDensity ⊤ W = ∫ (x : Ω), ∫ (y : Ω), ∫ (z : Ω), W x y * W x z * W y z ∂μ ∂μ ∂μ

The triangle density as an iterated integral.