The infinite Diaconis–Janson / Aldous–Hoover correspondence (issue #53)

Composing the mixture representation with the infinite-law equivalence:

• GraphonSpace.infiniteMixtureLawEquiv — every exchangeable probability law on infinite graphs is represented by a unique probability measure on graphon space: ProbabilityMeasure (GraphonSpace α μ) ≃ InfiniteExchangeableGraphLaw, the graphon-space form of Aldous–Hoover at the level of distributions;
• simp lemmas for both directions, and the finite marginals of the represented infinite law (infiniteMixtureLawEquiv_law_map_restrictFin: the level-k restriction is the mixture marginal mixturePMF P k).

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

The infinite Diaconis–Janson / Aldous–Hoover correspondence: probability measures on the graphon space are exactly the exchangeable probability laws on infinite graphs — the composition of the mixture representation with the infinite-law equivalence.

Equations

• GraphonSpace.infiniteMixtureLawEquiv = GraphonSpace.mixtureExchangeableLawEquiv.trans Graphon.exchangeableGraphLawEquivInfinite

@[simp]

theorem GraphonSpace.infiniteMixtureLawEquiv_apply_law {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) : (infiniteMixtureLawEquiv P).law = (mixtureExchangeableLaw P).infiniteLaw

@[simp]

theorem GraphonSpace.mixtureExchangeableLaw_infiniteMixtureLawEquiv_symm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (M : Graphon.InfiniteExchangeableGraphLaw) : mixtureExchangeableLaw (infiniteMixtureLawEquiv.symm M) = M.toExchangeableGraphLaw

theorem GraphonSpace.infiniteMixtureLawEquiv_law_map_restrictFin {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) (k : ℕ) : MeasureTheory.Measure.map (InfiniteGraph.restrictFin k) ↑(infiniteMixtureLawEquiv P).law = (mixturePMF P k).toMeasure

Finite marginals of the represented infinite law: the level-k restriction of the infinite law of a mixing measure is the mixture marginal mixturePMF P k.