Finite-factor approximation of a graphon

Step 5a of the step-approximation programme (#107 remains open): every graphon is, to within any prescribed cut-norm error, the pullback of a graphon on a finite factor.

FiniteFactorApproximation U ε bundles the data — a factor map Ω → Fin (n + 1), its law, the measure-preserving witness, and a kernel on the finite factor — together with the error bound cutNormDiff U (pullback kernel factor) < ε. Packaging the factor as Fin (n + 1) with a bundled ProbabilityMeasure keeps every instance available by construction and makes the finite coupling machinery directly applicable.

exists_finiteFactorApproximation: such an approximation exists for every 0 < ε, with no standard-Borel, surjectivity, or positive-cell hypothesis. The construction reads the Frieze–Kannan partition off Graphon.regularity, indexes its parts by an enumeration, and sends every point to the index of its part — with a final index absorbing the null set of points no part covers, so no covering or positivity assumption is needed. The kernel is the matrix of rectangle averages, which rectAverage defines (as zero) on null cells.

This is the individual approximation used once per graphon; there is no shared factor across carriers. The triangle assembly reuses the middle graphon's approximation in both pairwise couplings — that assembly is a later unit and is not addressed here.

noncomputable def Graphon.enumPart {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) (i : Fin P.parts.card) : Set Ω

The i-th part of a finite measurable partition, under a fixed enumeration of its parts.

Equations

• Graphon.enumPart P i = ↑(P.parts.equivFin.symm i)

theorem Graphon.enumPart_mem {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) (i : Fin P.parts.card) : enumPart P i ∈ P.parts

theorem Graphon.measurableSet_enumPart {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) (i : Fin P.parts.card) : MeasurableSet (enumPart P i)

theorem Graphon.enumPart_ne {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) {i j : Fin P.parts.card} (h : i ≠ j) : enumPart P i ≠ enumPart P j

Distinct indices enumerate distinct parts.

theorem Graphon.eq_enumPart_of_mem {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) {S : Set Ω} (hS : S ∈ P.parts) {x : Ω} {i : Fin P.parts.card} (hxS : x ∈ S) (hxi : x ∈ enumPart P i) : S = enumPart P i

Any part containing a point of enumPart P i is enumPart P i itself.

theorem Graphon.enumPart_unique {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) {x : Ω} {i j : Fin P.parts.card} (hi : x ∈ enumPart P i) (hj : x ∈ enumPart P j) : i = j

A point lies in at most one enumerated part.

noncomputable def Graphon.partIndex {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) (x : Ω) : Fin (P.parts.card + 1)

The factor map: a point goes to the index of the part containing it. The final index absorbs the null set of points that no part covers, so no covering hypothesis is needed.

Equations

• Graphon.partIndex P x = if h : ∃ (i : Fin P.parts.card), x ∈ Graphon.enumPart P i then h.choose.castSucc else Fin.last P.parts.card

theorem Graphon.partIndex_of_mem {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) {x : Ω} {i : Fin P.parts.card} (hx : x ∈ enumPart P i) : partIndex P x = i.castSucc

theorem Graphon.partIndex_preimage_castSucc {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) (i : Fin P.parts.card) : partIndex P ⁻¹' {i.castSucc} = enumPart P i

theorem Graphon.partIndex_preimage_last {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) : partIndex P ⁻¹' {Fin.last P.parts.card} = (⋃ (i : Fin P.parts.card), enumPart P i)ᶜ

theorem Graphon.measurable_partIndex {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) : Measurable (partIndex P)

noncomputable def Graphon.indexPart {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) : Fin (P.parts.card + 1) → Set Ω

The part carried by a factor value; the final index carries the empty set.

Equations

• Graphon.indexPart P i = Fin.lastCases ∅ (Graphon.enumPart P) i

@[simp]

theorem Graphon.indexPart_castSucc {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) (i : Fin P.parts.card) : indexPart P i.castSucc = enumPart P i

@[simp]

theorem Graphon.indexPart_last {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) : indexPart P (Fin.last P.parts.card) = ∅

theorem Graphon.measurableSet_indexPart {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) (a : Fin (P.parts.card + 1)) : MeasurableSet (indexPart P a)

structure Graphon.FiniteFactorApproximation {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U : Graphon Ω μ) (ε : ℝ) : Type u_1

A finite-factor approximation of U at scale ε: a factor map to a finite space, its law, and a kernel on that finite space whose pullback is within ε of U in cut norm.

• n : ℕ

  The finite factor has n + 1 points.

• law : MeasureTheory.ProbabilityMeasure (Fin (self.n + 1))

  The law of the factor map on the finite factor.

• factor : Ω → Fin (self.n + 1)

  The factor map.

• factor_mp : MeasureTheory.MeasurePreserving self.factor μ ↑self.law

  The factor map pushes the carrier measure to the factor law.

• kernel : Graphon (Fin (self.n + 1)) ↑self.law

  The approximating kernel, a graphon on the finite factor.

• error_lt : U.cutNormDiff (self.kernel.pullback self.factor ⋯) < ε

  The pullback of the kernel is within ε of U in cut norm.

noncomputable def Graphon.partLaw {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition Ω μ) : MeasureTheory.ProbabilityMeasure (Fin (P.parts.card + 1))

The law of the factor map: the pushforward of the carrier measure, bundled.

Equations

• Graphon.partLaw P = ⟨MeasureTheory.Measure.map (Graphon.partIndex P) μ, ⋯⟩

theorem Graphon.measurePreserving_partIndex {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition Ω μ) : MeasureTheory.MeasurePreserving (partIndex P) μ ↑(partLaw P)

noncomputable def Graphon.stepMatrix {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (P : MeasurablePartition Ω μ) (U : Graphon Ω μ) (a b : Fin (P.parts.card + 1)) : ℝ

The step matrix on the finite factor: rectangle averages of U over the parts. Null cells need no special treatment — rectAverage is zero there.

Equations

• Graphon.stepMatrix P U a b = U.rectAverage (Graphon.indexPart P a) (Graphon.indexPart P b)

theorem Graphon.stepMatrix_symm {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition Ω μ) (U : Graphon Ω μ) (a b : Fin (P.parts.card + 1)) : stepMatrix P U a b = stepMatrix P U b a

theorem Graphon.stepMatrix_mem_Icc {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition Ω μ) (U : Graphon Ω μ) (a b : Fin (P.parts.card + 1)) : stepMatrix P U a b ∈ Set.Icc 0 1

noncomputable def Graphon.stepKernel {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition Ω μ) (U : Graphon Ω μ) : Graphon (Fin (P.parts.card + 1)) ↑(partLaw P)

The finite step kernel: the step matrix as a graphon on the finite factor.

Equations

• One or more equations did not get rendered due to their size.

theorem Graphon.stepKernel_ae {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition Ω μ) (U : Graphon Ω μ) : ∀ᵐ (q : Fin (P.parts.card + 1) × Fin (P.parts.card + 1)) ∂(↑(partLaw P)).prod ↑(partLaw P), ↑(stepKernel P U).toAEEqFun q = stepMatrix P U q.1 q.2

The finite step kernel agrees with the step matrix a.e.

theorem Graphon.pullback_stepKernel {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition Ω μ) (U : Graphon Ω μ) : (stepKernel P U).pullback (partIndex P) ⋯ = stepify P U

The pullback of the finite step kernel along the factor map is the stepification. This transports the Frieze–Kannan bound into the finite-factor form.

theorem Graphon.exists_finiteFactorApproximation {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (U : Graphon Ω μ) {ε : ℝ} (hε : 0 < ε) : Nonempty (U.FiniteFactorApproximation ε)

Finite-factor approximation exists at every scale. For every graphon and every 0 < ε there is a finite factor, a factor map, and a kernel on the factor whose pullback is within ε of the graphon in cut norm — with no standard-Borel, surjectivity, or positive-cell hypothesis. The factor is Fin (n + 1) with a bundled law, so the finite coupling machinery applies directly.