Padded vertex exposure and the fixed-F hom-density concentration tail (issue #72, item 1)

The one-stage padded vertex exposure of the W-random graph G(k, W): each sampled vertex carries its position together with a full padded row of k edge coins, so that the whole sample is a point of the finite i.i.d. product Fin k → α × (Fin k → ℝ) — exactly the shape consumed by the bounded-differences MGF bound of Graphon/McDiarmid.lean. Edge {i, j} reads its coin from row max i j, column min i j; unused entries are harmless padding.

• InfiniteGraph.exposedSample — the exposed sampled graph, a measurable SimpleGraph (Fin k)-valued function of the exposure state;
• InfiniteGraph.map_exposedSample — the law identification: pushing the exposure source forward along exposedSample W k gives exactly the finite sample law samplePMF W k (upper events factor into per-edge coin cylinders; Möbius inversion via Graphon.upperSum_injective closes, as in InfiniteGraph.map_sampleInfinite_restrictFin);
• InfiniteGraph.abs_homDensity_exposedSample_update_le — the oscillation bound: updating a single exposed vertex moves the hom-density of a fixed F on q vertices by at most q / k (only vertex maps whose range contains the updated vertex can change status).

Feeding the oscillation bound to ProbabilityTheory.hasSubgaussianMGF_of_bounded_differences and moving the center from the sample mean to homDensity F W by the public collision estimate (GraphonSpace.abs_integral_homDensityCoord_empiricalMixing_sub_le, specialized to sampleExchangeableLaw W) yields the public tail (issue #72 item 1, toward Lovász Cor 10.4; consumed by the Borel–Cantelli assembly of issue #71):

• Graphon.measureReal_abs_homDensity_sampled_sub_le — exponential concentration of the sampled hom-density at fixed F: for 2q² ≤ εk, the samplePMF W k-probability that |t(F, G(k,W)) − t(F,W)| ≥ ε is at most 2 exp(−ε²k / (2q²));
• InfiniteGraph.samplerSource_abs_homDensity_restrictFin_sub_le — the same tail for the explicit sampler restrictFin k ∘ sampleInfinite W;
• InfiniteGraph.tsum_samplerSource_homDensity_tail_ne_top — the summability bridge: for each fixed ε > 0 the tail masses at sizes n + 1 have finite total, in the exact shape consumed by Borel–Cantelli (MeasureTheory.ae_eventually_notMem).

The exposure source

noncomputable def InfiniteGraph.coinRowMeasure (k : ℕ) : MeasureTheory.Measure (Fin k → ℝ)

One padded coin row: k i.i.d. uniforms on [0, 1].

Equations

• InfiniteGraph.coinRowMeasure k = MeasureTheory.Measure.pi fun (x : Fin k) => InfiniteGraph.uniform01

instance InfiniteGraph.instIsProbabilityMeasureForallFinRealCoinRowMeasure (k : ℕ) : MeasureTheory.IsProbabilityMeasure (coinRowMeasure k)

noncomputable def InfiniteGraph.exposureVertexMeasure {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (k : ℕ) : MeasureTheory.Measure (α × (Fin k → ℝ))

The per-vertex exposure state: an i.i.d. position with law μ together with an independent full padded coin row.

Equations

• InfiniteGraph.exposureVertexMeasure μ k = μ.prod (InfiniteGraph.coinRowMeasure k)

instance InfiniteGraph.instIsProbabilityMeasureProdForallFinRealExposureVertexMeasure {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) : MeasureTheory.IsProbabilityMeasure (exposureVertexMeasure μ k)

noncomputable def InfiniteGraph.exposureMeasure {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) (k : ℕ) : MeasureTheory.Measure (Fin k → α × (Fin k → ℝ))

The exposure source: k i.i.d. exposed vertices — a finite i.i.d. product, the state space of the bounded-differences inequality.

Equations

• InfiniteGraph.exposureMeasure μ k = MeasureTheory.Measure.pi fun (x : Fin k) => InfiniteGraph.exposureVertexMeasure μ k

instance InfiniteGraph.instIsProbabilityMeasureForallFinProdForallRealExposureMeasure {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) : MeasureTheory.IsProbabilityMeasure (exposureMeasure μ k)

The exposed sampled graph

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

The exposed sampled graph: include the edge {i, j} exactly when the coin in row max i j, column min i j falls below the clamped graphon value at the Quot.out-representative endpoint positions (the same orientation convention as sampleInfinite/sampleIntegrand, which eliminates a.e.-symmetry juggling in the law identification). Symmetric because max, min, and s(i, j) are; irreflexive by the i ≠ j conjunct.

Equations

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

theorem InfiniteGraph.exposedSample_adj {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) (k : ℕ) (x : Fin k → α × (Fin k → ℝ)) (i j : Fin k) : (exposedSample W k x).Adj i j ↔ i ≠ j ∧ (x (max i j)).2 (min i j) ≤ clampedRep W ((x (Quot.out s(i, j)).1).1, (x (Quot.out s(i, j)).2).1)

The adjacency of the exposed sample, unfolded.

theorem InfiniteGraph.measurable_exposedSample {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) (k : ℕ) : Measurable (exposedSample W k)

The exposed sample is measurable in the exposure state: each adjacency is a measurable comparison of coordinate evaluations.

The law identification

theorem InfiniteGraph.map_exposedSample {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} (W : Graphon α μ) [MeasureTheory.IsProbabilityMeasure μ] (k : ℕ) : MeasureTheory.Measure.map (exposedSample W k) (exposureMeasure μ k) = (W.samplePMF k).toMeasure

The law identification (issue #72, item 1, commit 2): the exposed sampled graph of the exposure source has law exactly samplePMF W k — the padded coin rows are integrated out. Singleton masses via Measure.ext_of_singleton, then Möbius inversion via Graphon.upperSum_injective on the upper-event masses.

The oscillation bound

theorem InfiniteGraph.measurable_homDensity_exposedSample {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) {k : ℕ} [NeZero k] {q : ℕ} (F : SimpleGraph (Fin q)) [DecidableRel F.Adj] : Measurable fun (x : Fin k → α × (Fin k → ℝ)) => Graphon.homDensity F (Graphon.ofSimpleGraphOn (exposedSample W k x))

The hom-density of the embedded exposed sample is a measurable function of the exposure state (any function out of the countable discrete graph space is).

theorem InfiniteGraph.abs_homDensity_exposedSample_update_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) {k : ℕ} [NeZero k] {q : ℕ} (F : SimpleGraph (Fin q)) [DecidableRel F.Adj] (x : Fin k → α × (Fin k → ℝ)) (i : Fin k) (b : α × (Fin k → ℝ)) : |Graphon.homDensity F (Graphon.ofSimpleGraphOn (exposedSample W k (Function.update x i b))) - Graphon.homDensity F (Graphon.ofSimpleGraphOn (exposedSample W k x))| ≤ ↑q / ↑k

The oscillation bound (issue #72, item 1, commit 2): updating one exposed vertex moves the hom-density of a fixed F on q vertices by at most q / k — only the at most q * k ^ (q - 1) vertex maps whose range contains the updated vertex can change upper-event status (homDensity_ofSimpleGraphOn). This is the bounded-differences hypothesis of ProbabilityTheory.hasSubgaussianMGF_of_bounded_differences, stated for the exact function fed to it.

The fixed-F exponential concentration tail

theorem Graphon.measureReal_abs_homDensity_sampled_sub_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) {q : ℕ} (F : SimpleGraph (Fin q)) [DecidableRel F.Adj] {ε : ℝ} (hε : 0 < ε) {k : ℕ} [NeZero k] (hk : 2 * ↑q ^ 2 ≤ ε * ↑k) : (W.samplePMF k).toMeasure.real {G : SimpleGraph (Fin k) | ε ≤ |homDensity F (ofSimpleGraphOn G) - homDensity F W|} ≤ 2 * Real.exp (-(ε ^ 2 * ↑k) / (2 * ↑q ^ 2))

Exponential concentration of the sampled hom-density, fixed F (issue #72, item 1): an eventual fixed-F Corollary 10.4-style bound — not the exact manuscript Corollary 10.4: this theorem assumes 2q² ≤ εk (which holds eventually in k for fixed F and ε, and makes the collision bias q²/k at most ε/2) and carries a different, stronger exponent. For a fixed graph F on q vertices, the probability under the sample law G(k, W) that the hom-density of F deviates from t(F, W) by at least ε is at most 2 exp(−ε²k / (2q²)).

Both tails come from ProbabilityTheory.hasSubgaussianMGF_of_bounded_differences applied to the padded vertex exposure (variance proxy q²/(4k)), centered at the sample mean; the center moves to t(F, W) by the collision estimate. For q = 0 the density is constantly 1 and the tail set is empty.

theorem InfiniteGraph.samplerSource_abs_homDensity_restrictFin_sub_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) {q : ℕ} (F : SimpleGraph (Fin q)) [DecidableRel F.Adj] {ε : ℝ} (hε : 0 < ε) {k : ℕ} [NeZero k] (hk : 2 * ↑q ^ 2 ≤ ε * ↑k) : (samplerSource μ).real {ω : (ℕ → α) × (EdgeIndex → ℝ) | ε ≤ |Graphon.homDensity F (Graphon.ofSimpleGraphOn (restrictFin k (sampleInfinite W ω))) - Graphon.homDensity F W|} ≤ 2 * Real.exp (-(ε ^ 2 * ↑k) / (2 * ↑q ^ 2))

The fixed-F tail for the explicit sampler: the same bound for the event that the hom-density of the first-k-vertices restriction of the sampled infinite graph deviates from t(F, W), via the finite marginal identification map_sampleInfinite_restrictFin.

theorem InfiniteGraph.tsum_samplerSource_homDensity_tail_ne_top {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ] [StandardBorelSpace α] [MeasureTheory.NullSingletonClass μ] (W : Graphon α μ) {q : ℕ} (F : SimpleGraph (Fin q)) [DecidableRel F.Adj] {ε : ℝ} (hε : 0 < ε) : ∑' (n : ℕ), (samplerSource μ) {ω : (ℕ → α) × (EdgeIndex → ℝ) | ε ≤ |Graphon.homDensity F (Graphon.ofSimpleGraphOn (restrictFin (n + 1) (sampleInfinite W ω))) - Graphon.homDensity F W|} ≠ ⊤

The summability bridge (issue #72, item 1; consumed by the Borel–Cantelli assembly of issue #71 via MeasureTheory.ae_eventually_notMem): for each fixed ε > 0, the total sampler-source mass of the fixed-F deviation events at sizes n + 1 is finite — finitely many initial terms are bounded by 1, the rest decay geometrically.