The rounding half of the First Sampling Lemma

This file proves RoundingEvent for all sufficiently large k (rounding_event_of_large_k): conditionally on a.e. sampled points x, the Bernoulli edge rounding G of the weighted sampled graphon H_{W,x} lands within cut distance ε of H_{W,x} with probability ≥ 1 − η. Together with the reduction sampleGoodMassOn_of_events this leaves PointSamplingEvent as the only analytic content of first_sampling_lemma.

The proof is finite probability — no measure-theoretic randomness beyond the finite weighted sums sampleMassAt:

1. Deterministic cut certificate (cutNormDiff_mkStepGraphon_le_of_cuts): the cut norm of a same-partition step-graphon difference is bounded by the maximum over finitely many vertex cuts A, B : Finset (Fin k) of the corresponding weighted cut sums. A rectangle integral decomposes over cell products (rectIntegralDiff_mkStepGraphon), and a box-constrained bilinear form is maximized at cuts (abs_bilinear_box_le, via the signed-support trick — no induction).
2. Bad-event decomposition: the bad rounding event is contained in the finite union over cut pairs of per-cut deviation events.
3. Finite Hoeffding / union bound: the moment generating function of a cut sum factorizes over independent edges (sum_graphs_prod, the powerset bijection), each edge contributing ≤ exp(λ²) for |λ| ≤ 1 (Real.exp_bound); a Chernoff argument over the finite sum and a union bound over ≤ 4^k cut pairs finish. Crude constants throughout — only existence of large k matters.

Layer 1(b): box-constrained bilinear forms are maximized at cuts

theorem Graphon.abs_sum_box_le {k : ℕ} (w φ : Fin k → ℝ) (M : ℝ) (hM : ∀ (A : Finset (Fin k)), |∑ i ∈ A, w i * φ i| ≤ M) (u : Fin k → ℝ) (hu : ∀ (i : Fin k), u i ∈ Set.Icc 0 (w i)) : |∑ i : Fin k, u i * φ i| ≤ M

Signed-support trick (linear case): a linear form with box-constrained coefficients is bounded by its values at finite cuts. No induction: the upper bound is witnessed by the cut {i | 0 ≤ φ i}, the lower one by its complement.

theorem Graphon.abs_bilinear_box_le {k : ℕ} (w : Fin k → ℝ) (d : Fin k → Fin k → ℝ) (M : ℝ) (hM : ∀ (A B : Finset (Fin k)), |∑ i ∈ A, ∑ j ∈ B, w i * w j * d i j| ≤ M) (u v : Fin k → ℝ) (hu : ∀ (i : Fin k), u i ∈ Set.Icc 0 (w i)) (hv : ∀ (j : Fin k), v j ∈ Set.Icc 0 (w j)) : |∑ i : Fin k, ∑ j : Fin k, u i * v j * d i j| ≤ M

Box-constrained bilinear forms are maximized at cut pairs: two applications of the signed-support trick.

Layer 1(a): rectangle integrals of step differences decompose over cells

theorem Graphon.setIntegral_mkStepFun {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) (c : Set α → Set α → ℝ) (S' T' : Set α) : ∫ (p : α × α) in S' ×ˢ T', mkStepFun P c p ∂μ.prod μ = ∑ S ∈ P.parts, ∑ T ∈ P.parts, (μ (S ∩ S')).toReal * (μ (T ∩ T')).toReal * c S T

Set integral of a step function over a rectangle: the finite sum of indicators integrates term by term.

theorem Graphon.rectIntegralDiff_mkStepGraphon {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (P : MeasurablePartition α μ) (c c' : Set α → Set α → ℝ) (hc_symm : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c S T = c T S) (hc_mem : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c S T ∈ Set.Icc 0 1) (hc'_symm : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c' S T = c' T S) (hc'_mem : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c' S T ∈ Set.Icc 0 1) (S' T' : Set α) : (mkStepGraphon P c hc_symm hc_mem).rectIntegralDiff (mkStepGraphon P c' hc'_symm hc'_mem) S' T' = ∑ S ∈ P.parts, ∑ T ∈ P.parts, (μ (S ∩ S')).toReal * (μ (T ∩ T')).toReal * (c S T - c' S T)

Rectangle integrals of a same-partition step-graphon difference decompose over cell products.

theorem Graphon.cutNormDiff_mkStepGraphon_le_of_cuts {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ} (P : MeasurablePartition α μ) (ι : Fin k → Set α) (hι_mem : ∀ (i : Fin k), ι i ∈ P.parts) (hι_inj : Function.Injective ι) (hι_surj : ∀ S ∈ P.parts, ∃ (i : Fin k), ι i = S) (c c' : Set α → Set α → ℝ) (hc_symm : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c S T = c T S) (hc_mem : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c S T ∈ Set.Icc 0 1) (hc'_symm : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c' S T = c' T S) (hc'_mem : ∀ S ∈ P.parts, ∀ T ∈ P.parts, c' S T ∈ Set.Icc 0 1) (M : ℝ) (hM : ∀ (A B : Finset (Fin k)), |∑ i ∈ A, ∑ j ∈ B, (μ (ι i)).toReal * (μ (ι j)).toReal * (c (ι i) (ι j) - c' (ι i) (ι j))| ≤ M) : (mkStepGraphon P c hc_symm hc_mem).cutNormDiff (mkStepGraphon P c' hc'_symm hc'_mem) ≤ M

Layer 1 — the deterministic cut certificate: the cut norm of a same-partition step-graphon difference is bounded by the maximum weighted cut sum over finitely many vertex cuts A, B : Finset (Fin k). Combines the cell decomposition with the box maximum principle (abs_bilinear_box_le), the box constraint being μ(cell ∩ S') ≤ μ(cell).

Layer 3: the finite Chernoff engine

Everything here is graphon-free: massOf p G is the Bernoulli graph distribution with abstract edge probabilities p, matching sampleMassAt W x definitionally when p e := W(x_i, x_j).

noncomputable def Graphon.massOf {k : ℕ} (p : Sym2 (Fin k) → ℝ) (G : SimpleGraph (Fin k)) : ℝ

The Bernoulli graph mass with abstract edge probabilities.

Equations

• Graphon.massOf p G = (∏ e ∈ G.edgeFinset, p e) * ∏ e ∈ ⊤.edgeFinset \ G.edgeFinset, (1 - p e)

theorem Graphon.sum_graphs_prod {k : ℕ} (F F' : Sym2 (Fin k) → ℝ) : ∑ G : SimpleGraph (Fin k), (∏ e ∈ G.edgeFinset, F e) * ∏ e ∈ ⊤.edgeFinset \ G.edgeFinset, F' e = ∏ e ∈ ⊤.edgeFinset, (F e + F' e)

Independence as algebra: a product functional of the edge states sums over all graphs to the product of per-edge sums (the powerset bijection + Finset.prod_add).

theorem Graphon.exp_le_one_add_add_sq {s : ℝ} (hs : |s| ≤ 1) : Real.exp s ≤ 1 + s + s ^ 2

Elementary quadratic exponential bound: e^s ≤ 1 + s + s² for |s| ≤ 1 (from Real.exp_bound at order 3).

theorem Graphon.bernoulli_mgf_le {p t : ℝ} (hp : p ∈ Set.Icc 0 1) (ht : |t| ≤ 1) : p * Real.exp (t * (1 - p)) + (1 - p) * Real.exp (-(t * p)) ≤ Real.exp (t ^ 2)

Bernoulli MGF bound (crude Hoeffding-lemma substitute): for p ∈ [0,1] and |t| ≤ 1, the centered Bernoulli MGF satisfies p·e^{t(1−p)} + (1−p)·e^{−tp} ≤ e^{t²}.

noncomputable def Graphon.cutStat {k : ℕ} (p κ : Sym2 (Fin k) → ℝ) (G : SimpleGraph (Fin k)) : ℝ

The centered cut statistic of a graph: Z(G) = ∑_e κ_e (χ_e(G) − p_e).

Equations

• Graphon.cutStat p κ G = ∑ e ∈ ⊤.edgeFinset, κ e * ((if e ∈ G.edgeFinset then 1 else 0) - p e)

theorem Graphon.sum_massOf_exp_cutStat_le {k : ℕ} (p κ : Sym2 (Fin k) → ℝ) (hp : ∀ e ∈ ⊤.edgeFinset, p e ∈ Set.Icc 0 1) (hκ : ∀ (e : Sym2 (Fin k)), |κ e| ≤ 2) {lam : ℝ} (hlam : |lam| ≤ 1 / 2) : ∑ G : SimpleGraph (Fin k), massOf p G * Real.exp (lam * cutStat p κ G) ≤ Real.exp (lam ^ 2 * 4 * ↑⊤.edgeFinset.card)

MGF factorization + per-edge bound: the exponential moment of a cut statistic is at most exp(λ²·4·|E(⊤)|) for |λ| ≤ 1/2 and |κ| ≤ 2.

theorem Graphon.massOf_nonneg {k : ℕ} {p : Sym2 (Fin k) → ℝ} (hp : ∀ e ∈ ⊤.edgeFinset, p e ∈ Set.Icc 0 1) (G : SimpleGraph (Fin k)) : 0 ≤ massOf p G

Bernoulli graph masses are nonnegative for [0,1] edge probabilities.

theorem Graphon.mass_tail_le {k : ℕ} (p κ : Sym2 (Fin k) → ℝ) (hp : ∀ e ∈ ⊤.edgeFinset, p e ∈ Set.Icc 0 1) (hκ : ∀ (e : Sym2 (Fin k)), |κ e| ≤ 2) {lam t : ℝ} (hlam0 : 0 ≤ lam) (hlam : |lam| ≤ 1 / 2) : ∑ G : SimpleGraph (Fin k) with t ≤ cutStat p κ G, massOf p G ≤ Real.exp (lam ^ 2 * 4 * ↑⊤.edgeFinset.card - lam * t)

One-sided Chernoff tail for cut statistics.

theorem Graphon.cutStat_neg {k : ℕ} (p κ : Sym2 (Fin k) → ℝ) (G : SimpleGraph (Fin k)) : cutStat p (fun (e : Sym2 (Fin k)) => -κ e) G = -cutStat p κ G

Negating the coefficients negates the cut statistic.

theorem Graphon.mass_tail_abs_le {k : ℕ} (p κ : Sym2 (Fin k) → ℝ) (hp : ∀ e ∈ ⊤.edgeFinset, p e ∈ Set.Icc 0 1) (hκ : ∀ (e : Sym2 (Fin k)), |κ e| ≤ 2) {lam t : ℝ} (hlam0 : 0 ≤ lam) (hlam : |lam| ≤ 1 / 2) : ∑ G : SimpleGraph (Fin k) with t ≤ |cutStat p κ G|, massOf p G ≤ 2 * Real.exp (lam ^ 2 * 4 * ↑⊤.edgeFinset.card - lam * t)

Two-sided Chernoff tail for cut statistics.

theorem Graphon.mass_bad_family_le {k : ℕ} {ι : Type u_2} [Fintype ι] (p : Sym2 (Fin k) → ℝ) (κfam : ι → Sym2 (Fin k) → ℝ) (hp : ∀ e ∈ ⊤.edgeFinset, p e ∈ Set.Icc 0 1) (hκ : ∀ (i : ι) (e : Sym2 (Fin k)), |κfam i e| ≤ 2) {lam t : ℝ} (hlam0 : 0 ≤ lam) (hlam : |lam| ≤ 1 / 2) : ∑ G : SimpleGraph (Fin k) with ∃ (i : ι), t ≤ |cutStat p (κfam i) G|, massOf p G ≤ ↑(Fintype.card ι) * (2 * Real.exp (lam ^ 2 * 4 * ↑⊤.edgeFinset.card - lam * t))

Union bound over a finite family of cut statistics.

Layer 2(i): almost-everywhere alignment of edge parameters

theorem Graphon.graphonEval_symm_ae {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ} (W : Graphon α μ) {i j : Fin k} (hij : i ≠ j) : ∀ᵐ (x : Fin k → α) ∂MeasureTheory.Measure.pi fun (x : Fin k) => μ, ↑W.toAEEqFun (x j, x i) = ↑W.toAEEqFun (x i, x j)

A.e. symmetry at a pair of coordinates (mirror of graphonEval_mem_Icc_ae): the graphon's a.e. symmetry transfers along the pair evaluation map.

theorem Graphon.ae_all_finset {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {k : ℕ} {β : Type u_2} (s : Finset β) (Φ : β → (Fin k → α) → Prop) (h : ∀ b ∈ s, ∀ᵐ (x : Fin k → α) ∂MeasureTheory.Measure.pi fun (x : Fin k) => μ, Φ b x) : ∀ᵐ (x : Fin k → α) ∂MeasureTheory.Measure.pi fun (x : Fin k) => μ, ∀ b ∈ s, Φ b x

Finite a.e. conjunction over a finset (the standard induction, packaged).

theorem Graphon.ae_edge_params_aligned {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] {k : ℕ} (W : Graphon α μ) : ∀ᵐ (x : Fin k → α) ∂MeasureTheory.Measure.pi fun (x : Fin k) => μ, ∀ e ∈ ⊤.edgeFinset, ↑W.toAEEqFun (x (Quot.out e).1, x (Quot.out e).2) ∈ Set.Icc 0 1 ∧ min 1 (max 0 (↑W.toAEEqFun (x (min (Quot.out e).1 (Quot.out e).2), x (max (Quot.out e).1 (Quot.out e).2)))) = ↑W.toAEEqFun (x (Quot.out e).1, x (Quot.out e).2)

The aligned edge-parameter event: for a.e. sampled points, every edge parameter is in [0,1] and agrees with the clamped (min, max)-ordered evaluation used by the weighted sampled graphon.

Layer 2(ii): cut coefficients and the edge regrouping

noncomputable def Graphon.cutCoeff {k : ℕ} (A B : Finset (Fin k)) (e : Sym2 (Fin k)) : ℝ

The number of ordered off-diagonal pairs of the cut A × B mapping to the edge e.

Equations

• Graphon.cutCoeff A B e = ↑{ij ∈ A ×ˢ B | ij.1 ≠ ij.2 ∧ s(ij.1, ij.2) = e}.card

theorem Graphon.cutCoeff_le_two {k : ℕ} (A B : Finset (Fin k)) (e : Sym2 (Fin k)) : |cutCoeff A B e| ≤ 2

Each edge collects at most its two orientations.

theorem Graphon.sum_pairs_eq_sum_edges {k : ℕ} (A B : Finset (Fin k)) (f : Sym2 (Fin k) → ℝ) : ∑ ij ∈ A ×ˢ B with ij.1 ≠ ij.2, f s(ij.1, ij.2) = ∑ e ∈ ⊤.edgeFinset, cutCoeff A B e * f e

Edge regrouping: a sum of an edge functional over the off-diagonal ordered pairs of a cut equals the cutCoeff-weighted sum over edges.

Layer 2(iii): small combinatorial and numeric ingredients

theorem Graphon.minmax_out {k : ℕ} {i j : Fin k} : min (Quot.out s(i, j)).1 (Quot.out s(i, j)).2 = min i j ∧ max (Quot.out s(i, j)).1 (Quot.out s(i, j)).2 = max i j

The (min, max)-normalization of an unordered pair is orientation-independent.

theorem Graphon.card_diag_pairs_le {k : ℕ} (A B : Finset (Fin k)) : {ij ∈ A ×ˢ B | ij.1 = ij.2}.card ≤ k

The diagonal of a cut has at most k ordered pairs.

theorem Graphon.eventually_union_bound_small (c η : ℝ) (hc : 0 < c) (hη : 0 < η) : ∃ (K : ℕ), ∀ (k : ℕ), K ≤ k → 4 ^ k * (2 * Real.exp (-(c * ↑k ^ 2))) ≤ η

The eventual union-bound decay: 4^k · 2·exp(−c·k²) ≤ η for all large k.

Layer 2(iv): the rounding theorem

theorem Graphon.choose_cell_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} [NeZero k] {i : Fin k} (h : ∃ (i' : Fin k), equipartitionCell k i' = equipartitionCell k i) : h.choose = i

Collapse of the cell-existential choice through injectivity.

theorem Graphon.rounding_event_of_large_k {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (ε η : ℝ) (hε : 0 < ε) (hη : 0 < η) : ∃ (K : ℕ), ∀ (k : ℕ), K ≤ k → ∀ (x : NeZero k) (W : Graphon α μ), W.RoundingEvent k ε η

RoundingEvent holds for all sufficiently large k, uniformly in the graphon — the finite-probability half of the First Sampling Lemma. The threshold K depends only on (ε, η).