Counting a dart set by tail and by head

The bookkeeping that turns WalkDart.sum_two_darts_fixed — the operator form of "the walk crosses F at step k and again at step l" — into something Mixing.mixing_sq can estimate.

Two counts of a dart set are needed. dartCount F v counts the F-darts leaving v, and headCount F z counts those arriving at z. Both sum to F.card, and each is at most the degree. The first is the function whose stepIter the second crossing sees; the second is the measure the first crossing leaves behind.

Main definitions

• RegGraph.dartCount, RegGraph.headCount

Main results

• RegGraph.sum_dartCount, RegGraph.sum_headCount — both count F
• RegGraph.dartCount_le, RegGraph.headCount_le — at most the degree
• RegGraph.sum_indicator_nbr — a sum over F-darts of a function of the head is a sum over vertices weighted by headCount
• RegGraph.step_sum, RegGraph.stepIter_sum — the walk operator is linear over finite sums
• RegGraph.sum_indicator_dartCount, RegGraph.sum_indicator_mul — indicator sums collapse to the two counts
• RegGraph.sum_two_crossings — two crossings of F, in operator form
• RegGraph.sum_headCount_stepIter_le — the correlation bound: two crossings t steps apart are independent up to lam ^ t * deg * |F|
• geom_sum_le_inv, sum_pairs_geom_le — summing that over all position pairs costs only m / (1 - lam)
• RegGraph.sum_pairs_le — the second moment: all pairs of crossings together
• card_sq_eq_add_two_mul_pairs — a squared count is the count plus twice the ordered pairs
• card_filter_eq_sum_prod, sum_pairs_eq_sum_Ico — index bookkeeping for the second moment

Geometric sums

theorem Complexity.geom_sum_le_inv {lam : ℝ} (h0 : 0 ≤ lam) (h1 : lam < 1) (n : ℕ) : ∑ i ∈ Finset.range n, lam ^ i ≤ 1 / (1 - lam)

A truncated geometric series is bounded by its limit.

theorem Complexity.sum_pairs_geom_le {lam : ℝ} (h0 : 0 ≤ lam) (h1 : lam < 1) (m : ℕ) : ∑ k ∈ Finset.range m, ∑ l ∈ Finset.Ico (k + 1) m, lam ^ (l - k - 1) ≤ ↑m * (1 / (1 - lam))

Summed over all pairs of positions, the separation weights lam ^ (l-k-1) contribute at most m / (1 - lam).

Squares and ordered pairs

theorem Complexity.card_sq_eq_add_two_mul_pairs {ι : Type u_1} [LinearOrder ι] [DecidableEq ι] (S : Finset ι) : S.card ^ 2 = S.card + 2 * {p ∈ S ×ˢ S | p.1 < p.2}.card

The square of a count is the count plus twice the ordered pairs. This is how ∑ N ^ 2 in the second-moment method becomes a sum over pairs of crossings, which is what the correlation bound estimates.

theorem Complexity.card_filter_eq_sum_prod {ι : Type u_1} [Fintype ι] (P Q : ι → Prop) [DecidablePred P] [DecidablePred Q] : ↑{i : ι | P i ∧ Q i}.card = ∑ i : ι, (if P i then 1 else 0) * if Q i then 1 else 0

A count of a conjunction is a sum of products of indicators.

theorem Complexity.sum_pairs_eq_sum_Ico {M : Type u_1} [AddCommMonoid M] (T : ℕ) (f : ℕ × ℕ → M) : ∑ p ∈ Finset.range T ×ˢ Finset.range T with p.1 < p.2, f p = ∑ k ∈ Finset.range T, ∑ l ∈ Finset.Ico (k + 1) T, f (k, l)

A sum over ordered pairs below T, as an iterated sum.

Linearity of the walk operator

theorem Complexity.RegGraph.step_sum (G : RegGraph) {ι : Type u_1} (s : Finset ι) (f : ι → G.V → ℝ) (v : G.V) : G.step (fun (w : G.V) => ∑ i ∈ s, f i w) v = ∑ i ∈ s, G.step (f i) v

theorem Complexity.RegGraph.stepIter_sum (G : RegGraph) {ι : Type u_1} (s : Finset ι) (f : ι → G.V → ℝ) (t : ℕ) (v : G.V) : G.stepIter t (fun (w : G.V) => ∑ i ∈ s, f i w) v = ∑ i ∈ s, G.stepIter t (f i) v

def Complexity.RegGraph.dartCount (G : RegGraph) (F : Finset (G.V × G.D)) (v : G.V) : ℕ

How many darts of F leave v.

Equations

• G.dartCount F v = {p ∈ F | p.1 = v}.card

def Complexity.RegGraph.headCount (G : RegGraph) (F : Finset (G.V × G.D)) (z : G.V) : ℕ

How many darts of F arrive at z.

Equations

• G.headCount F z = {p ∈ F | G.nbr p.1 p.2 = z}.card

theorem Complexity.RegGraph.sum_dartCount (G : RegGraph) (F : Finset (G.V × G.D)) : ∑ v : G.V, G.dartCount F v = F.card

theorem Complexity.RegGraph.sum_headCount (G : RegGraph) (F : Finset (G.V × G.D)) : ∑ z : G.V, G.headCount F z = F.card

theorem Complexity.RegGraph.dartCount_le (G : RegGraph) (F : Finset (G.V × G.D)) (v : G.V) : G.dartCount F v ≤ G.deg

theorem Complexity.RegGraph.headCount_le (G : RegGraph) (F : Finset (G.V × G.D)) (z : G.V) : G.headCount F z ≤ G.deg

The darts arriving at z correspond, under reversal, to the darts leaving z, so there are at most deg of them.

theorem Complexity.RegGraph.sum_indicator_nbr (G : RegGraph) (F : Finset (G.V × G.D)) (h : G.V → ℝ) : ∑ p ∈ F, h (G.nbr p.1 p.2) = ∑ z : G.V, ↑(G.headCount F z) * h z

Summing a function of a dart's head over F is summing over vertices with the multiplicity headCount.

Indicator sums

theorem Complexity.RegGraph.sum_indicator_dartCount (G : RegGraph) (F : Finset (G.V × G.D)) (z : G.V) : (∑ b : G.D, if (z, b) ∈ F then 1 else 0) = ↑(G.dartCount F z)

Summing the F-indicator over the labels at a fixed vertex counts the F-darts there.

theorem Complexity.RegGraph.sum_indicator_mul (G : RegGraph) (F : Finset (G.V × G.D)) (φ : G.V → ℝ) : ∑ a : G.D, ∑ y : G.V, (if (y, a) ∈ F then 1 else 0) * φ (G.nbr y a) = ∑ p ∈ F, φ (G.nbr p.1 p.2)

Summing an F-weighted function of a dart's head over all darts is summing it over F.

The two-crossing identity

theorem Complexity.RegGraph.sum_two_crossings (G : RegGraph) (F : Finset (G.V × G.D)) {k l m : ℕ} (hkl : k < l) (hl : l < m) : (∑ x : G.V, ∑ r : Fin m → G.D, (if (G.walkAt m x r k, r ⟨k, ⋯⟩) ∈ F then 1 else 0) * if (G.walkAt m x r l, r ⟨l, hl⟩) ∈ F then 1 else 0) = ↑G.deg ^ (m - 2) * ∑ z : G.V, ↑(G.headCount F z) * G.stepIter (l - k - 1) (fun (w : G.V) => ↑(G.dartCount F w)) z

Two crossings, in operator form. Summed over all starts and all label sequences, the walks that cross F at step k and again at step l are counted by the walk operator applied to the dart counts: the first crossing leaves the measure headCount, and the second is seen through l - k - 1 steps of the walk. Mixing.mixing_sq estimates exactly this expression.

Bounding the correlation

theorem Complexity.RegGraph.sum_sq_headCount_le (G : RegGraph) (F : Finset (G.V × G.D)) : ∑ z : G.V, ↑(G.headCount F z) ^ 2 ≤ ↑G.deg * ↑F.card

The variance of a dart count is at most deg * |F|, since no vertex carries more than deg darts of F.

theorem Complexity.RegGraph.sum_sq_dartCount_le (G : RegGraph) (F : Finset (G.V × G.D)) : ∑ v : G.V, ↑(G.dartCount F v) ^ 2 ≤ ↑G.deg * ↑F.card

theorem Complexity.RegGraph.sum_headCount_stepIter_le (G : RegGraph) (F : Finset (G.V × G.D)) {lam : ℝ} (hlam : 0 ≤ lam) (hspec : G.SpectralBound lam) (hn : 0 < G.order) (t : ℕ) : ∑ z : G.V, ↑(G.headCount F z) * G.stepIter t (fun (w : G.V) => ↑(G.dartCount F w)) z ≤ ↑F.card * ↑F.card / ↑G.order + lam ^ t * (↑G.deg * ↑F.card)

The correlation bound. On a graph with spectral bound lam, two crossings of F separated by t steps are almost independent: the operator expression exceeds the independent value |F|² / n by at most lam ^ t * deg * |F|.

theorem Complexity.RegGraph.sum_pairs_le (G : RegGraph) (F : Finset (G.V × G.D)) {lam : ℝ} (hlam0 : 0 ≤ lam) (hlam1 : lam < 1) (hspec : G.SpectralBound lam) (hn : 0 < G.order) (m : ℕ) (C : ℕ → ℕ → ℝ) (hC : ∀ k ∈ Finset.range m, ∀ l ∈ Finset.Ico (k + 1) m, C k l = ∑ z : G.V, ↑(G.headCount F z) * G.stepIter (l - k - 1) (fun (w : G.V) => ↑(G.dartCount F w)) z) : ∑ k ∈ Finset.range m, ∑ l ∈ Finset.Ico (k + 1) m, C k l ≤ ↑m * ↑m * (↑F.card * ↑F.card / ↑G.order) + ↑m * (1 / (1 - lam)) * (↑G.deg * ↑F.card)

The second moment. Summed over every pair of positions, the two-crossing correlations exceed the independent value by at most m / (1 - lam) times deg * |F|. The counts are supplied abstractly as C, since writing the concrete one inside a sum would need the position bounds pointwise.