The barycenter interpretation of the infinite mixture (issue #54)

The represented infinite law of a mixing measure really is the mixture of the fiber laws, as a Measure.bind construction:

• GraphonSpace.measurable_infiniteSampleLaw_toMeasure — the canonical infinite law is a measurable family of measures (Dynkin induction over the cylinder π-system, using the measurable finite sample-law masses);
• GraphonSpace.mixtureInfiniteLaw — the barycenter (P : Measure _).bind (fun x => infiniteSampleLaw x), bundled as a probability measure and characterized on measurable sets by mixtureInfiniteLaw_apply : ... = ∫⁻ x, infiniteSampleLaw x A ∂P;
• GraphonSpace.mixtureInfiniteLaw_eq — the barycenter identification: mixtureInfiniteLaw P = (infiniteMixtureLawEquiv P).law (every cylinder marginal is the mixture marginal mixturePMF P k, and finite-restriction extensionality concludes).

theorem GraphonSpace.measurable_infiniteSampleLaw_toMeasure {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] : Measurable fun (x : GraphonSpace α μ) => ↑x.infiniteSampleLaw

The canonical infinite law is a measurable family of measures: measurability of each evaluation, by Dynkin induction over the generating cylinder π-system, where the masses are the (measurable) finite sample-law masses.

noncomputable def GraphonSpace.mixtureInfiniteLaw {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) : MeasureTheory.ProbabilityMeasure InfiniteGraph

The barycenter of the canonical infinite laws over a mixing measure, as a probability measure.

Equations

• GraphonSpace.mixtureInfiniteLaw P = ⟨(↑P).bind fun (x : GraphonSpace α μ) => ↑x.infiniteSampleLaw, ⋯⟩

@[simp]

theorem GraphonSpace.mixtureInfiniteLaw_coe {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) : ↑(mixtureInfiniteLaw P) = (↑P).bind fun (x : GraphonSpace α μ) => ↑x.infiniteSampleLaw

theorem GraphonSpace.mixtureInfiniteLaw_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) {A : Set InfiniteGraph} (hA : MeasurableSet A) : ↑(mixtureInfiniteLaw P) A = ∫⁻ (x : GraphonSpace α μ), ↑x.infiniteSampleLaw A ∂↑P

The barycenter, characterized on measurable sets.

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

The barycenter identification (issue #54): the represented infinite law of a mixing measure is the mixture of the canonical fiber laws — every cylinder marginal is the mixture marginal, and finite-restriction extensionality concludes.