The exact finite-sampling formula (issue #33, existence step 5, part 1) #
Sampling k vertices from the embedded graphon of a finite graph H on n vertices
is exactly uniform sampling of a vertex map Fin k → Fin n followed by pulling back:
Graphon.homDensity_ofSimpleGraphOn— the homomorphism density ofFin the embedded graphon is the average over all mapsfof the indicatorF ≤ H.comap f(the now-public step-graphon enginehomDensity_mkStepGraphon_eq_weightedHomSum, specialized to the equipartition);Graphon.sampleMass_ofSimpleGraphOn— the exact finite-sampling formula:sampleMass (ofSimpleGraphOn H) G = n⁻ᵏ ∑_f [H.comap f = G], byupperSum_injective(both sides have upper transform equal to the hom density).
The collision bound (splitting maps into injective and noninjective) and the identification of the empirical mixing limits build on this in the next step.
theorem
Graphon.homDensity_ofSimpleGraphOn
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsProbabilityMeasure μ]
[StandardBorelSpace α]
[MeasureTheory.NullSingletonClass μ]
{n : ℕ}
[NeZero n]
(H : SimpleGraph (Fin n))
{k : ℕ}
(F : SimpleGraph (Fin k))
[DecidableRel F.Adj]
:
homDensity F (ofSimpleGraphOn H) = (↑n)⁻¹ ^ k * ∑ f : Fin k → Fin n, if F ≤ SimpleGraph.comap f H then 1 else 0
Hom densities in an embedded finite graph are map averages: the density of F
in ofSimpleGraphOn H is the proportion of vertex maps f with F ≤ H.comap f.
theorem
Graphon.sampleMass_ofSimpleGraphOn
{α : Type u_1}
[MeasurableSpace α]
{μ : MeasureTheory.Measure α}
[MeasureTheory.IsProbabilityMeasure μ]
[StandardBorelSpace α]
[MeasureTheory.NullSingletonClass μ]
{n : ℕ}
[NeZero n]
(H : SimpleGraph (Fin n))
{k : ℕ}
(G : SimpleGraph (Fin k))
:
(ofSimpleGraphOn H).sampleMass G = (↑n)⁻¹ ^ k * ∑ f : Fin k → Fin n, if SimpleGraph.comap f H = G then 1 else 0
The exact finite-sampling formula (Diaconis–Janson existence, step 5 part 1):
the sample mass of G under the embedded graphon of H is the proportion of vertex
maps f : Fin k → Fin n with H.comap f = G.