The padded vertex exposure of a sampled graph

The finite sampling law sampleGraph W n is defined by its masses, so it does not present the sampled graph as a function of independent coordinates. A bounded-differences inequality needs exactly such a presentation: a product of independent coordinates, together with a bound on how much the estimator moves when one coordinate changes. Changing one sampled vertex position alone is not such a coordinate, because the edges at that vertex also carry their own independent randomness.

The padded exposure supplies the product structure. Each of the n vertices carries its position in the graphon's carrier together with a full row of n independent uniform coins, and the exposure source is the n-fold product of these vertex coordinates. The edge {i, j} reads its coin from one designated row: row max i j, column min i j, and it is present when that coin falls below the graphon value at the two positions. Every coin on or above the diagonal is padding that no edge reads. Since every edge reads a coin carried by one of its endpoints, changing the coordinate of one vertex changes only the pairs at that vertex.

The two results of the file make this a genuine representation of G(n, W):

• the law identification: the exposure source pushed through the exposed graph is the finite sampling law. At fixed positions the event that the exposed graph is a prescribed pattern is a box in the coins, whose uniform product is the conditional mass sampleIntegrand W H;
• the oscillation bound: changing one vertex coordinate moves the ordinary homomorphism density of the exposed graph by at most |V(F)| / n.

Main definitions

• TauCeti.DenseGraphLimits.exposureMeasure — the product source of positions and coin rows;
• TauCeti.DenseGraphLimits.exposedSample — the graph read off an exposure.

Main results

• exposedSample_adj — the designated-row rule for the edges;
• map_exposedSample — the exposure source induces the finite sampling law;
• exposedSample_update_adj_iff — updating one vertex coordinate only changes pairs at it;
• abs_homDensityFin_exposedSample_update_le — the bounded-differences estimate.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §10.1.
• C. Freer, cameronfreer/graphon at commit 6eccca5bbe5c9df46d7129bf59575b8b9b1d6699, Apache-2.0, Graphon/SampleExposure.lean. The padded exposure source, the designated-row convention, the law identification and the q / n oscillation bound are formalized there. The construction here is adapted to Tau Ceti's strict graphon carrier and uses the uniform coin TauCeti.Probability.uniformMeasure 0 1 and the strict comparison of the joint sampler infiniteSampleLaw; the law identification evaluates the mass of a single pattern as a box of coin intervals, and the oscillation bound is derived from a host-graph statement, SimpleGraph.abs_homDensityFin_sub_le_of_adj_iff.

noncomputable def TauCeti.DenseGraphLimits.exposureMeasure {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (n : ℕ) : MeasureTheory.Measure (Fin n → Ω × (Fin n → ℝ))

The exposure source of the n-vertex sampled graph: n independent vertex coordinates, each a position drawn from μ together with a row of n independent uniform coins on the unit interval.

Equations

• TauCeti.DenseGraphLimits.exposureMeasure μ n = MeasureTheory.Measure.pi fun (x : Fin n) => μ.prod (MeasureTheory.Measure.pi fun (x : Fin n) => TauCeti.Probability.uniformMeasure 0 1)

theorem TauCeti.DenseGraphLimits.exposureMeasure_def {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (n : ℕ) : exposureMeasure μ n = MeasureTheory.Measure.pi fun (x : Fin n) => μ.prod (MeasureTheory.Measure.pi fun (x : Fin n) => Probability.uniformMeasure 0 1)

The defining product of the exposure source.

instance TauCeti.DenseGraphLimits.exposureMeasure_isProbabilityMeasure {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : MeasureTheory.IsProbabilityMeasure (exposureMeasure μ n)

@[simp]

theorem TauCeti.DenseGraphLimits.map_fst_exposureMeasure {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (n : ℕ) : MeasureTheory.Measure.map (fun (x : Fin n → Ω × (Fin n → ℝ)) (i : Fin n) => (x i).1) (exposureMeasure μ n) = MeasureTheory.Measure.pi fun (x : Fin n) => μ

The positions of the exposure source are independent with law μ: forgetting the rows of coins maps the exposure source to the product Measure.pi fun _ => μ.

def TauCeti.DenseGraphLimits.exposedSample {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (x : Fin n → Ω × (Fin n → ℝ)) : SimpleGraph (Fin n)

The exposed sampled graph: the pair {i, j} is an edge exactly when the coin in row max i j, column min i j falls below the graphon value at the two positions. Every edge reads a coin carried by one of its endpoints, so changing one vertex coordinate changes only the pairs at that vertex.

Equations

• TauCeti.DenseGraphLimits.exposedSample W x = { Adj := fun (i j : Fin n) => i ≠ j ∧ (x (max i j)).2 (min i j) < W (x i).1 (x j).1, symm := ⋯, loopless := ⋯ }

@[simp]

theorem TauCeti.DenseGraphLimits.exposedSample_adj {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (x : Fin n → Ω × (Fin n → ℝ)) (i j : Fin n) : (exposedSample W x).Adj i j ↔ i ≠ j ∧ (x (max i j)).2 (min i j) < W (x i).1 (x j).1

The designated-row rule. The edge {i, j} of the exposed graph is present exactly when the coin in row max i j, column min i j falls below the graphon value at the two positions.

theorem TauCeti.DenseGraphLimits.measurable_exposedSample {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) : Measurable (exposedSample W)

The exposed graph depends measurably on the exposure.

theorem TauCeti.DenseGraphLimits.exposedSample_update_adj_iff {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (W : Graphon Ω μ) (x : Fin n → Ω × (Fin n → ℝ)) (i : Fin n) (y : Ω × (Fin n → ℝ)) {a b : Fin n} (ha : a ≠ i) (hb : b ≠ i) : (exposedSample W (Function.update x i y)).Adj a b ↔ (exposedSample W x).Adj a b

Updating the coordinate of the vertex i leaves every pair avoiding i unchanged: such a pair reads its positions and its coin from vertices other than i.

@[simp]

theorem TauCeti.DenseGraphLimits.map_exposedSample {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] (W : Graphon Ω μ) (n : ℕ) : MeasureTheory.Measure.map (exposedSample W) (exposureMeasure μ n) = sampleGraph W n

The law identification of the exposure. Pushing the exposure source through the exposed graph gives the finite sampling law G(n, W): the exposure is a representation of the sampled graph by independent vertex coordinates.

theorem TauCeti.DenseGraphLimits.abs_homDensityFin_exposedSample_update_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {V : Type u_2} [Fintype V] (F : SimpleGraph V) (W : Graphon Ω μ) {n : ℕ} (x : Fin n → Ω × (Fin n → ℝ)) (i : Fin n) (y : Ω × (Fin n → ℝ)) : |homDensityFin F (exposedSample W (Function.update x i y)) - homDensityFin F (exposedSample W x)| ≤ ↑(Fintype.card V) / ↑n

The bounded-differences estimate of the exposure. Changing the coordinate of one exposed vertex moves the ordinary homomorphism density of the exposed graph by at most |V(F)| / n.