Rounding the weights of a finite weighted graph

A finite weighted graph is a symmetric [0, 1]-valued matrix together with vertex weights, read as a graphon by Graphon.ofMatrix. This file rounds both weightings onto a grid at a controlled cost in cut distance, so that only finitely many candidates remain on a fixed vertex set.

The two grids are handled quite differently. Edge weights are rounded pointwise: the difference of the two kernels is bounded by the mesh, and so is the cut norm. Vertex weights cannot be rounded pointwise -- they have to keep summing to one -- so all but one of them are rounded down and the remaining vertex absorbs the slack (TauCeti.exists_nat_weights_of_sum_eq_one). Comparing the two weightings then needs a coupling of them, and the one used here (TauCeti.MeasureTheory.shiftCoupling) keeps the matched mass on the diagonal, where the overlaid difference vanishes, and sends the slack to the absorbing vertex; the cost is twice the transferred mass. Two arbitrary weightings are compared through the common weighting that keeps the smaller of the two weights at every vertex but one, which costs twice their ℓ¹ distance.

Main definitions

• TauCeti.DenseGraphLimits.gridValue / TauCeti.DenseGraphLimits.gridIndex -- the grid of multiples of 1 / (N + 1) in [0, 1], and rounding down onto it;
• TauCeti.DenseGraphLimits.gridWeightMeasure -- the probability measure on Fin n whose weights are multiples of 1 / N.

Main results

• TauCeti.DenseGraphLimits.exists_gridValue_cutDist_le -- the edge weights can be taken on the grid of multiples of 1 / (N + 1), at a cost of 1 / (N + 1);
• TauCeti.DenseGraphLimits.cutDist_ofMatrix_le_two_mul_sum_tsub -- transferring vertex weight onto one designated vertex costs at most twice the transferred mass;
• TauCeti.DenseGraphLimits.cutDist_ofMatrix_le_two_mul_sum_abs -- changing the vertex weights arbitrarily costs at most twice their ℓ¹ distance;
• TauCeti.DenseGraphLimits.exists_gridWeightMeasure_cutDist_le -- the vertex weights can be taken on the grid of multiples of 1 / N, at a cost of 2 n / N.

References

• L. Lovász, Large Networks and Graph Limits, AMS Colloquium Publications 60 (2012), §9.2 -- weighted graphs are dense in the space of graphons.

noncomputable def TauCeti.DenseGraphLimits.gridValue (N : ℕ) (k : Fin (N + 2)) : ↑(Set.Icc 0 1)

The point k / (N + 1) of [0, 1]. As k runs over Fin (N + 2) these are the N + 2 multiples of 1 / (N + 1) in [0, 1], a grid of mesh 1 / (N + 1).

Equations

• TauCeti.DenseGraphLimits.gridValue N k = ⟨↑↑k / (↑N + 1), ⋯⟩

@[simp]

theorem TauCeti.DenseGraphLimits.coe_gridValue (N : ℕ) (k : Fin (N + 2)) : ↑(gridValue N k) = ↑↑k / (↑N + 1)

noncomputable def TauCeti.DenseGraphLimits.gridIndex (N : ℕ) (t : ↑(Set.Icc 0 1)) : Fin (N + 2)

The grid point just below a [0, 1] value: the index of ⌊t (N + 1)⌋ / (N + 1).

Equations

• TauCeti.DenseGraphLimits.gridIndex N t = ⟨⌊↑t * (↑N + 1)⌋₊, ⋯⟩

@[simp]

theorem TauCeti.DenseGraphLimits.coe_gridIndex (N : ℕ) (t : ↑(Set.Icc 0 1)) : ↑(gridIndex N t) = ⌊↑t * (↑N + 1)⌋₊

theorem TauCeti.DenseGraphLimits.abs_sub_gridValue_gridIndex_le (N : ℕ) (t : ↑(Set.Icc 0 1)) : |↑t - ↑(gridValue N (gridIndex N t))| ≤ 1 / (↑N + 1)

Rounding to the grid moves a value by at most the mesh 1 / (N + 1).

theorem TauCeti.DenseGraphLimits.exists_gridValue_cutDist_le {κ : Type u_1} [MeasurableSpace κ] [Countable κ] [MeasurableSingletonClass κ] (ν : MeasureTheory.Measure κ) [MeasureTheory.IsProbabilityMeasure ν] (N : ℕ) (b : κ → κ → ↑(Set.Icc 0 1)) (hb : ∀ (i j : κ), b i j = b j i) : ∃ (c : κ → κ → Fin (N + 2)) (hc : ∀ (i j : κ), c i j = c j i), cutDist (Graphon.ofMatrix ν b hb) (Graphon.ofMatrix ν (fun (i j : κ) => gridValue N (c i j)) ⋯) ≤ 1 / (↑N + 1)

Every finite weighted graph is within 1 / (N + 1) in cut distance of one whose block values lie on the grid of multiples of 1 / (N + 1). Only the edge weights move; the vertex weights ν are untouched.

theorem TauCeti.DenseGraphLimits.cutDist_ofMatrix_le_two_mul_sum_tsub {κ : Type u_1} [Fintype κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] {ν ν' : MeasureTheory.Measure κ} {k₀ : κ} [MeasureTheory.IsProbabilityMeasure ν] [MeasureTheory.IsProbabilityMeasure ν'] (hdom : ∀ (k : κ), k ≠ k₀ → ν' {k} ≤ ν {k}) (b : κ → κ → ↑(Set.Icc 0 1)) (hb : ∀ (i j : κ), b i j = b j i) : cutDist (Graphon.ofMatrix ν b hb) (Graphon.ofMatrix ν' b hb) ≤ 2 * (∑ k : κ, (ν {k} - ν' {k})).toReal

Moving vertex weights costs at most twice the moved mass. If ν' is dominated by ν away from one designated vertex k₀ -- so that ν' arises from ν by transferring weight onto k₀ -- then the two finite weighted graphs with the same edge weights b are at cut distance at most twice the transferred mass.

The witnessing coupling is TauCeti.MeasureTheory.shiftCoupling, which keeps the matched mass on the diagonal, where the overlaid difference vanishes, and sends the rest to k₀; the overlaid difference is bounded by one and supported on the pairs with a mismatched coordinate.

theorem TauCeti.DenseGraphLimits.cutDist_ofMatrix_le_two_mul_sum_abs {κ : Type u_1} [Fintype κ] [MeasurableSpace κ] [MeasurableSingletonClass κ] {ν ν' : MeasureTheory.Measure κ} [MeasureTheory.IsProbabilityMeasure ν] [MeasureTheory.IsProbabilityMeasure ν'] (b : κ → κ → ↑(Set.Icc 0 1)) (hb : ∀ (i j : κ), b i j = b j i) : cutDist (Graphon.ofMatrix ν b hb) (Graphon.ofMatrix ν' b hb) ≤ 2 * ∑ k : κ, |ν.real {k} - ν'.real {k}|

Changing the vertex weights of a finite weighted graph costs at most twice their ℓ¹ distance in cut distance: two finite weighted graphs with the same edge weights b and arbitrary vertex weights ν, ν' are at cut distance at most 2 ∑ₖ |ν {k} - ν' {k}|.

noncomputable def TauCeti.DenseGraphLimits.gridWeightMeasure {n N : ℕ} (hN : 0 < N) (w : Fin n → ℕ) (hw : ∑ i : Fin n, w i = N) : MeasureTheory.Measure (Fin n)

The probability measure on Fin n whose weights are the multiples w i / N of 1 / N.

Equations

• TauCeti.DenseGraphLimits.gridWeightMeasure hN w hw = (PMF.ofFintype (fun (i : Fin n) => ↑(w i) / ↑N) ⋯).toMeasure

instance TauCeti.DenseGraphLimits.instIsProbabilityMeasureFinGridWeightMeasure {n N : ℕ} (hN : 0 < N) (w : Fin n → ℕ) (hw : ∑ i : Fin n, w i = N) : MeasureTheory.IsProbabilityMeasure (gridWeightMeasure hN w hw)

Weights on the grid of multiples of 1 / N that sum to N make gridWeightMeasure a probability measure, so that a matrix over them is a graphon by typeclass synthesis alone.

@[simp]

theorem TauCeti.DenseGraphLimits.gridWeightMeasure_apply_singleton {n N : ℕ} (hN : 0 < N) (w : Fin n → ℕ) (hw : ∑ i : Fin n, w i = N) (i : Fin n) : (gridWeightMeasure hN w hw) {i} = ↑(w i) / ↑N

theorem TauCeti.DenseGraphLimits.exists_gridWeightMeasure_cutDist_le {n N : ℕ} [NeZero n] (hN : 0 < N) (ν : MeasureTheory.Measure (Fin n)) [MeasureTheory.IsProbabilityMeasure ν] (b : Fin n → Fin n → ↑(Set.Icc 0 1)) (hb : ∀ (i j : Fin n), b i j = b j i) : ∃ (w : Fin n → ℕ) (hw : ∑ i : Fin n, w i = N), cutDist (Graphon.ofMatrix ν b hb) (Graphon.ofMatrix (gridWeightMeasure hN w hw) b hb) ≤ 2 * ↑n / ↑N

Every finite weighted graph is close in cut distance to one whose vertex weights are multiples of 1 / N. Rounding every weight but one down to the grid and letting the remaining vertex absorb the slack moves at most n / N of the mass, and each unit of moved mass costs at most two in cut distance.