Uniform pairs: complements and discrepancy

Between two disjoint vertex sets, every vertex pair is an edge of exactly one of G and Gᶜ, so on nonempty sets the two edge densities sum to one. Consequently an ε-uniform pair of disjoint sets in G is also ε-uniform in Gᶜ. Disjointness is needed: within a single set the diagonal pairs are edges of neither graph.

An ε-uniform pair (s, t) also has small rectangle discrepancy: the number of edges between s' ⊆ s and t' ⊆ t is within ε |s| |t| of d(s, t) |s'| |t'|. Large rectangles are controlled by uniformity itself, and small ones because both counts are then at most |s'| |t'| ≤ ε |s| |t|. Testing against functions with values in [0, 1] instead of indicator functions does not increase the discrepancy (Finset.abs_sum_sum_mul_mul_le_of_forall_subset). Neither bound needs the sets to be disjoint.

Main results

• SimpleGraph.IsUniform.compl: uniformity of disjoint sets passes to the complement graph.
• SimpleGraph.IsUniform.abs_card_interedges_sub_le: rectangle discrepancy of a uniform pair.
• SimpleGraph.IsUniform.abs_sum_sum_mul_sub_le: the same bound for tests with values in [0, 1].

theorem SimpleGraph.IsUniform.compl {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α} [DecidableEq α] (h : G.IsUniform ε s t) (hst : Disjoint s t) : Gᶜ.IsUniform ε s t

An ε-uniform pair of disjoint vertex sets is ε-uniform in the complement graph.

theorem SimpleGraph.isUniform_compl_iff {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α} [DecidableEq α] (hst : Disjoint s t) : Gᶜ.IsUniform ε s t ↔ G.IsUniform ε s t

For disjoint vertex sets, uniformity in G and in Gᶜ coincide.

theorem SimpleGraph.IsUniform.abs_card_interedges_sub_le {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {s t s' t' : Finset α} (h : G.IsUniform ε s t) (hs' : s' ⊆ s) (ht' : t' ⊆ t) : |↑(G.interedges s' t').card - ↑(G.edgeDensity s t) * ↑s'.card * ↑t'.card| ≤ ε * ↑s.card * ↑t.card

Rectangle discrepancy of a uniform pair. If (s, t) is ε-uniform, then for all s' ⊆ s and t' ⊆ t the number of edges between s' and t' is within ε |s| |t| of the count d(s, t) |s'| |t'| predicted by the density of (s, t).

theorem SimpleGraph.IsUniform.abs_sum_sum_mul_sub_le {α : Type u_1} {𝕜 : Type u_2} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α} [DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α} (h : G.IsUniform ε s t) {f g : α → 𝕜} (hf₀ : ∀ x ∈ s, 0 ≤ f x) (hf₁ : ∀ x ∈ s, f x ≤ 1) (hg₀ : ∀ y ∈ t, 0 ≤ g y) (hg₁ : ∀ y ∈ t, g y ≤ 1) : |∑ x ∈ s, ∑ y ∈ t, f x * g y * ((if G.Adj x y then 1 else 0) - ↑(G.edgeDensity s t))| ≤ ε * ↑s.card * ↑t.card

Test-function discrepancy of a uniform pair. If (s, t) is ε-uniform, then testing the deviation of the adjacency indicator from the density d(s, t) against functions f on s and g on t with values in [0, 1] gives at most ε |s| |t|.