The point-sampling half of the First Sampling Lemma (scaffold)

Target (PR #11):

point_sampling_event_of_large_k : ∀ ε η > 0, ∃ K, ∀ k ≥ K, ∀ [NeZero k], ∀ W : Graphon α μ, PointSamplingEvent W k ε η

matching the shape of rounding_event_of_large_k, so that PR #12 can pick one k for both events and close first_sampling_lemma via sampleGoodMassOn_of_events.

Design notes (recorded 2026-07-07)

• The rounding-style union bound does NOT work here. For a fixed index cut A, B ⊆ Fin k, the statistic (1/k²) ∑_{i∈A,j∈B} D(xᵢ, xⱼ) is a function of the k sampled points with bounded differences ≤ 2/k, so vertex-exposure Azuma gives only exp(−c ε² k) tails — which loses against the 4^k cut pairs. This is the genuine extra difficulty of point sampling versus rounding (where independence over k² edges gave exp(−c k²)).
• The classical route (Lovász, Large Networks and Graph Limits, Lemma 10.6; BCLSV "Convergent sequences I" §4.3) therefore bounds the EXPECTATION of the sup first — E_x[d_□(W, H_{W,x})] → 0 uniformly in W — by the ghost-sample / quadratic-form argument, and only then concentrates the (bounded-differences) random variable x ↦ d_□(W, H_{W,x}) around its expectation via McDiarmid/Azuma.
• Step reduction helps but does not dodge the core. With Frieze–Kannan (regularity, PROVED) one may reduce W to a step graphon U with m(ε) parts: d(W,H_{W,x}) ≤ d(W,U) + d(U,H_{U,x}) + d(H_{U,x},H_{W,x}). The middle term is finite (cell-frequency concentration, m cells, honest union bound). The last term is the empirical matrix of the small-cut-norm kernel D := W − U, and bounding ITS cut norm is exactly the hard expectation step — sampling does not commute with cut-norm smallness pointwise.
• Mathlib support: Mathlib.Probability.Moments.SubGaussian provides HasSubgaussianMGF, Hoeffding for independent sums, and the conditionally sub-Gaussian Azuma (measure_sum_ge_le_of_HasCondSubgaussianMGF); there is no off-the-shelf McDiarmid, so the bounded-differences step will go through the conditional sub-Gaussian route (Doob/vertex-exposure decomposition of f(x) − E f) or a bespoke finite version in the style of SamplingRounding.
• Measurability of the witness set (PointSamplingEvent carries it as data): the plan is to take X := {x | discretized majorant of d_□(W, H_{W,x}) < ε} for a FINITE discretization of the cut-norm sup (cell-cuts on the H-side suffice for a 2-sided estimate up to constants), making X a finite intersection/union of preimages of measurable coordinate functions. If this still turns ugly, a narrowed named lemma for the measurable bad set stays inside the first_sampling_lemma accounting — NOT a new live input.

Layer plan (per the PR #11 decomposition)

1. discretized cut norm approximation — reduce d_□(W, H_{W,x}) to finitely many cut predicates in the sampled coordinates, with controlled error.
2. bounded-differences / Azuma scaffold — the vertex-exposure decomposition for functionals of the sampled point sequence.
3. uniform tail bound — the expectation bound (Lovász 10.6 core) + concentration, uniform in W.
4. event packaging — the measurable witness set for PointSamplingEvent.

PR #11A architecture (settled 2026-07-07, after literature check)

Reference mechanisms: Lovász Lemmas 10.6/10.7 (bounded kernels); the modern generalization arXiv:2203.07581 confirms the split into systematic error (expectation bound; Q-subsample ghost argument, their §6.2) and dispersion (vertex-exposure martingale + Azuma — deferred to PR #11B).

Majorant + triangle decomposition. Fix ε; let P be the Frieze–Kannan partition of W at quality ε' := ε/8 with m = m(ε') parts (uniform in W — PROVED regularity), U := stepify P W. Then

d_□(W, H_{W,x}) ≤ ε' + d_□(U, H_{U,x}) + maxcut((W−U)[x])

• Frequency term d_□(U, H_{U,x}): H_{U,x} is the equipartition step graphon with entries U(xᵢ,xⱼ); comparing to U is a pure weight-perturbation problem — bounded by 2·∑_cells |empirical frequency − μ(cell)| (repo tooling: cutDistance_step_weight_le-style). Its expectation is elementary: E|freq − μ| ≤ 1/(2√k) per cell via Cauchy–Schwarz + the iid variance computation (E(freq−μ)² = μ(1−μ)/k) — no concentration inequality needed, m cells total.
• Core term maxcut(D[x]), D := W − U, ‖D‖_□ ≤ ε', |D| ≤ 1: THE deep step — E_x[max_{S,T ⊆ [k]} (1/k²)|∑_{i∈S,j∈T} D(xᵢ,xⱼ)|] ≤ ‖D‖_□ + O(k^{−1/4}). Mechanism (Q-subsample cut guessing; AFKK / book 10.7): naive union over 4^k cuts fails (only exp(−cε²k) per-cut tails). Instead: for the maximizer (S*,T*), the optimal T given S is the sign set of r_j := (1/k)∑_{i∈S*} D(xᵢ,xⱼ); estimate r_j by a random subsample Q of size q (error O(1/√q) per point in expectation), so the near-optimal cut is DETERMINED by (x_Q, S* ∩ Q) — only 2^q selection rules. For each FIXED rule, the cut becomes a genuine measurable set determined by the Q-coordinates, independent of the fresh coordinates, so the fresh-sample expectation of the rectangle sum is ≤ ‖D‖_□ + O((q + √k)/k). Union over 2^q rules with second-moment control; q := ⌈√k⌉ gives O(k^{−1/4}). Both ± directions by applying to D and −D.

PR #11A execution notes (2026-07-07 survey of repo APIs)

• Deliverable shape (point_sampling_expectation_bound): ∃K, ∀ k ≥ K, ∀ W, ∃ a measurable nonnegative integrable majorant M with ∀ᵐ x, cutDistance W (sampleWeightedGraphonOn W x) ≤ M x and ∫ M < ε.
• KEY SIMPLIFICATION — PR #11B is just Markov. Given the expectation bound at accuracy ε·η, Markov's inequality on the nonnegative majorant gives π{M ≥ ε} ≤ η, and X := {M < ε} \ N (N a measurable null superset of the domination-failure set) is the measurable witness for PointSamplingEvent W k ε η. NO Azuma / bounded differences needed for the qualitative statement — concentration would only improve η-rates.
• regularity W ε hε : ∃ P, P.parts.card ≤ regularityBound ε ∧ cutNormDiff W (stepify P W) ≤ ε (proved) — the m(ε) source.
• cutDistance_step_weight_le (InverseCounting, PRIVATE — de-privatize like exists_partition_with_measures; carries the Rokhlin trace, acceptable): needs the SAME cell count on both sides via injective enumerations. For the frequency term (d(U, H_{U,x})), the coarsened partition (equicells grouped by the P-cell of their sample point) can have EMPTY groups, which break enumeration injectivity — pad empty groups with distinct measure-zero decorated cells (singleton-point technique from exists_partition_with_measures's proof). This is the main construction cost of the frequency layer.
• The coefficient alignment (U(xᵢ,xⱼ) = c_P(cell of xᵢ, cell of xⱼ) at sampled points, clamps invisible) is a.e.-x, via the graphonEval transfer machinery (as in ae_edge_params_aligned) applied to BOTH W and U := stepify P W.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloq. Publ. 60 (2012), Lemmas 10.6, 10.7, 10.16 (First Sampling Lemma).
• C. Borgs, J.T. Chayes, L. Lovász, V.T. Sós, K. Vesztergombi, Convergent sequences of dense graphs I, Adv. Math. 219 (2008), §4.3.
• N. Alon, W. Fernandez de la Vega, R. Kannan, M. Karpinski, Random sampling and approximation of MAX-CSPs, J. Comput. Syst. Sci. 67 (2003) — the Q-subsample cut-guessing mechanism.
• M. Borbényi, B. Ráth, S. Rokob, The cut norm and sampling lemmas for unbounded kernels, arXiv:2203.07581 — modern treatment; confirms the systematic-error / dispersion split.

PR #11A Layers 1+2: the point-sampling majorant and its frequency accounting

This section builds the nonnegative, measurable, integrable majorant pointSamplingMajorant W ε' k x dominating cutDistance W (H_{W,x}) a.e., and bounds the expectation of its frequency term. The deep core term (Layer 3, the AFKK Q-subsample ghost argument) is isolated in the private lemma coreTerm_expectation_bound (fully proved; this section's layering dates from when it was the last open obligation).

The triangle decomposition through U := stepify P W (P the Frieze–Kannan partition of W at quality ε') is

d_□(W, H_{W,x}) ≤ d_□(W, U) + d_□(U, H_{U,x}) + d_□(H_{U,x}, H_{W,x}) ≤ ε' + freqTerm + coreTerm.

• d_□(W, U) ≤ cutNormDiff W U ≤ ε' — cutDistance_le_cutNormDiff + regularity.
• d_□(H_{U,x}, H_{W,x}) ≤ coreTerm — the PR #10 cut certificate cutNormDiff_mkStepGraphon_le_of_cuts, pointwise in x.
• d_□(U, H_{U,x}) ≤ freqTerm — the weight-perturbation construction (see cutDistance_chosenStep_sampleWeighted_le_freqTerm).

noncomputable def Graphon.chosenPartition {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (ε' : ℝ) : MeasurablePartition α μ

The chosen Frieze–Kannan partition of W at quality ε' (junk trivialPartition when ε' ≤ 0; all theorems below carry 0 < ε').

Equations

• W.chosenPartition ε' = if hε' : 0 < ε' then ⋯.choose else Graphon.trivialPartition

noncomputable def Graphon.chosenStep {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (ε' : ℝ) : Graphon α μ

The chosen step-graphon approximation U := stepify P W.

Equations

• W.chosenStep ε' = Graphon.stepify (W.chosenPartition ε') W

noncomputable def Graphon.clampEval {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (V : Graphon α μ) {k : ℕ} (x : Fin k → α) (i j : Fin k) : ℝ

The clamped, (min,max)-ordered evaluation of a graphon V at the sampled pair (x_i, x_j) — matching the coefficient shape of sampleWeightedGraphonOn.

Equations

• V.clampEval x i j = min 1 (max 0 (↑V.toAEEqFun (x (min i j), x (max i j))))

noncomputable def Graphon.empFreq {α : Type u_1} {k : ℕ} (S : Set α) (x : Fin k → α) : ℝ

The empirical frequency of a cell S among the k sampled points.

Equations

• Graphon.empFreq S x = ↑{i : Fin k | x i ∈ S}.card / ↑k

noncomputable def Graphon.freqTerm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) (x : Fin k → α) : ℝ

The frequency term: 2·∑_cells |empirical frequency − μ(cell)|, plus a 1/k slack absorbing the diagonal mismatch between H_{U,x} and the coarsened comparison graphon (see the domination proof).

Equations

• W.freqTerm ε' k x = 2 * ∑ S ∈ (W.chosenPartition ε').parts, |Graphon.empFreq S x - (μ S).toReal| + (↑k)⁻¹

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

The core term: the maximum, over vertex cuts A, B ⊆ [k], of the weighted cut sum of the empirical matrix clampEval W − clampEval U on the equipartition. Its summand shape matches cutNormDiff_mkStepGraphon_le_of_cuts exactly (weights (μ cell)·(μ cell)), so the certificate applies to d_□(H_{U,x}, H_{W,x}) directly.

Equations

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

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

The point-sampling majorant ε' + freqTerm + coreTerm.

Equations

• W.pointSamplingMajorant ε' k x = ε' + W.freqTerm ε' k x + W.coreTerm ε' k x

Bounds and nonnegativity

theorem Graphon.clampEval_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (V : Graphon α μ) {k : ℕ} (x : Fin k → α) (i j : Fin k) : 0 ≤ V.clampEval x i j

theorem Graphon.clampEval_le_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (V : Graphon α μ) {k : ℕ} (x : Fin k → α) (i j : Fin k) : V.clampEval x i j ≤ 1

theorem Graphon.coreTerm_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) [NeZero k] (x : Fin k → α) : 0 ≤ W.coreTerm ε' k x

theorem Graphon.coreTerm_le_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) [NeZero k] (x : Fin k → α) : W.coreTerm ε' k x ≤ 1

Crude uniform bound on the core term: coreTerm ≤ 1.

theorem Graphon.empFreq_nonneg {α : Type u_1} {k : ℕ} (S : Set α) (x : Fin k → α) : 0 ≤ empFreq S x

theorem Graphon.empFreq_le_one {α : Type u_1} {k : ℕ} [NeZero k] (S : Set α) (x : Fin k → α) : empFreq S x ≤ 1

theorem Graphon.abs_empFreq_sub_le_one {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [StandardBorelSpace α] {k : ℕ} [NeZero k] (S : Set α) (x : Fin k → α) (hS : (μ S).toReal ≤ 1) : |empFreq S x - (μ S).toReal| ≤ 1

The frequency deviation of a single cell is at most 1.

theorem Graphon.freqTerm_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) [NeZero k] (x : Fin k → α) : 0 ≤ W.freqTerm ε' k x

theorem Graphon.pointSamplingMajorant_nonneg {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) {ε' : ℝ} (hε' : 0 ≤ ε') (k : ℕ) [NeZero k] (x : Fin k → α) : 0 ≤ W.pointSamplingMajorant ε' k x

The nonnegativity of the majorant (given 0 ≤ ε').

Measurability and integrability

theorem Graphon.measurable_clampEval {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (V : Graphon α μ) {k : ℕ} (i j : Fin k) : Measurable fun (x : Fin k → α) => V.clampEval x i j

theorem Graphon.measurable_empFreq {α : Type u_1} [MeasurableSpace α] {k : ℕ} {S : Set α} (hS : MeasurableSet S) : Measurable fun (x : Fin k → α) => empFreq S x

theorem Graphon.measurable_freqTerm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) [NeZero k] : Measurable fun (x : Fin k → α) => W.freqTerm ε' k x

theorem Graphon.measurable_coreTerm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) [NeZero k] : Measurable fun (x : Fin k → α) => W.coreTerm ε' k x

theorem Graphon.measurable_pointSamplingMajorant {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) [NeZero k] : Measurable fun (x : Fin k → α) => W.pointSamplingMajorant ε' k x

theorem Graphon.freqTerm_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) [NeZero k] (x : Fin k → α) : W.freqTerm ε' k x ≤ 2 * ↑(W.chosenPartition ε').parts.card + 1

Crude uniform bound on the frequency term.

theorem Graphon.integrable_pointSamplingMajorant {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) [NeZero k] : MeasureTheory.Integrable (fun (x : Fin k → α) => W.pointSamplingMajorant ε' k x) (MeasureTheory.Measure.pi fun (x : Fin k) => μ)

A.e. domination

theorem Graphon.cutDistance_W_chosenStep_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon α μ) {ε' : ℝ} (hε' : 0 < ε') : W.cutDistance (W.chosenStep ε') ≤ ε'

Part a (deterministic): W is ε'-close to its step approximation.

theorem Graphon.cutDistance_sampleWeighted_le_coreTerm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) [NeZero k] (x : Fin k → α) : ((W.chosenStep ε').sampleWeightedGraphonOn x).cutDistance (W.sampleWeightedGraphonOn x) ≤ W.coreTerm ε' k x

Part b (pointwise cut certificate): the two weighted sampled graphons differ by at most the core term. Applies cutNormDiff_mkStepGraphon_le_of_cuts on the equipartition.

theorem Graphon.chosenStep_eq_mkStepGraphon {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (ε' : ℝ) : W.chosenStep ε' = mkStepGraphon (W.chosenPartition ε') W.rectAverage ⋯ ⋯

chosenStep W ε' is definitionally the step graphon on chosenPartition W ε' with the rectangle-average coefficients rectAverage W.

theorem Graphon.ae_forall_sample_mem_part {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (P : MeasurablePartition α μ) {k : ℕ} [NeZero k] : ∀ᵐ (x : Fin k → α) ∂MeasureTheory.Measure.pi fun (x : Fin k) => μ, ∀ (i : Fin k), ∃ S ∈ P.parts, x i ∈ S

For a.e. sampled x, every sampled point lies in some part of P.

theorem Graphon.cutNormDiff_eq_zero_of_ae_eq {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (V₁ V₂ : Graphon α μ) (h : ∀ᵐ (p : α × α) ∂μ.prod μ, ↑V₁.toAEEqFun p = ↑V₂.toAEEqFun p) : V₁.cutNormDiff V₂ = 0

Graphons with a.e.-equal kernels are at cut-norm difference zero (every rectangle integral of the difference vanishes).

noncomputable def Graphon.coeffOfMatrix {α : Type u_1} {n : ℕ} (ι : Fin n → Set α) (M : Fin n → Fin n → ℝ) : Set α → Set α → ℝ

A step-graphon coefficient function built from a symmetric matrix M indexed through an injective enumeration ι : Fin n → Set α (matching the dite-shape of sampleWeightedGraphonOn).

Equations

• Graphon.coeffOfMatrix ι M A B = if h : (∃ (i : Fin n), ι i = A) ∧ ∃ (j : Fin n), ι j = B then M ⋯.choose ⋯.choose else 0

theorem Graphon.coeffOfMatrix_symm {α : Type u_1} [MeasurableSpace α] {n : ℕ} (ι : Fin n → Set α) (M : Fin n → Fin n → ℝ) (hM : ∀ (i j : Fin n), M i j = M j i) (A B : Set α) : coeffOfMatrix ι M A B = coeffOfMatrix ι M B A

theorem Graphon.coeffOfMatrix_mem {α : Type u_1} [MeasurableSpace α] {n : ℕ} (ι : Fin n → Set α) (M : Fin n → Fin n → ℝ) (hM : ∀ (i j : Fin n), M i j ∈ Set.Icc 0 1) (A B : Set α) : coeffOfMatrix ι M A B ∈ Set.Icc 0 1

theorem Graphon.coeffOfMatrix_eq {α : Type u_1} [MeasurableSpace α] {n : ℕ} (ι : Fin n → Set α) (M : Fin n → Fin n → ℝ) (hι : Function.Injective ι) (a b : Fin n) : coeffOfMatrix ι M (ι a) (ι b) = M a b

theorem Graphon.ae_cutDistance_le_pointSamplingMajorant {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) {ε' : ℝ} (hε' : 0 < ε') (k : ℕ) [NeZero k] : ∀ᵐ (x : Fin k → α) ∂MeasureTheory.Measure.pi fun (x : Fin k) => μ, W.cutDistance (W.sampleWeightedGraphonOn x) ≤ W.pointSamplingMajorant ε' k x

A.e. domination of the cut distance by the point-sampling majorant. Assembles the triangle d_□(W, H_{W,x}) ≤ d_□(W, U) + d_□(U, H_{U,x}) + d_□(H_{U,x}, H_{W,x}) from parts a (cutDistance_W_chosenStep_le), c (cutDistance_chosenStep_sampleWeighted_le_freqTerm) and b (cutDistance_sampleWeighted_le_coreTerm).

Layer 2: the frequency expectation bound

theorem Graphon.measurable_abs_empFreq_sub {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [StandardBorelSpace α] {k : ℕ} {S : Set α} (hS : MeasurableSet S) : Measurable fun (x : Fin k → α) => |empFreq S x - (μ S).toReal|

theorem Graphon.integrable_abs_empFreq_sub {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] {k : ℕ} [NeZero k] {S : Set α} (hS : MeasurableSet S) : MeasureTheory.Integrable (fun (x : Fin k → α) => |empFreq S x - (μ S).toReal|) (MeasureTheory.Measure.pi fun (x : Fin k) => μ)

theorem Graphon.freqTerm_expectation_bound {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) [NeZero k] : (∫ (x : Fin k → α), W.freqTerm ε' k x ∂MeasureTheory.Measure.pi fun (x : Fin k) => μ) ≤ ↑(W.chosenPartition ε').parts.card / √↑k + (↑k)⁻¹

Layer 2 — the frequency expectation bound. The expectation of the frequency term is at most m/√k + 1/k, where m is the number of Frieze–Kannan cells; both terms vanish as k → ∞ (with m = m(ε') fixed). Elementary: linearity of the integral plus the per-cell integral_abs_empFreq_sub_le.

theorem Graphon.chosenStep_cutNormDiff_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) {ε' : ℝ} (hε' : 0 < ε') : W.cutNormDiff (W.chosenStep ε') ≤ ε'

Frieze–Kannan control of the chosen step approximation. By construction chosenStep W ε' = stepify P W for the regularity partition P at quality ε', so the cut-norm difference ‖W − U‖_□ is at most ε'. This is the systematic-error budget of the core term: the a.e. entries of the empirical difference matrix are the sampled values of W − U, whose continuous cut norm the AFKK core compares against.

AFKK cut-guessing apparatus (private)

The proof of guessBlock_integral_le_cutNormDiff follows docs/afkk-cut-guessing.md (= arXiv:2203.07581 §6.2 + Appendix §10; AFKK, JCSS 67 (2003), Lemma 3; Lovász, Large Networks, Lemma 10.7). Everything here is private. The subsections marked (I) hypergeometric moments, (II) product-space McDiarmid MGF, and (III) finite soft-max are self-contained infrastructure, candidates for later extraction.

(H4) ⌈√k⌉₊ arithmetic

(I) Hypergeometric moments of the subsample estimator

Purely finite averages over Finset.powersetCard q Finset.univ — sampling q of k fixed real numbers without replacement. Reusable infrastructure.

Conditioning on a block (Layer 2)

(II) McDiarmid at MGF level on finite product measures

The bounded-differences implementation (coordinate-peeling induction, one application of Hoeffding's lemma per peeled coordinate) lives in Graphon/McDiarmid.lean, packaged as ProbabilityTheory.hasSubgaussianMGF_of_bounded_differences' (arbitrary finite index type) and its Fin n special case. Here we only unpack the HasSubgaussianMGF form back into the integral-form MGF bound (H13b) consumed by the soft-max/assembly layer below.

(III) Finite soft-max

Per-block assembly and rate arithmetic (Layers 2+3+4)

Layer 4 — event packaging (Markov) and the uniform target theorem

theorem Graphon.integrable_freqTerm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) [NeZero k] : MeasureTheory.Integrable (fun (x : Fin k → α) => W.freqTerm ε' k x) (MeasureTheory.Measure.pi fun (x : Fin k) => μ)

The frequency term is integrable: it is bounded by a constant on the finite-measure product space (crude uniform bound freqTerm_le).

theorem Graphon.integrable_coreTerm {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) (ε' : ℝ) (k : ℕ) [NeZero k] : MeasureTheory.Integrable (fun (x : Fin k → α) => W.coreTerm ε' k x) (MeasureTheory.Measure.pi fun (x : Fin k) => μ)

The core term is integrable: it is bounded by 1 on the finite-measure product space (coreTerm_le_one).

theorem Graphon.point_sampling_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.PointSamplingEvent k ε η

The point-sampling half of the First Sampling Lemma (PR #11 target; PROVED). With W-uniform K: for all k ≥ K, the weighted sampled graphon H_{W,x} is within cut distance ε of W outside a bad set of measure ≤ η.

Proof: at accuracy ε' := εη/4, the majorant's expectation is ≤ 2ε' + regularityBound ε'/√k + 1/k + 8·k^{-1/4} < εη for all large k — uniformly in W, since regularityBound is W-free; Markov applied to the nonnegative integrable majorant plus the a.e. domination ae_cutDistance_le_pointSamplingMajorant packages the measurable event set.

Together with rounding_event_of_large_k and sampleGoodMassOn_of_events, this closes first_sampling_lemma (the PR #12 recombination).