Degree-count marks in the cyclic bridge identity

Finitely many prescribed outdegree counts are invariant under rotating the Łukasiewicz word. The weighted cycle identity therefore restricts to these marks, without requiring positive mass or introducing another finite-tree carrier. Repeated degrees are allowed; incompatible prescribed counts simply give zero.

def BGW.wordDegreeCount (x : List ℤ) (k : ℕ) : ℕ

The number of steps corresponding to offspring count k. In particular, k = 0 counts steps equal to -1, hence leaves on a tree word.

Equations

• BGW.wordDegreeCount x k = List.count (↑k - 1) x

@[simp]

theorem BGW.wordDegreeCount_rotate (x : List ℤ) (i k : ℕ) : wordDegreeCount (x.rotate i) k = wordDegreeCount x k

@[simp]

theorem BGW.wordDegreeCount_stepWord {n : ℕ} (ω : Fin n → ℕ) (k : ℕ) : wordDegreeCount (stepWord ω) k = List.count k (List.ofFn ω)

def BGW.PlaneTree.degreeCount (t : PlaneTree) (k : ℕ) : ℕ

Number of vertices whose outdegree is k, counting every DFS occurrence.

Equations

• t.degreeCount k = List.count k t.degrees

@[simp]

theorem BGW.PlaneTree.wordDegreeCount_increments (t : PlaneTree) (k : ℕ) : wordDegreeCount t.increments k = t.degreeCount k

theorem BGW.PlaneTree.degreeCount_le_size (t : PlaneTree) (k : ℕ) : t.degreeCount k ≤ t.size

theorem BGW.PlaneTree.natCast_mul_tsum_weight_degreeCounts (p : ℕ → ENNReal) (n r : ℕ) (ks cs : Fin r → ℕ) : (↑n * ∑' (t : { t : PlaneTree // t.size = n }), weight p ↑t * if ∀ (j : Fin r), (↑t).degreeCount (ks j) = cs j then 1 else 0) = ∑' (ω : Fin n → ℕ), (countBridges n ∩ {ω : Fin n → ℕ | ∀ (j : Fin r), List.count (ks j) (List.ofFn ω) = cs j}).indicator (fun (ω : Fin n → ℕ) => ∏ i : Fin n, p (ω i)) ω

Weighted Kemperman identity with finitely many prescribed degree counts. The marks may repeat a degree, and no assumption on the weights or size is needed.