The collision estimate for empirical mixing measures (issue #33, existence step 5) #
The empirical hom-density integrals of an exchangeable graph law converge to its upper masses, quantitatively:
Graphon.ExchangeableGraphLaw.sum_upperEvent_comap— the restriction identity from consistency, inℝ≥0∞: for every injectione, the upper-event mass of then-vertex law alongeis the upper mass of thek-vertex law;GraphonSpace.abs_integral_homDensityCoord_empiricalMixing_sub_le— the collision estimate: for every exchangeable lawL,|∫ homDensityCoord F d(empiricalMixing L (n+1)) − ∑_{G ⊇ F} (L.law k G).toReal| ≤ k²/(n+1). Injective maps contribute the exact upper mass by consistency; non-injective maps are bounded by their proportion.GraphonSpace.abs_mixturePMF_empiricalMixing_sub_le— the induced-marginal bound: each marginal mass of the empirical mixing measure is withink²/(n+1)of the law's mass (exact-event analogue of the collision estimate, viasampleMass_ofSimpleGraphOnandlaw_eq_sum_comap).GraphonSpace.exists_mixtureExchangeableLaw_eq— the existence half of the Diaconis–Janson correspondence: every exchangeable graph law is the mixture law of a probability measure on the graphon space. A Prokhorov subsequential limit of the empirical mixing measures (exists_subseq_tendsto) has the correct hom-density integrals by weak convergence plus the collision estimate, hence the correct marginals by upper-sum injectivity (integral_homDensityCoord+pmf_ext_of_upperSum).
Combined with mixtureExchangeableLaw_injective (Graphon/MixtureUniqueness.lean),
this makes the mixture map a bijection — the full representation theorem is assembled
next.
The exact-event restriction identity from consistency (in ℝ≥0∞): for any
injection of labels, each k-vertex mass is the total n-vertex mass of its exact
preimage event.
The restriction identity from consistency (in ℝ≥0∞): for any injection of
labels, the mass of the upper event F ≤ ·.comap e under the n-vertex law is the
upper mass of F under the k-vertex law.
The collision estimate (issue #33, existence step 5): the empirical hom-density
integral of an exchangeable law at size n + 1 is within k²/(n + 1) of the upper mass
of F under the k-vertex marginal. Injective vertex maps contribute the exact upper
mass by consistency (sum_upperEvent_comap); non-injective maps are controlled by the
birthday bound (Graphon.card_not_injective_le).
The induced-marginal bound: each k-vertex marginal mass of the empirical
mixing measure at size n + 1 is within k²/(n + 1) of the law's mass. Injective
vertex maps contribute the exact mass by consistency (law_eq_sum_comap);
non-injective maps are controlled by the birthday bound.
Every weak limit of empirical mixing measures along a diverging index sequence represents the law: weak convergence and the collision estimate identify every hom-density integral of the limit, and upper-sum injectivity identifies the marginals.
The existence half of the Diaconis–Janson correspondence (issue #33): every exchangeable graph law is the mixture law of a probability measure on the graphon space, obtained as a Prokhorov subsequential limit of the empirical mixing measures.