Extremality: dissociated exchangeable laws are the Dirac mixtures (issue #33)

The Diaconis–Janson extremality criterion (their Theorem 5.5), via upper-event factorization:

• Graphon.ExchangeableGraphLaw.upperMass — the total mass of the supergraphs of F under the k-vertex marginal;
• Graphon.ExchangeableGraphLaw.IsDissociated — upper events on disjoint vertex blocks are independent (cross-block edges remain unrestricted);
• GraphonSpace.isDissociated_mixtureExchangeableLaw_iff — a graphon mixture is dissociated iff the mixing measure is a Dirac. Dissociation applied to two copies of F says every hom-density coordinate has second moment equal to its squared mean, so each coordinate is a.s. constant; a countable intersection and point separation of the coordinates collapse the mixing measure to a point.
• GraphonSpace.isDissociated_sampleExchangeableLaw — the exchangeable law of a fixed graphon is dissociated (it is the Dirac mixture at its class);
• GraphonSpace.isDissociated_iff_exists_sampleExchangeableLaw — the arbitrary-law form: an exchangeable law is dissociated iff it is the sample law of a fixed graphon.

This proves the extremality criterion without formalizing the convex extreme-point structure itself.

noncomputable def Graphon.ExchangeableGraphLaw.upperMass (L : ExchangeableGraphLaw) {k : ℕ} (F : SimpleGraph (Fin k)) : ℝ

The upper mass of a finite graph under an exchangeable law: the total mass of the supergraphs of F under the k-vertex marginal.

Equations

• L.upperMass F = Graphon.upperSum (fun (G : SimpleGraph (Fin k)) => ((L.law k) G).toReal) F

def Graphon.ExchangeableGraphLaw.IsDissociated (L : ExchangeableGraphLaw) : Prop

Dissociated exchangeable laws: upper events on disjoint vertex blocks are independent (Diaconis–Janson Theorem 5.5 criterion; cross-block edges remain unrestricted).

Equations

• L.IsDissociated = ∀ {k l : ℕ} (F : SimpleGraph (Fin k)) (H : SimpleGraph (Fin l)), L.upperMass (SimpleGraph.map (⇑finSumFinEquiv.toEmbedding) (F ⊕g H)) = L.upperMass F * L.upperMass H

theorem GraphonSpace.upperMass_mixtureExchangeableLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) {k : ℕ} (F : SimpleGraph (Fin k)) : (mixtureExchangeableLaw P).upperMass F = ∫ (x : GraphonSpace α μ), homDensityCoord F x ∂↑P

The upper mass of a graphon mixture is the integral of the corresponding hom-density coordinate against the mixing measure.

theorem GraphonSpace.isDissociated_mixtureExchangeableLaw_iff {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) : (mixtureExchangeableLaw P).IsDissociated ↔ ∃ (x : GraphonSpace α μ), P = MeasureTheory.diracProba x

Diaconis–Janson extremality (their Theorem 5.5): a graphon mixture is dissociated iff the mixing measure is a Dirac. Dissociation at two copies of F makes every hom-density coordinate a.s. constant; point separation of the coordinates then collapses the mixing measure to a point.

theorem GraphonSpace.sampleExchangeableLaw_eq_mixture_diracProba {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) : W.sampleExchangeableLaw = mixtureExchangeableLaw (MeasureTheory.diracProba (mk W))

The sample law of a fixed graphon is the Dirac mixture at its graphon class.

theorem GraphonSpace.isDissociated_sampleExchangeableLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) : W.sampleExchangeableLaw.IsDissociated

The exchangeable law of a fixed graphon is dissociated: it is the Dirac mixture at its graphon class.

theorem GraphonSpace.isDissociated_iff_exists_sampleExchangeableLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (L : Graphon.ExchangeableGraphLaw) : L.IsDissociated ↔ ∃ (W : Graphon α μ), W.sampleExchangeableLaw = L

Extremality for arbitrary exchangeable laws: a law is dissociated iff it is the sample law of a fixed graphon (the Dirac characterization, transported along the representation and surjective_mk).