Homomorphism densities of a measurable family of graphons #
If a family of graphons W t depends jointly measurably on a parameter t, meaning that
(t, x, y) ↦ W t x y is measurable, then each homomorphism density t ↦ t(F, W t) is a
measurable parametric integral.
Main results #
TauCeti.DenseGraphLimits.measurable_homDensity— the homomorphism density of a jointly measurable family of graphons is measurable in the parameter.
theorem
TauCeti.DenseGraphLimits.measurable_homDensity
{Ω : Type u_1}
[MeasurableSpace Ω]
{μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsProbabilityMeasure μ]
{T : Type u_2}
[MeasurableSpace T]
{V : Type u_3}
[Fintype V]
(F : SimpleGraph V)
[DecidableRel F.Adj]
{W : T → Graphon Ω μ}
(hW : Measurable fun (p : T × Ω × Ω) => (W p.1) p.2.1 p.2.2)
:
Measurable fun (t : T) => homDensity F (W t)
Homomorphism densities of a measurable family of graphons. If a family of graphons depends jointly measurably on a parameter, then so does the homomorphism density of every finite graph in it.