Documentation

TauCeti.Combinatorics.DenseGraphLimits.ExchangeableGraphLaw.Sampling

The sampling laws of a graphon form an exchangeable graph law #

Sampling l independent points from a graphon and then tossing an independent coin for each unordered pair produces a law on SimpleGraph (Fin l). Those laws are consistent under restriction of the label set — that is TauCeti.DenseGraphLimits.sampleGraph_map_comap — so the whole family is an exchangeable graph law, which is what this file packages.

The upper mass of a pattern under a sampling law is its graphon homomorphism density: the sample contains F exactly when every edge of F wins its coin toss, whose conditional probability at fixed positions is the product of the edge factors of F. Hence sampling laws are dissociated: the upper masses of a disjoint union of patterns multiply because homomorphism densities do.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.DenseGraphLimits.sampleExchangeableLaw {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) :
ExchangeableGraphLaw

The sampling laws of a fixed graphon, packaged as an exchangeable graph law.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.DenseGraphLimits.sampleExchangeableLaw_law {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (k : ℕ) :
    (sampleExchangeableLaw W).law k = sampleGraph W k
    source
    @[simp]
    theorem TauCeti.DenseGraphLimits.upperMass_sampleExchangeableLaw {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ} (F : SimpleGraph (Fin k)) [DecidableRel F.Adj] (W : Graphon Ω μ) :
    (sampleExchangeableLaw W).upperMass F = homDensity F W

    The sampling anchor. The upper mass of a pattern under a graphon's sampling law is its homomorphism density: P(F ≤ G(k, W)) = t(F, W).

    source
    @[simp]
    theorem TauCeti.DenseGraphLimits.sampleGraph_Ici {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) {k : ℕ} (F : SimpleGraph (Fin k)) [DecidableRel F.Adj] :
    (sampleGraph W k) (Set.Ici F) = ENNReal.ofReal (homDensity F W)

    The probability that a graphon sample contains a pattern is the pattern's homomorphism density, as a measure of the upper ray at the pattern.

    source
    theorem TauCeti.DenseGraphLimits.sampleGraph_eq_of_forall_homDensity_eq {Ω₁ : Type u_2} {Ω₂ : Type u_3} [MeasurableSpace Ω₁] [MeasurableSpace Ω₂] {μ₁ : MeasureTheory.Measure Ω₁} {μ₂ : MeasureTheory.Measure Ω₂} [MeasureTheory.IsProbabilityMeasure μ₁] [MeasureTheory.IsProbabilityMeasure μ₂] (U : Graphon Ω₁ μ₁) (W : Graphon Ω₂ μ₂) (n : ℕ) (h : ∀ (F : SimpleGraph (Fin n)) [inst : DecidableRel F.Adj], homDensity F U = homDensity F W) :
    sampleGraph U n = sampleGraph W n

    Sampling laws are determined by homomorphism densities. Two graphons, on arbitrary probability carriers, with the same homomorphism density for every graph on n vertices have the same n-vertex sampling law: a law on the finite lattice of graphs is determined by its upper-ray masses, which are homomorphism densities.

    source
    theorem TauCeti.DenseGraphLimits.isDissociated_sampleExchangeableLaw {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) :
    (sampleExchangeableLaw W).IsDissociated

    Sampling laws are dissociated. Disjoint label windows of a graphon sample read disjoint sets of sampled points and coins. Through upper masses this is the multiplicativity of homomorphism densities over disjoint unions: the upper mass of a pattern is its homomorphism density, which is unchanged by relabelling the pattern into Fin (k + l).