Step graphons

A step graphon is specified by a measurable finite partition of its probability carrier and a symmetric matrix of values in [0, 1], indexed by the parts. The resulting graphon is constant on every rectangle cut out by the partition.

The definition uses Mathlib's Finpartition directly. Its value is written as a finite sum of indicators of the measurable rectangles. Pairwise disjointness and coverage of the partition then show that exactly one summand is nonzero at every point. This presentation makes joint measurability immediate and does not choose a distinguished index for each point of the carrier.

Main definitions

• TauCeti.DenseGraphLimits.stepGraphon is the graphon associated to a measurable finite partition and a symmetric matrix of block values.

Main results

• TauCeti.DenseGraphLimits.stepGraphon_apply evaluates the graphon on a specified block;
• TauCeti.DenseGraphLimits.stepGraphon_inj says that, for a fixed partition, two step graphons are equal exactly when their block values agree;
• TauCeti.DenseGraphLimits.stepGraphon_const identifies a constant block matrix with the constant graphon.

References

• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 2 — the block-constant stepGraphon, which is the carrier for stepGraphonAvg and the Frieze--Kannan weak regularity output.
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §9.2.

noncomputable def TauCeti.DenseGraphLimits.stepGraphon {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (val : ↥P.parts → ↥P.parts → ↑(Set.Icc 0 1)) (hsymm : ∀ (p q : ↥P.parts), val p q = val q p) : Graphon Ω μ

The step graphon associated to a measurable finite partition and a symmetric matrix of block values in [0, 1].

The matrix is indexed by the subtype of parts of P; consequently it has no entries unrelated to an actual block of the partition. Use stepGraphon_apply as the evaluation rule.

Equations

• TauCeti.DenseGraphLimits.stepGraphon P hP val hsymm = { toFun := TauCeti.DenseGraphLimits.stepValue✝ P val, symm' := ⋯, meas' := ⋯, bdd' := ⋯, mem01' := ⋯ }

theorem TauCeti.DenseGraphLimits.stepGraphon_apply {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (val : ↥P.parts → ↥P.parts → ↑(Set.Icc 0 1)) (hsymm : ∀ (p q : ↥P.parts), val p q = val q p) {p q : ↥P.parts} {x y : Ω} (hx : x ∈ ↑p) (hy : y ∈ ↑q) : (stepGraphon P hP val hsymm) x y = ↑(val p q)

A step graphon takes its prescribed value on each rectangle of the partition.

theorem TauCeti.DenseGraphLimits.stronglyMeasurable_comap_stepGraphon {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (val : ↥P.parts → ↥P.parts → ↑(Set.Icc 0 1)) (hsymm : ∀ (p q : ↥P.parts), val p q = val q p) : MeasureTheory.StronglyMeasurable fun (z : Ω × Ω) => (stepGraphon P hP val hsymm) z.1 z.2

A step graphon is strongly measurable with respect to the σ-algebra recording the partition part of each coordinate, since it is a function of the pair of part indices.

@[simp]

theorem TauCeti.DenseGraphLimits.stepGraphon_inj {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (val val' : ↥P.parts → ↥P.parts → ↑(Set.Icc 0 1)) (hsymm : ∀ (p q : ↥P.parts), val p q = val q p) (hsymm' : ∀ (p q : ↥P.parts), val' p q = val' q p) : stepGraphon P hP val hsymm = stepGraphon P hP val' hsymm' ↔ val = val'

Two step graphons on a fixed partition are equal exactly when their block matrices agree.

@[simp]

theorem TauCeti.DenseGraphLimits.stepGraphon_const {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : Finpartition Set.univ) (hP : ∀ p ∈ P.parts, MeasurableSet p) (c : ↑(Set.Icc 0 1)) : stepGraphon P hP (fun (x x_1 : ↥P.parts) => c) ⋯ = Graphon.const μ c

A step graphon whose block matrix is constant is the corresponding constant graphon.