Documentation

TauCeti.Combinatorics.DenseGraphLimits.ExchangeableGraphLaw.Infinite.Correspondence

Graphon mixtures and exchangeable laws on infinite graphs #

Every exchangeable probability law on infinite graphs corresponds to a unique probability measure on the graphon quotient. The correspondence transports the finite-marginal mixture equivalence through extension to infinite graphs. Its finite upper masses are integrals of homomorphism densities. Dirac mixing measures give the joint sampling law of one graphon.

This is the graphon-mixture correspondence of Diaconis and Janson, Graph limits and exchangeable random graphs, Section 5.

source
noncomputable def TauCeti.DenseGraphLimits.graphonMixtureLawEquiv :
MeasureTheory.ProbabilityMeasure GraphonSpaceI ≃ InfiniteExchangeableGraphLaw

The Diaconis–Janson correspondence between mixing measures on graphon space and exchangeable probability laws on infinite graphs.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.DenseGraphLimits.graphonMixtureLawEquiv_apply (P : MeasureTheory.ProbabilityMeasure GraphonSpaceI) :
    graphonMixtureLawEquiv P = exchangeableGraphLawEquivInfinite (mixtureExchangeableLaw P)

    The correspondence sends a mixing measure to the extension of its finite-window mixture law.

    source
    theorem TauCeti.DenseGraphLimits.graphonMixtureLawEquiv_dirac (W : Graphon (↑unitInterval) MeasureTheory.volume) :
    graphonMixtureLawEquiv (MeasureTheory.diracProba (SeparationQuotient.mk W)) = exchangeableGraphLawEquivInfinite (sampleExchangeableLaw W)

    A Dirac mixing measure gives the infinite joint sampling law of its graphon.

    source
    theorem TauCeti.DenseGraphLimits.graphonMixtureLawEquiv_upperMass (P : MeasureTheory.ProbabilityMeasure GraphonSpaceI) {k : ℕ} (F : SimpleGraph (Fin k)) [DecidableRel F.Adj] :
    (exchangeableGraphLawEquivInfinite.symm (graphonMixtureLawEquiv P)).upperMass F = ∫ (x : GraphonSpaceI), homDensityOnSpace F x ∂↑P

    The upper mass of each finite window of a graphon mixture is the mixing average of its homomorphism density.