The sampling route to the quantitative inverse counting lemma

This file hosts the space-generic good-mass layer over the sampled graph distribution (Graphon/Sampling.lean) and derives the partition-size-independent quantitative inverse counting lemma from the (sorried) First Sampling Lemma.

Everything is stated over an arbitrary atomless standard Borel probability space: the classical sampling lemma is not inherently about [0,1] — the unit interval is just a convenient presentation — and the space-generic statement is the honest interface, since transferring cut distances between spaces would require the measure isomorphism theorem (α ≅ ([0,1], volume) mod 0), which mathlib currently lacks (it is Rokhlin-adjacent and will be developed with that blocker).

Main declarations

• Graphon.exists_partition_with_measures — partitions with prescribed cell measures (moved from Graphon/InverseCounting.lean)
• Graphon.ofSimpleGraphOn — the finite-graph step-graphon embedding on an arbitrary atomless standard Borel space (equal-measure cells)
• Graphon.sampleGoodMassOn — probability that the sampled graph lands within cut distance ε of W
• (moved) Graphon.first_sampling_lemma and Graphon.sampling_quantitative_icl now live in Graphon/SamplingLemma.lean, downstream of the two proved concentration events — the First Sampling Lemma is PROVED there by recombination

References

• [L. Lovász, Large Networks and Graph Limits][lovasz2012], Lemma 10.16
• Borgs–Chayes–Lovász–Sós–Vesztergombi, Convergent sequences of dense graphs I, Theorem 4.6

theorem Graphon.exists_partition_with_measures {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {K : ℕ} (w : Fin K → ℝ) (hw_nn : ∀ (i : Fin K), 0 ≤ w i) (hw_sum : ∑ i : Fin K, w i = 1) : ∃ (P : MeasurablePartition α μ) (ι : Fin K → Set α), (∀ (i : Fin K), ι i ∈ P.parts) ∧ Function.Injective ι ∧ (∀ S ∈ P.parts, ∃ (i : Fin K), ι i = S) ∧ P.parts.card = K ∧ ∀ (i : Fin K), (μ (ι i)).toReal = w i

Build a MeasurablePartition with K cells having prescribed measures. (Moved here from Graphon/InverseCounting.lean, 2026-07-07, and de-privatized so the sampling layer can build finite-graph embeddings on arbitrary atomless standard Borel spaces.)

noncomputable def Graphon.equipartition {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) [NeZero k] : MeasurablePartition α μ

A chosen equal-measure k-cell partition (shared by every finite-graph and weighted-sample embedding at level k, so their step graphons live on the SAME partition).

Equations

• Graphon.equipartition k = ⋯.choose

noncomputable def Graphon.equipartitionCell {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) [NeZero k] : Fin k → Set α

The chosen enumeration of the cells of equipartition k.

Equations

• Graphon.equipartitionCell k = ⋯.choose

theorem Graphon.equipartitionCell_mem {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) [NeZero k] (i : Fin k) : equipartitionCell k i ∈ (equipartition k).parts

theorem Graphon.equipartitionCell_injective {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) [NeZero k] : Function.Injective (equipartitionCell k)

theorem Graphon.equipartitionCell_surjOn {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) [NeZero k] (S : Set α) : S ∈ (equipartition k).parts → ∃ (i : Fin k), equipartitionCell k i = S

theorem Graphon.equipartitionCell_measure {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (k : ℕ) [NeZero k] (i : Fin k) : (μ (equipartitionCell k i)).toReal = (↑k)⁻¹

noncomputable def Graphon.ofSimpleGraphOn {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} [NeZero k] (G : SimpleGraph (Fin k)) : Graphon α μ

The finite-graph embedding on an arbitrary atomless standard Borel space: the step graphon of G over the chosen equal-measure k-cell partition (equipartition k), with 0/1 coefficients given by adjacency. The generic analogue of ofSimpleGraph (which is the [0,1]-interval presentation). Downstream uses treat this as opaque.

Equations

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

noncomputable def Graphon.sampleGoodMassOn {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (k : ℕ) [NeZero k] (ε : ℝ) : ℝ

The mass of "good" sampled graphs: those whose embedded step graphon lies within cut distance ε of W.

Equations

• W.sampleGoodMassOn k ε = ∑ G : SimpleGraph (Fin k), if W.cutDistance (Graphon.ofSimpleGraphOn G) < ε then W.sampleMass G else 0

theorem Graphon.sampleGoodMassOn_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (k : ℕ) [NeZero k] (ε : ℝ) : 0 ≤ W.sampleGoodMassOn k ε

The good mass is nonnegative.

theorem Graphon.sampleGoodMassOn_le_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (k : ℕ) [NeZero k] (ε : ℝ) : W.sampleGoodMassOn k ε ≤ 1

The good mass is at most 1.

theorem Graphon.sampleGoodMassOn_mono {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (k : ℕ) [NeZero k] {ε₁ ε₂ : ℝ} (h : ε₁ ≤ ε₂) : W.sampleGoodMassOn k ε₁ ≤ W.sampleGoodMassOn k ε₂

The good mass is monotone in the accuracy ε.

theorem Graphon.one_sub_sampleGoodMassOn {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (k : ℕ) [NeZero k] (ε : ℝ) : 1 - W.sampleGoodMassOn k ε = ∑ G : SimpleGraph (Fin k), if ε ≤ W.cutDistance (ofSimpleGraphOn G) then W.sampleMass G else 0

Complement form: the bad mass is 1 minus the good mass.

theorem Graphon.sampleGoodMassOn_extract {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} [NeZero k] (U W : Graphon α μ) (ε η ρ tv : ℝ) (hUW : U.cutDistance W ≤ ρ) (htv : ∑ G : SimpleGraph (Fin k), |U.sampleMass G - W.sampleMass G| ≤ tv) (hU : 1 - η < U.sampleGoodMassOn k ε) : 1 - η - tv < W.sampleGoodMassOn k (ε + ρ)

Good-mass extraction — the coupling bridge. If U and W are within cut distance ρ and their sampled distributions are within total variation tv, then a (1−η)-good mass for U at accuracy ε yields a (1−η−tv)-good mass for W at the slackened accuracy ε + ρ. The slack ρ is unavoidable (the good events differ), and this lemma is NOT used in the ICL derivation below (that would be circular); it is the general-purpose coupling form.