Documentation

TauCeti.Combinatorics.DenseGraphLimits.ExchangeableGraphLaw.Extreme

Extreme exchangeable graph laws #

The exchangeable probability measures on the graphs on ℕ form a convex set, exchangeableGraphProbabilityMeasures. Its extreme points are the dissociated laws: an exchangeable law on infinite graphs is an extreme point if and only if its finite law is dissociated (mem_extremePoints_iff_isDissociated). This is the graph-side form of the characterisation of joint dissociation as extremality among jointly exchangeable array laws, for callers who work with graph laws; the two convex sets correspond under the graph-law/array-law adapter (arrayLaw_mem_iff, mem_extremePoints_iff_arrayLaw_mem_extremePoints).

Two consequences. The infinite sampling law of a graphon is an extreme exchangeable graph measure (infiniteSampleLaw_mem_extremePoints). And a dissociated exchangeable graph law does not mix: a mixture of exchangeable graph laws equal to it has almost every component equal to it (InfiniteExchangeableGraphLaw.ae_eq_of_comp_eq), the graph counterpart of JointlyDissociated.ae_eq_of_comp_eq; it is the uniqueness input for representing an exchangeable graph law as a mixture of dissociated ones. Both conclude equality of laws.

Main results #

References #

source
def TauCeti.DenseGraphLimits.exchangeableGraphProbabilityMeasures :
Set (MeasureTheory.Measure (SimpleGraph ℕ))

The convex set of exchangeable probability measures on the graphs on ℕ.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.DenseGraphLimits.mem_exchangeableGraphProbabilityMeasures_iff {μ : MeasureTheory.Measure (SimpleGraph ℕ)} :
    μ ∈ exchangeableGraphProbabilityMeasures ↔ (∀ (σ : Equiv.Perm ℕ), MeasureTheory.Measure.map (SimpleGraph.comap ⇑σ) μ = μ) ∧ MeasureTheory.IsProbabilityMeasure μ

    Membership in the exchangeable probability measures on graphs.

    source
    theorem TauCeti.DenseGraphLimits.arrayLaw_mem_iff {μ : MeasureTheory.Measure (SimpleGraph ℕ)} :
    arrayLaw μ ∈ Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag Bool false ↔ μ ∈ exchangeableGraphProbabilityMeasures

    A law on graphs is an exchangeable probability measure exactly when its array law is a jointly exchangeable probability law carried by the symmetric false-diagonal arrays.

    source
    theorem TauCeti.DenseGraphLimits.convex_exchangeableGraphProbabilityMeasures :
    Convex ENNReal exchangeableGraphProbabilityMeasures

    The exchangeable probability measures on graphs form a convex set.

    source
    theorem TauCeti.DenseGraphLimits.mem_extremePoints_iff_arrayLaw_mem_extremePoints {μ : MeasureTheory.Measure (SimpleGraph ℕ)} :
    μ ∈ Set.extremePoints ENNReal exchangeableGraphProbabilityMeasures ↔ arrayLaw μ ∈ Set.extremePoints ENNReal (Probability.jointlyExchangeableProbabilityMeasuresOnSymmetricArraysWithDiag Bool false)

    Extremality transports along the adapter: a law on graphs is extreme among exchangeable probability measures exactly when its array law is extreme among the jointly exchangeable laws carried by the symmetric arrays. The array law and the graph law are mutually inverse affine maps between the two convex sets.

    source
    @[simp]
    theorem TauCeti.DenseGraphLimits.mem_extremePoints_iff_isDissociated (L : InfiniteExchangeableGraphLaw) :
    L.law ∈ Set.extremePoints ENNReal exchangeableGraphProbabilityMeasures ↔ (exchangeableGraphLawEquivInfinite.symm L).IsDissociated

    Extremality is dissociation: an exchangeable law on infinite graphs is an extreme point of the exchangeable probability measures on graphs if and only if its finite law is dissociated.

    source
    theorem TauCeti.DenseGraphLimits.infiniteSampleLaw_mem_extremePoints {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) :
    infiniteSampleLaw W ∈ Set.extremePoints ENNReal exchangeableGraphProbabilityMeasures

    The infinite sampling law of a graphon is an extreme exchangeable graph measure.

    source
    theorem TauCeti.DenseGraphLimits.InfiniteExchangeableGraphLaw.ae_eq_of_comp_eq {Z : Type u_1} [MeasurableSpace Z] (L : InfiniteExchangeableGraphLaw) (hL : (exchangeableGraphLawEquivInfinite.symm L).IsDissociated) {π : MeasureTheory.Measure Z} {κ : ProbabilityTheory.Kernel Z (SimpleGraph ℕ)} [ProbabilityTheory.IsMarkovKernel κ] (hκ : ∀ᵐ (z : Z) ∂π, ∀ (σ : Equiv.Perm ℕ), MeasureTheory.Measure.map (SimpleGraph.comap ⇑σ) (κ z) = κ z) (hmix : π.bind ⇑κ = L.law) :
    ∀ᵐ (z : Z) ∂π, κ z = L.law

    A dissociated graph law does not mix: a mixture of exchangeable graph laws equal to a dissociated exchangeable graph law has almost every component equal to that law.