Cut Norm for Graphons

This file defines the cut norm (also called rectangle norm) for graphons and signed kernels, and proves basic properties.

Main definitions

• SymmKernel.rectIntegral - Integral over a rectangle S × T
• SymmKernel.cutNorm - The cut norm ‖W‖□ = sup{S,T} |∫_{S×T} W|

Main results

• SymmKernel.cutNorm_nonneg - Cut norm is non-negative
• SymmKernel.cutNorm_le_one - Cut norm of a graphon is at most 1

Implementation notes

The cut norm is crucial for graphon convergence theory. It measures how well a graphon can be approximated by step functions.

For a graphon W ∈ [0,1], we have 0 ≤ ‖W‖_□ ≤ 1.

The cut distance δ_□(U, W) = inf_{φ,ψ} ‖U^φ - W^ψ‖_□ is defined in CutDistance.lean (two-sided reparametrization for trivial symmetry).

References

• [L. Lovász, Large Networks and Graph Limits][lovasz2012], Section 8.2.1

Rectangle integrals

noncomputable def SymmKernel.rectIntegral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : SymmKernel α μ) (S T : Set α) : ℝ

The integral of a symmetric kernel over a measurable rectangle S × T.

This is the key building block for the cut norm: rectIntegral W S T = ∫∫_{S×T} W(x,y) dμ(x) dμ(y)

Equations

• W.rectIntegral S T = ∫ (p : α × α) in S ×ˢ T, ↑W.toAEEqFun p ∂μ.prod μ

theorem SymmKernel.rectIntegral_symm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {S T : Set α} (W : SymmKernel α μ) (hS : MeasurableSet S) (hT : MeasurableSet T) : W.rectIntegral S T = W.rectIntegral T S

Rectangle integral is symmetric by symmetry of W.

theorem SymmKernel.rectIntegral_empty_left {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : SymmKernel α μ) (T : Set α) : W.rectIntegral ∅ T = 0

Rectangle integral over empty set is zero.

theorem SymmKernel.rectIntegral_empty_right {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : SymmKernel α μ) (S : Set α) : W.rectIntegral S ∅ = 0

Rectangle integral over empty set is zero.

theorem SymmKernel.rectIntegral_univ {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : SymmKernel α μ) : W.rectIntegral Set.univ Set.univ = ∫ (p : α × α), ↑W.toAEEqFun p ∂μ.prod μ

Rectangle integral over the full space.

Cut norm

noncomputable def SymmKernel.cutNorm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : SymmKernel α μ) : ℝ

The cut norm of a symmetric kernel.

‖W‖_□ = sup_{S,T measurable} |∫_{S×T} W dμ×μ|

This measures the "discrepancy" of the kernel - how far it deviates from being constant on rectangles.

Equations

• W.cutNorm = ⨆ (S : Set α), ⨆ (_ : MeasurableSet S), ⨆ (T : Set α), ⨆ (_ : MeasurableSet T), |W.rectIntegral S T|

theorem SymmKernel.cutNorm_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : SymmKernel α μ) : 0 ≤ W.cutNorm

Cut norm is non-negative (follows from abs being non-negative).

theorem SymmKernel.graphon_abs_le_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : ∀ᵐ (p : α × α) ∂μ.prod μ, |↑W.toAEEqFun p| ≤ 1

Graphon values are bounded by 1 in absolute value.

theorem SymmKernel.graphon_integrable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : MeasureTheory.Integrable (↑W.toAEEqFun) (μ.prod μ)

Graphons are integrable on probability spaces.

theorem SymmKernel.abs_rectIntegral_le_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (S T : Set α) : |W.rectIntegral S T| ≤ 1

Rectangle integral of a graphon is bounded by 1.

theorem SymmKernel.abs_rectIntegral_le_cutNorm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) {S T : Set α} (hS : MeasurableSet S) (hT : MeasurableSet T) : |W.rectIntegral S T| ≤ W.cutNorm

Cut norm bounds individual rectangle integrals.

For graphons this follows from boundedness of the function (values in [0,1]). The proof requires showing the supremum is over a bounded-above set, which follows from the graphon value bounds.

theorem SymmKernel.cutNorm_le_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) : W.cutNorm ≤ 1

Cut norm for graphons is bounded by 1.

Since graphon values are in [0,1], the rectangle integral over any S × T is at most μ(S) * μ(T) ≤ 1.

noncomputable def Graphon.cutNorm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) [MeasureTheory.IsProbabilityMeasure μ] : ℝ

Cut norm of a graphon, via its symmetric kernel.

Equations

• W.cutNorm = W.cutNorm

theorem Graphon.cutNorm_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) [MeasureTheory.IsProbabilityMeasure μ] : 0 ≤ W.cutNorm

Graphon cut norm is non-negative.

theorem Graphon.cutNorm_le_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) [MeasureTheory.IsProbabilityMeasure μ] : W.cutNorm ≤ 1

Graphon cut norm is at most 1.

Weighted integrals and cut norm

theorem Graphon.abs_weighted_integral_le_cutNorm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (K : Graphon α μ) (f g : α → ℝ) (hf_meas : Measurable f) (hg_meas : Measurable g) (hf_bound : ∀ (x : α), f x ∈ Set.Icc 0 1) (hg_bound : ∀ (x : α), g x ∈ Set.Icc 0 1) : |∫ (x : α), ∫ (y : α), f x * g y * ↑K.toAEEqFun (x, y) ∂μ ∂μ| ≤ K.cutNorm

The key lemma for the counting lemma: weighted integrals are bounded by cut norm.

For f, g : α → [0, 1] measurable and K a graphon: |∫∫ f(x) g(y) K(x,y) dμ(x) dμ(y)| ≤ ‖K‖_□

The proof approximates f and g by simple functions (linear combinations of indicator functions of measurable sets). Since ‖K‖_□ bounds each rectangle integral, it bounds the weighted sum by triangle inequality.

Note: This is Lemma 10.21 in Lovász [2012].

theorem Graphon.weighted_integral_indicator {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (K : Graphon α μ) (S T : Set α) (hS : MeasurableSet S) (hT : MeasurableSet T) : ∫ (x : α), ∫ (y : α), S.indicator (fun (x : α) => 1) x * T.indicator (fun (x : α) => 1) y * ↑K.toAEEqFun (x, y) ∂μ ∂μ = K.rectIntegral S T

Special case: indicator functions give rectangle integrals.

This connects the weighted integral form to the rectangle integral definition.

theorem Graphon.abs_weighted_integral_indicator_le_cutNorm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (K : Graphon α μ) (S T : Set α) (hS : MeasurableSet S) (hT : MeasurableSet T) : |∫ (x : α), ∫ (y : α), S.indicator (fun (x : α) => 1) x * T.indicator (fun (x : α) => 1) y * ↑K.toAEEqFun (x, y) ∂μ ∂μ| ≤ K.cutNorm

Corollary: indicator weighted integrals are bounded by cut norm.

For measurable sets S, T: |∫∫ 1_S(x) 1_T(y) K(x,y) dμ(x) dμ(y)| ≤ ‖K‖_□

This is the base case for the general weighted integral bound. It follows directly from weighted_integral_indicator + abs_rectIntegral_le_cutNorm.