Graphons

A graphon on a probability space (Ω, μ) is a [0, 1]-valued symmetric kernel: an everywhere-defined W : Ω → Ω → ℝ that is symmetric, jointly measurable, and takes values in [0, 1]. It is the limit object of the dense graph limit theory.

A graphon is a kernel with a range constraint, not a new carrier. Graphon extends SymmKernel, so symmetry and measurability are inherited rather than restated, and every kernel-level construction applies to a graphon through Graphon.toSymmKernel. That projection is what lets the cut norm — defined on kernels, so that a difference U - W of graphons is in its domain — be applied to graphons without a second definition.

Graphons carry no algebra. They are deliberately not an AddCommGroup or a Module: the [0, 1] constraint is not preserved by addition, negation, or scaling, so U - W is a kernel and not a graphon. This is exactly why the roadmap puts the cut norm on SymmKernel and the range constraint here.

The measure is a genuine parameter here. Unlike SymmKernel, whose measure is a phantom argument, Graphon requires [IsProbabilityMeasure μ]: the analytic theory built on graphons — homomorphism densities, the cut metric, sampling — integrates against μ and needs total mass one.

Main definitions

• TauCeti.DenseGraphLimits.Graphon — the [0, 1]-valued symmetric kernel, with a FunLike coercion, extensionality by the underlying function, and the toSymmKernel projection.
• TauCeti.DenseGraphLimits.Graphon.const — the constant graphon with value p : I.
• TauCeti.DenseGraphLimits.Graphon.clampSymm — turn a measurable real-valued kernel into a graphon by averaging with its transpose and clamping to [0, 1].

Main results

• Graphon.symm, Graphon.measurable — symmetry and joint measurability, inherited from the kernel;
• Graphon.nonneg, Graphon.le_one — the pointwise range constraint, in eliminator form;
• Graphon.const_apply — the constant graphon evaluates to its parameter.
• Graphon.clampSymm_apply_of_symm_of_mem — symmetrizing and clamping leaves a symmetric value already in [0, 1] unchanged.

References

• Roadmap: TauCetiRoadmap/DenseGraphLimits/README.md, Layer 1 — the graphon carrier and the constant graphon. The signature follows TauCetiRoadmap/DenseGraphLimits/Suggested.lean. Homomorphism densities, the cut norm and cut distance, the GraphonSpace quotient and its a.e.-identification, and the step graphon of a finite graph are separate targets and are not built here.
• S. Janson, Graphons, cut norm and distance, couplings and rearrangements, NYJM Monographs 4 (2013).
• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §7.

structure TauCeti.DenseGraphLimits.Graphon (Ω : Type u_2) [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] extends TauCeti.DenseGraphLimits.SymmKernel Ω μ : Type u_2

A graphon: a [0, 1]-valued symmetric kernel on a probability space.

Extends SymmKernel, so symmetry, measurability and boundedness come from there; the only new field is the pointwise range constraint.

• toFun : Ω → Ω → ℝ
• symm' (x y : Ω) : self.toFun x y = self.toFun y x
• meas' : Measurable (Function.uncurry self.toFun)
• bdd' : ∃ (C : ℝ), ∀ (x y : Ω), |self.toFun x y| ≤ C
• mem01' (x y : Ω) : self.toFun x y ∈ Set.Icc 0 1

  A graphon takes values in [0, 1]. Stated via Graphon.nonneg and Graphon.le_one.

@[instance_reducible]

instance TauCeti.DenseGraphLimits.Graphon.instFunLike {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] : FunLike (Graphon Ω μ) Ω (Ω → ℝ)

A graphon acts as its underlying function Ω → Ω → ℝ.

Equations

• TauCeti.DenseGraphLimits.Graphon.instFunLike = { coe := fun (W : TauCeti.DenseGraphLimits.Graphon Ω μ) => ⇑W.toSymmKernel, coe_injective := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.Graphon.coe_mk {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (K : SymmKernel Ω μ) (hmem : ∀ (x y : Ω), K.toFun x y ∈ Set.Icc 0 1) : ⇑{ toSymmKernel := K, mem01' := hmem } = ⇑K

Constructing a graphon does not change the underlying function of its symmetric kernel.

@[simp]

theorem TauCeti.DenseGraphLimits.Graphon.coe_toSymmKernel {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : ⇑W.toSymmKernel = ⇑W

Projecting a graphon to its kernel does not change the underlying function.

theorem TauCeti.DenseGraphLimits.Graphon.ext {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {W W' : Graphon Ω μ} (h : ∀ (x y : Ω), W x y = W' x y) : W = W'

Two graphons agreeing pointwise are equal: the range constraint is a proposition, so the underlying function determines the graphon.

theorem TauCeti.DenseGraphLimits.Graphon.ext_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {W W' : Graphon Ω μ} : W = W' ↔ ∀ (x y : Ω), W x y = W' x y

theorem TauCeti.DenseGraphLimits.Graphon.symm {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (x y : Ω) : W x y = W y x

A graphon is symmetric, inherited from the underlying kernel.

theorem TauCeti.DenseGraphLimits.Graphon.measurable {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) : Measurable (Function.uncurry ⇑W)

A graphon is jointly measurable, inherited from the underlying kernel.

theorem TauCeti.DenseGraphLimits.Graphon.mem_Icc {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (x y : Ω) : W x y ∈ Set.Icc 0 1

A graphon takes values in [0, 1].

theorem TauCeti.DenseGraphLimits.Graphon.nonneg {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (x y : Ω) : 0 ≤ W x y

A graphon is nonnegative.

theorem TauCeti.DenseGraphLimits.Graphon.le_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (x y : Ω) : W x y ≤ 1

A graphon is bounded above by 1.

noncomputable def TauCeti.DenseGraphLimits.Graphon.clampSymm {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (f : Ω → Ω → ℝ) (hf : Measurable (Function.uncurry f)) : Graphon Ω μ

Average a measurable real-valued kernel with its transpose and clamp the result to [0, 1].

This is the common strict-representative construction: averaging enforces pointwise symmetry, and clamping enforces the graphon range without changing values that were already symmetric and in [0, 1].

Equations

• TauCeti.DenseGraphLimits.Graphon.clampSymm μ f hf = { toFun := fun (x y : Ω) => max 0 (min 1 ((f x y + f y x) / 2)), symm' := ⋯, meas' := ⋯, bdd' := ⋯, mem01' := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.Graphon.clampSymm_apply {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (f : Ω → Ω → ℝ) (hf : Measurable (Function.uncurry f)) (x y : Ω) : (clampSymm μ f hf) x y = max 0 (min 1 ((f x y + f y x) / 2))

Evaluating clampSymm gives the averaged and clamped kernel.

theorem TauCeti.DenseGraphLimits.Graphon.clampSymm_apply_of_symm_of_mem {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (f : Ω → Ω → ℝ) (hf : Measurable (Function.uncurry f)) {x y : Ω} (hsymm : f x y = f y x) (hmem : f x y ∈ Set.Icc 0 1) : (clampSymm μ f hf) x y = f x y

Symmetrizing and clamping does not change a value that is symmetric and already in [0, 1].

def TauCeti.DenseGraphLimits.Graphon.const {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ↑unitInterval) : Graphon Ω μ

The constant graphon with value p.

The parameter is taken in unitInterval, the same convention Mathlib's SimpleGraph.binomialRandom uses for G(V, p), so that the later sampling compatibility statement needs no translation.

Equations

• TauCeti.DenseGraphLimits.Graphon.const μ p = { toFun := fun (x x_1 : Ω) => ↑p, symm' := ⋯, meas' := ⋯, bdd' := ⋯, mem01' := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.Graphon.const_apply {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (p : ↑unitInterval) (x y : Ω) : (const μ p) x y = ↑p

The constant graphon evaluates to its parameter at every pair of points.