Mixture-coordinate infrastructure (issue #33)

Shared layer between the uniqueness and existence halves of the Diaconis–Janson correspondence:

• GraphonSpace.homDensityCoordBCF — the hom-density coordinates as bounded continuous functions on the compact graphon space;
• GraphonSpace.integral_homDensityCoord — the integral of a hom-density coordinate against a mixing measure is the upper mass of F under the corresponding mixture marginal (the coordinate is a finite upper sum of sampleMassCoords, whose integrals are the marginal masses).

Graphon/MixtureUniqueness.lean builds the coordinate StarSubalgebra on top of these; Graphon/MixtureExistence.lean consumes them for the Prokhorov-limit marginal identification.

noncomputable def GraphonSpace.homDensityCoordBCF {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} (F : SimpleGraph (Fin k)) : BoundedContinuousFunction (GraphonSpace α μ) ℝ

The hom-density coordinates as bounded continuous functions on the compact graphon space.

Equations

• GraphonSpace.homDensityCoordBCF F = BoundedContinuousFunction.mkOfCompact { toFun := GraphonSpace.homDensityCoord F, continuous_toFun := ⋯ }

@[simp]

theorem GraphonSpace.homDensityCoordBCF_apply {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} (F : SimpleGraph (Fin k)) (x : GraphonSpace α μ) : (homDensityCoordBCF F) x = homDensityCoord F x

theorem GraphonSpace.integral_homDensityCoord {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (R : MeasureTheory.ProbabilityMeasure (GraphonSpace α μ)) {k : ℕ} (F : SimpleGraph (Fin k)) : ∫ (x : GraphonSpace α μ), homDensityCoord F x ∂↑R = ∑ G : SimpleGraph (Fin k), if F ≤ G then ((mixturePMF R k) G).toReal else 0

The integral of a hom-density coordinate against a mixing measure is the upper mass of F under the corresponding mixture marginal (the coordinate is a finite upper sum of sampleMassCoords, whose integrals are the marginal masses).