Cyclic indicators (Definition def:indicators)

Source lines 679–696 (DFS sequence, ζ, eq:fringe) and 735–764 (Section 2.3).

For a mark G (a {0,1}-valued function on finite plane trees, here a predicate G : PlaneTree → Prop), a cutoff M ∈ ℕ ∪ {∞} (here M : ℕ∞) and a finite sequence 𝐱 = (x_1, …, x_n) of integers (a List ℤ):

• Cyclic.firstIndicator G M 𝐱 = I_1^{(M)}(𝐱): it is 1 iff ζ(𝐱) ≤ M (in particular ζ(𝐱) < ∞) and G(T(x_1, …, x_{ζ(𝐱)})) = 1, and 0 otherwise (Cyclic.FirstMarked);
• Cyclic.shiftIndicator G M 𝐱 i = I_{i+1}^{(M)}(𝐱) = I_1^{(M)}(x_{i+1}, …, x_n, x_1, …, x_i) (0-based shifts: the paper's I_i is our shiftIndicator … (i - 1));
• Cyclic.cyclicSum G M 𝐱 = ∑_{i=1}^{n} I_i^{(M)}(𝐱).

We prove the two cases of the definition (firstIndicator_of_zeta_eq_none, firstIndicator_of_lt_zeta, firstIndicator_of_zeta_le), the Boolean range, locality in the first M entries (firstIndicator_take, firstIndicator_congr_take), monotonicity in the cutoff, the infinite cutoff (firstIndicator_top), invariance of the cyclic sum under cyclic shifts (cyclicSum_rotate, part of B04), and the counting identity of source lines 758–760: ∑_i I_i^{(M)}(𝐱(T)) is the number of vertices v with |T_v| ≤ M and G(T_v) = 1 (cyclicSum_dfsSeq); for M ≥ |T| it is markCount G T (cyclicSum_dfsSeq_of_le).

We also prove U05 (source lines 914–920, 960–969): a proper fringe subtree has strictly fewer vertices (PlaneTree.vertexCount_fringeTrees_lt), so two marks forcing the same size cannot hold at a vertex and at a proper descendant (PlaneTree.not_forced_size_nested).

theorem PoissonDeclumping.Lukasiewicz.zeta_take_eq_some_iff {x : List ℤ} {M m : ℕ} : zeta (List.take M x) = some m ↔ zeta x = some m ∧ m ≤ M

ζ(x_1, …, x_M) = m iff ζ(𝐱) = m ≤ M: the first passage time is local.

theorem PoissonDeclumping.PlaneTree.zeta_eq_of_ofSeq_eq_some {x : List ℤ} {T : PlaneTree} (h : ofSeq x = some T) : Lukasiewicz.zeta x = some T.vertexCount

If T(𝐱) = T, then ζ(𝐱) = |T|.

theorem PoissonDeclumping.PlaneTree.ofSeq_take_of_zeta_eq {x : List ℤ} {m M : ℕ} (hz : Lukasiewicz.zeta x = some m) (hm : m ≤ M) : ofSeq (List.take M x) = ofSeq x

T(x_1, …, x_M) = T(𝐱) as soon as ζ(𝐱) ≤ M.

theorem PoissonDeclumping.PlaneTree.vertexCount_fringeTrees_add_le (T : PlaneTree) (i : ℕ) (hi : i < T.fringeTrees.length) : T.fringeTrees[i].vertexCount + i ≤ T.vertexCount

The fringe subtree at the i-th vertex (DFS order, 0-indexed) has at most |T| - i vertices.

theorem PoissonDeclumping.PlaneTree.vertexCount_fringeTrees_lt (T : PlaneTree) {i : ℕ} (hi : i < T.fringeTrees.length) (h1 : 1 ≤ i) : T.fringeTrees[i].vertexCount < T.vertexCount

U05: a proper fringe subtree (at a vertex u_{i+1} with i ≥ 1, i.e. not the root) has strictly fewer vertices than the tree.

theorem PoissonDeclumping.PlaneTree.vertexCount_le_of_mem_fringeTrees {T U : PlaneTree} (hU : U ∈ T.fringeTrees) : U.vertexCount ≤ T.vertexCount

theorem PoissonDeclumping.PlaneTree.fringeTrees_getElem_zero (T : PlaneTree) (h : 0 < T.fringeTrees.length) : T.fringeTrees[0] = T

The fringe subtree at the root is the tree itself.

theorem PoissonDeclumping.PlaneTree.not_forced_size_nested {G₁ G₂ : PlaneTree → Prop} {k : ℕ} (h₁ : ∀ (T : PlaneTree), G₁ T → T.vertexCount = k) (h₂ : ∀ (T : PlaneTree), G₂ T → T.vertexCount = k) (T : PlaneTree) {i : ℕ} (hi : i < T.fringeTrees.length) (h1 : 1 ≤ i) : ¬(G₁ T ∧ G₂ T.fringeTrees[i])

U05: two nested marks forcing the same size cannot both hold at the root and at a proper fringe subtree.

def PoissonDeclumping.Cyclic.FirstMarked (G : PlaneTree → Prop) (M : ℕ∞) (x : List ℤ) : Prop

Definition def:indicators: I_1^{(M)}(𝐱) = 1 iff ζ(𝐱) ≤ M (in particular ζ(𝐱) < ∞) and G(T(x_1, …, x_{ζ(𝐱)})) = 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def PoissonDeclumping.Cyclic.firstIndicator (G : PlaneTree → Prop) (M : ℕ∞) (x : List ℤ) : ℕ

Definition def:indicators: the truncated indicator I_1^{(M)}(𝐱) ∈ {0, 1}.

Equations

• PoissonDeclumping.Cyclic.firstIndicator G M x = if PoissonDeclumping.Cyclic.FirstMarked G M x then 1 else 0

noncomputable def PoissonDeclumping.Cyclic.shiftIndicator (G : PlaneTree → Prop) (M : ℕ∞) (x : List ℤ) (i : ℕ) : ℕ

Definition def:indicators: the cyclically shifted indicator. With 0-based shifts, shiftIndicator G M 𝐱 i = I_{i+1}^{(M)}(𝐱) = I_1^{(M)}(x_{i+1}, …, x_n, x_1, …, x_i).

Equations

• PoissonDeclumping.Cyclic.shiftIndicator G M x i = PoissonDeclumping.Cyclic.firstIndicator G M (x.rotate i)

noncomputable def PoissonDeclumping.Cyclic.cyclicSum (G : PlaneTree → Prop) (M : ℕ∞) (x : List ℤ) : ℕ

∑_{i=1}^{n} I_i^{(M)}(𝐱) for a sequence 𝐱 of length n.

Equations

• PoissonDeclumping.Cyclic.cyclicSum G M x = ∑ i ∈ Finset.range x.length, PoissonDeclumping.Cyclic.shiftIndicator G M x i

theorem PoissonDeclumping.Cyclic.firstIndicator_eq_one_iff {G : PlaneTree → Prop} {M : ℕ∞} {x : List ℤ} : firstIndicator G M x = 1 ↔ FirstMarked G M x

theorem PoissonDeclumping.Cyclic.firstIndicator_eq_zero_iff {G : PlaneTree → Prop} {M : ℕ∞} {x : List ℤ} : firstIndicator G M x = 0 ↔ ¬FirstMarked G M x

theorem PoissonDeclumping.Cyclic.firstIndicator_eq_zero_or_eq_one (G : PlaneTree → Prop) (M : ℕ∞) (x : List ℤ) : firstIndicator G M x = 0 ∨ firstIndicator G M x = 1

Boolean range of I_1^{(M)}.

theorem PoissonDeclumping.Cyclic.firstIndicator_le_one (G : PlaneTree → Prop) (M : ℕ∞) (x : List ℤ) : firstIndicator G M x ≤ 1

theorem PoissonDeclumping.Cyclic.shiftIndicator_eq_zero_or_eq_one (G : PlaneTree → Prop) (M : ℕ∞) (x : List ℤ) (i : ℕ) : shiftIndicator G M x i = 0 ∨ shiftIndicator G M x i = 1

Boolean range of I_i^{(M)}.

theorem PoissonDeclumping.Cyclic.firstIndicator_of_zeta_eq_none {G : PlaneTree → Prop} {M : ℕ∞} {x : List ℤ} (h : Lukasiewicz.zeta x = none) : firstIndicator G M x = 0

First case of Definition def:indicators: ζ(𝐱) = ∞.

theorem PoissonDeclumping.Cyclic.firstIndicator_of_lt_zeta {G : PlaneTree → Prop} {M : ℕ∞} {x : List ℤ} {m : ℕ} (h : Lukasiewicz.zeta x = some m) (hM : M < ↑m) : firstIndicator G M x = 0

First case of Definition def:indicators: ζ(𝐱) > M.

theorem PoissonDeclumping.Cyclic.firstIndicator_of_zeta_le {G : PlaneTree → Prop} {M : ℕ∞} {x : List ℤ} {m : ℕ} {T : PlaneTree} [Decidable (G T)] (h : Lukasiewicz.zeta x = some m) (hM : ↑m ≤ M) (hT : T.dfsSeq = List.take m x) : firstIndicator G M x = if G T then 1 else 0

Second case of Definition def:indicators: if ζ(𝐱) = m ≤ M and T is the tree whose DFS sequence is (x_1, …, x_m), then I_1^{(M)}(𝐱) = G(T).

theorem PoissonDeclumping.Cyclic.firstMarked_iff {G : PlaneTree → Prop} {M : ℕ∞} {x : List ℤ} : FirstMarked G M x ↔ ∃ (T : PlaneTree), PlaneTree.ofSeq x = some T ∧ ↑T.vertexCount ≤ M ∧ G T

I_1^{(M)}(𝐱) = 1 iff the tree T(𝐱) is defined, has at most M vertices and is marked.

theorem PoissonDeclumping.Cyclic.FirstMarked.mono {G : PlaneTree → Prop} {M M' : ℕ∞} {x : List ℤ} (h : FirstMarked G M x) (hMM' : M ≤ M') : FirstMarked G M' x

Monotonicity of I_1^{(M)} in the cutoff.

theorem PoissonDeclumping.Cyclic.firstIndicator_mono {G : PlaneTree → Prop} {M M' : ℕ∞} {x : List ℤ} (hMM' : M ≤ M') : firstIndicator G M x ≤ firstIndicator G M' x

theorem PoissonDeclumping.Cyclic.monotone_firstIndicator (G : PlaneTree → Prop) (x : List ℤ) : Monotone fun (M : ℕ∞) => firstIndicator G M x

theorem PoissonDeclumping.Cyclic.shiftIndicator_mono {G : PlaneTree → Prop} {M M' : ℕ∞} {x : List ℤ} (hMM' : M ≤ M') (i : ℕ) : shiftIndicator G M x i ≤ shiftIndicator G M' x i

theorem PoissonDeclumping.Cyclic.cyclicSum_mono {G : PlaneTree → Prop} {M M' : ℕ∞} {x : List ℤ} (hMM' : M ≤ M') : cyclicSum G M x ≤ cyclicSum G M' x

theorem PoissonDeclumping.Cyclic.firstMarked_take_iff {G : PlaneTree → Prop} {x : List ℤ} {M : ℕ} : FirstMarked G (↑M) (List.take M x) ↔ FirstMarked G (↑M) x

Locality: I_1^{(M)}(𝐱) only depends on x_1, …, x_M.

theorem PoissonDeclumping.Cyclic.firstIndicator_take (G : PlaneTree → Prop) (M : ℕ) (x : List ℤ) : firstIndicator G (↑M) (List.take M x) = firstIndicator G (↑M) x

theorem PoissonDeclumping.Cyclic.firstIndicator_congr_take {G : PlaneTree → Prop} {x y : List ℤ} {M : ℕ} (h : List.take M x = List.take M y) : firstIndicator G (↑M) x = firstIndicator G (↑M) y

Locality: two sequences with the same first M entries have the same I_1^{(M)}.

theorem PoissonDeclumping.Cyclic.firstMarked_top_iff {G : PlaneTree → Prop} {x : List ℤ} : FirstMarked G ⊤ x ↔ ∃ (T : PlaneTree), PlaneTree.ofSeq x = some T ∧ G T

With the infinite cutoff, I_1^{(∞)}(𝐱) = G(T(𝐱)) (and 0 if ζ(𝐱) = ∞).

theorem PoissonDeclumping.Cyclic.firstIndicator_top (G : PlaneTree → Prop) (x : List ℤ) [Decidable (∃ (T : PlaneTree), PlaneTree.ofSeq x = some T ∧ G T)] : firstIndicator G ⊤ x = if ∃ (T : PlaneTree), PlaneTree.ofSeq x = some T ∧ G T then 1 else 0

theorem PoissonDeclumping.Cyclic.firstMarked_iff_top_of_length_le {G : PlaneTree → Prop} {M : ℕ∞} {x : List ℤ} (h : ↑x.length ≤ M) : FirstMarked G M x ↔ FirstMarked G ⊤ x

A cutoff at least the length of the sequence is no cutoff.

theorem PoissonDeclumping.Cyclic.firstIndicator_of_length_le {G : PlaneTree → Prop} {M : ℕ∞} {x : List ℤ} (h : ↑x.length ≤ M) : firstIndicator G M x = firstIndicator G ⊤ x

Cyclic shifts of a DFS sequence

theorem PoissonDeclumping.Cyclic.shiftIndicator_dfsSeq_eq_one_iff (G : PlaneTree → Prop) (M : ℕ∞) (T : PlaneTree) (i : ℕ) (hi : i < T.vertexCount) : shiftIndicator G M T.dfsSeq i = 1 ↔ ↑T.fringeTrees[i].vertexCount ≤ M ∧ G T.fringeTrees[i]

The i-th cyclic indicator of 𝐱(T) tests the fringe subtree at the i-th vertex (eq:fringe).

theorem PoissonDeclumping.Cyclic.countP_eq_sum_range {α : Type u_1} (p : α → Bool) (l : List α) : List.countP p l = ∑ i ∈ Finset.range l.length, if h : i < l.length then if p l[i] = true then 1 else 0 else 0

theorem PoissonDeclumping.Cyclic.cyclicSum_dfsSeq (G : PlaneTree → Prop) (M : ℕ∞) (T : PlaneTree) : cyclicSum G M T.dfsSeq = PlaneTree.markCount (fun (U : PlaneTree) => ↑U.vertexCount ≤ M ∧ G U) T

The counting identity of Section 2.3: ∑_{i=1}^{n} I_i^{(M)}(𝐱(T)) is the number of vertices v of T whose fringe subtree T_v has at most M vertices and is marked.

theorem PoissonDeclumping.Cyclic.cyclicSum_dfsSeq_of_le (G : PlaneTree → Prop) {M : ℕ∞} {T : PlaneTree} (hM : ↑T.vertexCount ≤ M) : cyclicSum G M T.dfsSeq = PlaneTree.markCount G T

With a cutoff M ≥ |T|, the cyclic sum counts all marked vertices (markCount G T).

theorem PoissonDeclumping.Cyclic.cyclicSum_dfsSeq_top (G : PlaneTree → Prop) (T : PlaneTree) : cyclicSum G ⊤ T.dfsSeq = PlaneTree.markCount G T

theorem PoissonDeclumping.Cyclic.cyclicSum_rotate_one (G : PlaneTree → Prop) (M : ℕ∞) (x : List ℤ) : cyclicSum G M (x.rotate 1) = cyclicSum G M x

The cyclic sum is invariant under one rotation.

theorem PoissonDeclumping.Cyclic.cyclicSum_rotate (G : PlaneTree → Prop) (M : ℕ∞) (x : List ℤ) (k : ℕ) : cyclicSum G M (x.rotate k) = cyclicSum G M x

B04: the sum of the cyclic indicators is invariant under cyclic shifts.

theorem PoissonDeclumping.Cyclic.cyclicSum_ofFn {n : ℕ} (G : PlaneTree → Prop) (M : ℕ∞) (ω : Fin n → ℤ) : cyclicSum G M (List.ofFn ω) = ∑ i : Fin n, shiftIndicator G M (List.ofFn ω) ↑i

The cyclic sum of a vector (x_1, …, x_n), as a sum over Fin n.