The homomorphism-density coordinate algebra (issue #33, uniqueness bricks 1–2)

The uniqueness half of the Diaconis–Janson correspondence runs through the algebra of descended homomorphism-density coordinates on the graphon space. This file provides its first two bricks:

• GraphonSpace.homDensityCoord — homomorphism densities descend to continuous coordinates on the graphon space (well-defined by the counting lemma, continuous by Lipschitz continuity in cut distance), each a finite upper sum of sampleMassCoords (homDensityCoord_eq_sum_sampleMassCoord), and jointly point-separating;
• Graphon.homDensity_sum — multiplicativity over disjoint unions: homDensity (F ⊕g H) W = homDensity F W * homDensity H W. Proof: F ⊕g H is the sup of the two vertex-embedded copies, whose edge sets are disjoint, so the integrand factors pointwise (Quot.out orientation is absorbed by the range lemma out_mem_range_of_mem_edgeFinset_map and by homDensity_map_embedding); the pi integral over V ⊕ V' splits by measurePreserving_sumPiEquivProdPi_symm and integral_prod_mul, and each factor is homDensity of a mapped graph, which homDensity_map_embedding reduces to the original;
• Graphon.homDensity_sum_finAdd — the Fin (k + l) corollary via finSumFinEquiv, keeping the coordinate algebra indexed by graphs on Fin n.

Bricks 3–4 (the multiplicatively closed coordinate span and the Polish measure extensionality) complete the uniqueness theorem.

theorem Graphon.homDensity_sum {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} {V' : Type u_3} [Fintype V] [Fintype V'] [DecidableEq V] [DecidableEq V'] (F : SimpleGraph V) [DecidableRel F.Adj] (H : SimpleGraph V') [DecidableRel H.Adj] (W : Graphon α μ) : homDensity (F ⊕g H) W = homDensity F W * homDensity H W

Multiplicativity of homomorphism densities over disjoint unions.

theorem Graphon.homDensity_sum_finAdd {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k l : ℕ} (F : SimpleGraph (Fin k)) [DecidableRel F.Adj] (H : SimpleGraph (Fin l)) [DecidableRel H.Adj] (W : Graphon α μ) : homDensity (SimpleGraph.map (⇑finSumFinEquiv.toEmbedding) (F ⊕g H)) W = homDensity F W * homDensity H W

The Fin (k + l) coordinate form of disjoint-union multiplicativity, via finSumFinEquiv: keeps the coordinate algebra indexed by graphs on Fin n.

noncomputable def GraphonSpace.homDensityCoord {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) : GraphonSpace α μ → ℝ

The homomorphism-density coordinate: homDensity F · descends to the graphon space (well-defined by the counting lemma homDensity_eq_of_cutDistance_zero).

Equations

• GraphonSpace.homDensityCoord F = SeparationQuotient.lift (fun (W : Graphon α μ) => Graphon.homDensity F W) ⋯

@[simp]

theorem GraphonSpace.homDensityCoord_mk {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) (W : Graphon α μ) : homDensityCoord F (mk W) = Graphon.homDensity F W

theorem GraphonSpace.continuous_homDensityCoord {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) : Continuous (homDensityCoord F)

theorem GraphonSpace.homDensityCoord_eq_sum_sampleMassCoord {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} (F : SimpleGraph (Fin k)) (x : GraphonSpace α μ) : homDensityCoord F x = ∑ G : SimpleGraph (Fin k), if F ≤ G then sampleMassCoord G x else 0

The hom-density coordinates are finite upper sums of the sample-mass coordinates (the forward Möbius identity, descended): equal mixture marginals therefore give equal integrals of every hom-density coordinate.

theorem GraphonSpace.homDensityCoord_eq_all_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {x y : GraphonSpace α μ} : (∀ (k : ℕ) (F : SimpleGraph (Fin k)), homDensityCoord F x = homDensityCoord F y) ↔ x = y

The hom-density coordinates separate points of the graphon space (via the determination theorem).