Uniqueness of the graphon mixture (issue #33, bricks 3–4) #

The mixing measure of a graphon mixture is determined by its finite marginals:

GraphonSpace.homDensityCoordBCF / GraphonSpace.homDensityGenerators — the hom-density coordinates as bounded continuous functions; the generator set contains 1 (the empty graph on Fin 0) and is closed under multiplication (homDensity_sum_finAdd);
GraphonSpace.homDensityStarSubalgebra — the real linear span of the generators, packaged directly as a StarSubalgebra (multiplication closure by nested Submodule.span_induction; star is trivial over ℝ) — deliberately NOT Algebra.adjoin, whose induction principle does not see the span structure;
GraphonSpace.integral_homDensityCoordSpan_eq — equal mixture marginals give equal integrals on the span: each generator is a finite upper sum of sampleMassCoords, whose integrals are the marginal masses (mixturePMF_apply_toReal);
the mapped subalgebra separates points (homDensityCoord_eq_all_iff), so Mathlib's ext_of_forall_mem_subalgebra_integral_eq_of_polish yields GraphonSpace.mixtureExchangeableLaw_injective — the uniqueness half of the Diaconis–Janson correspondence.

def GraphonSpace.homDensityGenerators {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] :

Set (BoundedContinuousFunction (GraphonSpace α μ) ℝ)

The generator set of the coordinate algebra: all hom-density coordinates of finite graphs on Fin k, over all k.

Equations

GraphonSpace.homDensityGenerators = {f : BoundedContinuousFunction (GraphonSpace α μ) ℝ | ∃ (k : ℕ) (F : SimpleGraph (Fin k)), f = GraphonSpace.homDensityCoordBCF F}

Instances For

source

theorem GraphonSpace.one_mem_homDensityGenerators {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] :

1 ∈ homDensityGenerators

1 is a generator: the hom density of the empty graph on Fin 0.

source

theorem GraphonSpace.mul_mem_homDensityGenerators {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {f g : BoundedContinuousFunction (GraphonSpace α μ) ℝ} (hf : f ∈ homDensityGenerators) (hg : g ∈ homDensityGenerators) :

f * g ∈ homDensityGenerators

The generators are closed under multiplication (homDensity_sum_finAdd).

source

noncomputable def GraphonSpace.homDensityCoordSpan {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] :

Submodule ℝ (BoundedContinuousFunction (GraphonSpace α μ) ℝ)

The real linear span of the hom-density coordinates.

Equations

GraphonSpace.homDensityCoordSpan = Submodule.span ℝ GraphonSpace.homDensityGenerators

Instances For

source

theorem GraphonSpace.mul_mem_homDensityCoordSpan {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {f g : BoundedContinuousFunction (GraphonSpace α μ) ℝ} (hf : f ∈ homDensityCoordSpan) (hg : g ∈ homDensityCoordSpan) :

f * g ∈ homDensityCoordSpan

The span is closed under multiplication (nested span_induction).

source

noncomputable def GraphonSpace.homDensityStarSubalgebra {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] :

StarSubalgebra ℝ (BoundedContinuousFunction (GraphonSpace α μ) ℝ)

The hom-density coordinate algebra: the span of the coordinates, packaged as a StarSubalgebra of the bounded continuous functions on the graphon space.

Equations

GraphonSpace.homDensityStarSubalgebra = { carrier := ↑GraphonSpace.homDensityCoordSpan, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, algebraMap_mem' := ⋯, star_mem' := ⋯ }