Approximation by block-average step graphons

On a countably generated probability space, the block averages of a graphon along the canonical refining finite partitions converge to the graphon in L¹. The finite partitions generate the ambient σ-algebra, so this is Lévy's upward theorem after identifying each block average with the corresponding conditional expectation.

This gives a strict, finite-step approximation with convergence stated as vanishing eLpNorm at exponent one.

Main result

• TauCeti.DenseGraphLimits.countableStepGraphonAvg is the canonical sequence of block-average step graphons, characterized by TauCeti.DenseGraphLimits.countableStepGraphonAvg_def.
• TauCeti.DenseGraphLimits.tendsto_eLpNorm_countableStepGraphonAvg gives L¹ convergence of canonical block averages.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §9.2.

noncomputable def TauCeti.DenseGraphLimits.countableStepGraphonAvg {Ω : Type u_1} [m : MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (n : ℕ) : Graphon Ω μ

The block-average step graphon on the level-n canonical finite partition of a countably generated measurable space.

Equations

• TauCeti.DenseGraphLimits.countableStepGraphonAvg W n = TauCeti.DenseGraphLimits.stepGraphonAvg (Finpartition.countablePartition Ω n) ⋯ W

theorem TauCeti.DenseGraphLimits.countableStepGraphonAvg_def {Ω : Type u_1} [m : MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (n : ℕ) : countableStepGraphonAvg W n = stepGraphonAvg (Finpartition.countablePartition Ω n) ⋯ W

The canonical block-average step graphon is the block average on the canonical finite partition.

countableStepGraphonAvg is a definition whose body is not exposed outside this module, so this is the only way a downstream file can rewrite it into the bundled stepGraphonAvg API.

@[simp]

theorem TauCeti.DenseGraphLimits.countableStepGraphonAvg_apply {Ω : Type u_1} [m : MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (n : ℕ) (x y : Ω) : (countableStepGraphonAvg W n) x y = (stepGraphonAvg (Finpartition.countablePartition Ω n) ⋯ W) x y

The canonical block-average step graphon takes the same values as the block average on the canonical finite partition.

theorem TauCeti.DenseGraphLimits.tendsto_eLpNorm_countableStepGraphonAvg {Ω : Type u_1} [m : MeasurableSpace Ω] [MeasurableSpace.CountablyGenerated Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm ((fun (z : Ω × Ω) => (countableStepGraphonAvg W n) z.1 z.2) - fun (z : Ω × Ω) => W z.1 z.2) 1 (μ.prod μ)) Filter.atTop (nhds 0)

The block-average step graphons along the canonical refining finite partitions converge to the original graphon in L¹ on the product space.