Extremality for infinite exchangeable laws (issue #55)

Transporting the Diaconis–Janson extremality criterion through the infinite representation:

• GraphonSpace.infiniteMixtureLawEquiv_dirac_law — the Dirac bridge: the represented law of a Dirac mixing measure is the canonical infinite law of its point;
• GraphonSpace.infiniteSampleExchangeableLaw — the canonical infinite law, bundled with its exchangeability;
• Graphon.InfiniteExchangeableGraphLaw.IsDissociated — dissociation of an infinite law (via its finite marginals);
• GraphonSpace.isDissociated_iff_exists_infiniteSampleExchangeableLaw — an infinite exchangeable law is dissociated iff it is the canonical law of a single graphon class;
• GraphonSpace.isDissociated_iff_representing_dirac — equivalently, iff its representing measure is a Dirac.

@[simp]

theorem GraphonSpace.infiniteMixtureLawEquiv_dirac_law {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (x : GraphonSpace α μ) : (infiniteMixtureLawEquiv (MeasureTheory.diracProba x)).law = x.infiniteSampleLaw

The Dirac bridge: the represented infinite law of a Dirac mixing measure is the canonical infinite law of its point.

noncomputable def GraphonSpace.infiniteSampleExchangeableLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (x : GraphonSpace α μ) : Graphon.InfiniteExchangeableGraphLaw

The canonical infinite law of a graphon class, bundled with its exchangeability.

Equations

• x.infiniteSampleExchangeableLaw = GraphonSpace.infiniteMixtureLawEquiv (MeasureTheory.diracProba x)

@[simp]

theorem GraphonSpace.infiniteSampleExchangeableLaw_law {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (x : GraphonSpace α μ) : x.infiniteSampleExchangeableLaw.law = x.infiniteSampleLaw

def Graphon.InfiniteExchangeableGraphLaw.IsDissociated (M : InfiniteExchangeableGraphLaw) : Prop

Dissociation of an infinite exchangeable law: dissociation of its finite marginals (upper events on disjoint vertex blocks are independent).

Equations

• M.IsDissociated = M.toExchangeableGraphLaw.IsDissociated

theorem GraphonSpace.isDissociated_iff_representing_dirac {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (M : Graphon.InfiniteExchangeableGraphLaw) : M.IsDissociated ↔ ∃ (x : GraphonSpace α μ), infiniteMixtureLawEquiv.symm M = MeasureTheory.diracProba x

Extremality at the infinite level, Dirac form: an infinite exchangeable law is dissociated iff its representing measure is a Dirac.

theorem GraphonSpace.isDissociated_iff_exists_infiniteSampleExchangeableLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (M : Graphon.InfiniteExchangeableGraphLaw) : M.IsDissociated ↔ ∃ (x : GraphonSpace α μ), M = x.infiniteSampleExchangeableLaw

Extremality at the infinite level: an infinite exchangeable law is dissociated iff it is the canonical law of a single graphon class.

theorem GraphonSpace.isDissociated_infiniteSampleExchangeableLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (x : GraphonSpace α μ) : x.infiniteSampleExchangeableLaw.IsDissociated

The canonical infinite law of a graphon class is dissociated.