Concentration scaffold for the First Sampling Lemma

The First Sampling Lemma (first_sampling_lemma, proved 2026-07-08 in Graphon/SamplingLemma.lean) was the sampling route's one analytic sorry. This file decomposes it along the classical two-stage analysis: all statements here are proved or packaged as hypotheses of a proved reduction.

The two-stage decomposition (Lovász, Large Networks and Graph Limits, §10.5–10.6): condition on the sampled points x : Fin k → α, and interpolate through the weighted sampled graphon H_{W,x} := sampleWeightedGraphonOn W x (matrix entries W(xᵢ, xⱼ) on the equal-measure k-partition):

1. Point sampling (PointSamplingEvent): with probability ≥ 1 − η₁ over x, d_□(W, H_{W,x}) < ε/2 — the genuinely analytic step (Lemma 10.11 / Azuma).
2. Rounding (RoundingEvent): conditionally on (a.e.) x, the Bernoulli edge rounding G of H_{W,x} satisfies d_□(H_{W,x}, K_G) < ε/2 with conditional probability ≥ 1 − η₂ — a finite union bound over cuts.

sampleGoodMassOn_of_events (PROVED) recombines the two stages into the good-mass bound demanded by first_sampling_lemma; the deterministic triangle route cutDistance_ofSimpleGraphOn_le is the gluing inequality. Both events were established with W-uniform k (point_sampling_event_of_large_k, rounding_event_of_large_k), completing first_sampling_lemma (2026-07-08, Graphon/SamplingLemma.lean).

Main declarations

• Graphon.sampleMassAt — the conditional edge distribution at fixed sampled points, with sampleMass W G = ∫ x, sampleMassAt W x G
• Graphon.sampleWeightedGraphonOn — the weighted sampled step graphon H_{W,x}
• Graphon.cutDistance_ofSimpleGraphOn_le — the deterministic triangle route
• Graphon.PointSamplingEvent, Graphon.RoundingEvent — the two concentration events
• Graphon.sampleGoodMassOn_of_events — the PROVED reduction: both events ⟹ the good-mass bound of first_sampling_lemma

noncomputable def Graphon.sampleMassAt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {k : ℕ} (W : Graphon α μ) (x : Fin k → α) (G : SimpleGraph (Fin k)) : ℝ

The conditional edge distribution: the probability that the sampled graph equals G, conditioned on the sampled points being x. (Definitionally the integrand of sampleMass.)

Equations

• W.sampleMassAt x G = W.sampleIntegrand G x

theorem Graphon.sampleMass_eq_integral_sampleMassAt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {k : ℕ} (W : Graphon α μ) (G : SimpleGraph (Fin k)) : W.sampleMass G = ∫ (x : Fin k → α), W.sampleMassAt x G ∂MeasureTheory.Measure.pi fun (x : Fin k) => μ

The unconditional mass integrates the conditional one over the sampled points.

theorem Graphon.sampleMassAt_sum_eq_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {k : ℕ} (W : Graphon α μ) (x : Fin k → α) : ∑ G : SimpleGraph (Fin k), W.sampleMassAt x G = 1

The conditional masses form a probability distribution at every point.

theorem Graphon.sampleMassAt_nonneg_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ} (W : Graphon α μ) : ∀ᵐ (x : Fin k → α) ∂MeasureTheory.Measure.pi fun (x : Fin k) => μ, ∀ (G : SimpleGraph (Fin k)), 0 ≤ W.sampleMassAt x G

The conditional masses are nonnegative for a.e. sampled points.

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

The weighted sampled step graphon H_{W,x}: on the chosen equal-measure k-partition (the same equipartition k used by ofSimpleGraphOn), the cell (i, j) carries the entry W(xᵢ, xⱼ) — clamped into [0,1] and evaluated at the (min, max)-ordered pair, so the coefficients are pointwise symmetric and bounded (the clamp and the ordering are invisible a.e. in x since W is a.e. [0,1]-valued and a.e. symmetric).

Equations

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

theorem Graphon.cutDistance_ofSimpleGraphOn_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} [NeZero k] (W : Graphon α μ) (x : Fin k → α) (G : SimpleGraph (Fin k)) : W.cutDistance (ofSimpleGraphOn G) ≤ W.cutDistance (W.sampleWeightedGraphonOn x) + (W.sampleWeightedGraphonOn x).cutDistance (ofSimpleGraphOn G)

The deterministic triangle route: closeness of W to the weighted sample and of the weighted sample to the rounded graph combine into goodness of the sampled graph.

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

Stage 1 — point-sampling concentration (event form): with probability ≥ 1 − η over the sampled points, the weighted sampled graphon is ε-close to W. The measurable witness set is part of the data (measurability of x ↦ d_□(W, H_{W,x}) is not needed anywhere). This is the genuinely analytic content of the First Sampling Lemma (Lovász Lemma 10.11 / Azuma–Hoeffding).

Equations

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

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

Stage 2 — rounding concentration (event form): for a.e. sampled points, the Bernoulli edge rounding lands ε-close to the weighted sampled graphon with conditional probability ≥ 1 − η. A finite union bound over cuts (proved: rounding_event_of_large_k, Graphon/SamplingRounding.lean; the a.e. qualifier absorbs the pointwise pathologies of the L⁰ representative).

Equations

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

theorem Graphon.sampleGoodMassOn_of_events {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (k : ℕ) [NeZero k] (ε η₁ η₂ : ℝ) (hη₂ : 0 ≤ η₂) (hpt : W.PointSamplingEvent k (ε / 2) η₁) (hrd : W.RoundingEvent k (ε / 2) η₂) : 1 - η₁ - η₂ ≤ W.sampleGoodMassOn k ε

The recombination (PROVED): the two concentration events at accuracy ε/2 yield the good-mass bound demanded by first_sampling_lemma at accuracy ε. Both events were subsequently established with W-uniform k (point_sampling_event_of_large_k, rounding_event_of_large_k), completing the First Sampling Lemma — no new independent assumption is introduced anywhere in the chain.