Approximation of Graphons by Step Functions

This file develops the theory of approximating graphons by step functions, which is central to the regularity lemma and compactness of graphon space.

Main definitions

• Graphon.rectAverage - Average value of a graphon over a rectangle
• Graphon.Refines - Partition refinement relation

Main results

• Graphon.rectAverage_mem_Icc - Rectangle averages are in [0, 1]
• Graphon.rectAverage_symm - Rectangle averages are symmetric

Implementation notes

Given a measurable partition P of α, the stepified graphon takes the average value on each rectangle S × T for S, T ∈ P: (stepify P W)(x, y) = (1/(μ(S)μ(T))) ∫_{S×T} W dμ×μ for x ∈ S, y ∈ T

The stepification stepify P W constructs the step-function approximation as an AEEqFun, with stepify_ae providing the pointwise characterization.

References

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

Rectangle averages

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

The average value of a graphon over a rectangle S × T.

This is the building block for stepification: rectAverage W S T = (1/(μ(S)μ(T))) ∫_{S×T} W dμ×μ

Equations

• W.rectAverage S T = if hS : μ S = 0 then 0 else if hT : μ T = 0 then 0 else (μ S).toReal⁻¹ * (μ T).toReal⁻¹ * ∫ (p : α × α) in S ×ˢ T, ↑W.toAEEqFun p ∂μ.prod μ

theorem Graphon.rectAverage_mem_Icc {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (S T : Set α) (hS : MeasurableSet S) (hT : MeasurableSet T) : W.rectAverage S T ∈ Set.Icc 0 1

The rectangle average is in [0, 1] for graphons.

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

The rectangle average is symmetric.

theorem Graphon.rectAverage_zero {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (S T : Set α) : zero.rectAverage S T = 0

Rectangle average of zero graphon is zero.

theorem Graphon.rectAverage_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {S T : Set α} (hS : μ S ≠ 0) (hT : μ T ≠ 0) (hSm : MeasurableSet S) (hTm : MeasurableSet T) : one.rectAverage S T = 1

Rectangle average of one graphon is one (for positive measure sets).

Refinement

def Graphon.Refines {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (Q P : MeasurablePartition α μ) : Prop

A partition Q refines P if every part of Q is contained in some part of P.

Equations

• Graphon.Refines Q P = ∀ T ∈ Q.parts, ∃ S ∈ P.parts, T ⊆ S

theorem Graphon.Refines.refl {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) : Refines P P

Refinement is reflexive.

theorem Graphon.Refines.trans {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {P Q R : MeasurablePartition α μ} (hPQ : Refines Q P) (hQR : Refines R Q) : Refines R P

Refinement is transitive.

Partition splitting

noncomputable def Graphon.MeasurablePartition.splitPart {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (P : MeasurablePartition α μ) (S : Set α) (hS : S ∈ P.parts) (S₁ : Set α) (hS₁_meas : MeasurableSet S₁) (hS₁_sub : S₁ ⊆ S) (_hS₁_pos : μ S₁ ≠ 0) (_hS₂_pos : μ (S \ S₁) ≠ 0) : MeasurablePartition α μ

Split one part of a partition into two pieces.

Given partition P and a part S ∈ P.parts, and a measurable subset S₁ ⊆ S, construct the refinement Q that replaces S with S₁ and S \ S₁.

Preconditions:

• S ∈ P.parts
• S₁ ⊆ S is measurable
• Both S₁ and S \ S₁ have positive measure (to be non-trivial)

Implementation note: Uses classical decidability for Finset operations on Set α.

Equations

• Graphon.MeasurablePartition.splitPart P S hS S₁ hS₁_meas hS₁_sub _hS₁_pos _hS₂_pos = { parts := P.parts.erase S ∪ {S₁, S \ S₁}, measurable_parts := ⋯, pairwiseDisjoint := ⋯, ae_covers := ⋯ }

theorem Graphon.MeasurablePartition.splitPart_refines {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) (S : Set α) (hS : S ∈ P.parts) (S₁ : Set α) (hS₁_meas : MeasurableSet S₁) (hS₁_sub : S₁ ⊆ S) (hS₁_pos : μ S₁ ≠ 0) (hS₂_pos : μ (S \ S₁) ≠ 0) : Refines (splitPart P S hS S₁ hS₁_meas hS₁_sub hS₁_pos hS₂_pos) P

Splitting a part produces a refinement.

theorem Graphon.MeasurablePartition.splitPart_card {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) (S : Set α) (hS : S ∈ P.parts) (S₁ : Set α) (hS₁_meas : MeasurableSet S₁) (hS₁_sub : S₁ ⊆ S) (hS₁_pos : μ S₁ ≠ 0) (hS₂_pos : μ (S \ S₁) ≠ 0) : (splitPart P S hS S₁ hS₁_meas hS₁_sub hS₁_pos hS₂_pos).parts.card ≤ P.parts.card + 1

Splitting adds at most one part.

noncomputable def Graphon.MeasurablePartition.splitAllParts {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (P : MeasurablePartition α μ) (A : Set α) (hA : MeasurableSet A) : MeasurablePartition α μ

Split every part of a partition by a measurable set A.

For each S ∈ P.parts, we include S ∩ A and S \ A in the new partition (keeping all pieces, even null ones — this simplifies ae_covers).

This is the global splitting operation needed for the Frieze-Kannan regularity proof when both within-variances are large.

Equations

• Graphon.MeasurablePartition.splitAllParts P A hA = { parts := P.parts.biUnion fun (S : Set α) => {S ∩ A, S \ A}, measurable_parts := ⋯, pairwiseDisjoint := ⋯, ae_covers := ⋯ }

theorem Graphon.MeasurablePartition.splitAllParts_refines {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (P : MeasurablePartition α μ) (A : Set α) (hA : MeasurableSet A) : Refines (splitAllParts P A hA) P

splitAllParts produces a refinement.

theorem Graphon.MeasurablePartition.splitAllParts_card {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (P : MeasurablePartition α μ) (A : Set α) (hA : MeasurableSet A) : (splitAllParts P A hA).parts.card ≤ 2 * P.parts.card

splitAllParts has at most 2 * P.parts.card parts.

Stepification

noncomputable def Graphon.stepifyFun {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (P : MeasurablePartition α μ) (W : Graphon α μ) : α × α → ℝ

The stepification function: piecewise constant on partition rectangles.

For a partition P and graphon W, stepifyFun P W (x,y) = rectAverage W S T when (x,y) ∈ S × T for S, T ∈ P.parts.

Equations

• Graphon.stepifyFun P W p = ∑ S ∈ P.parts, ∑ T ∈ P.parts, (S ×ˢ T).indicator (fun (x : α × α) => W.rectAverage S T) p

theorem Graphon.stepifyFun_measurable {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (P : MeasurablePartition α μ) (W : Graphon α μ) : Measurable (stepifyFun P W)

stepifyFun is measurable.

theorem Graphon.stepifyFun_symm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) (W : Graphon α μ) (p : α × α) : stepifyFun P W p.swap = stepifyFun P W p

stepifyFun is symmetric: stepifyFun P W (y,x) = stepifyFun P W (x,y).

theorem Graphon.stepifyFun_eq_rectAverage {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) (W : Graphon α μ) {p : α × α} {S : Set α} (hS : S ∈ P.parts) {T : Set α} (hT : T ∈ P.parts) (hp : p ∈ S ×ˢ T) : stepifyFun P W p = W.rectAverage S T

At every point in S × T, the stepification equals rectAverage W S T.

For any (x,y), if x ∈ S and y ∈ T for unique parts S, T ∈ P.parts, then stepifyFun P W (x,y) = rectAverage W S T.

theorem Graphon.stepifyFun_mem_Icc_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) (W : Graphon α μ) : ∀ᵐ (p : α × α) ∂μ.prod μ, stepifyFun P W p ∈ Set.Icc 0 1

stepifyFun takes values in [0,1] a.e.

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

The stepification of a graphon with respect to a partition.

This is the step graphon that equals rectAverage W S T on each rectangle S × T for parts S, T ∈ P.parts.

Equations

• Graphon.stepify P W = { toAEEqFun := MeasureTheory.AEEqFun.mk (Graphon.stepifyFun P W) ⋯, symm' := ⋯, ae_mem_Icc := ⋯ }

theorem Graphon.stepify_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) (W : Graphon α μ) : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑(stepify P W).toAEEqFun p = stepifyFun P W p

The stepification agrees with the stepification function a.e.