Renaming invariance of the Proposition 5.9 summand

The collapse induction replaces the Hepp-leaf alphabet by the canonical inside/outside sum alphabet. This file records that both word restrictions and the positional chain statistic are invariant under that replacement.

Word predicates

theorem Anderson4D.noAdjacentEqual_wordRename_iff {α : Type u_1} {β : Type u_2} {m : ℕ} (e : α ≃ β) (w : Fin m → α) : NoAdjacentEqual ((wordRenameEquiv e m) w) ↔ NoAdjacentEqual w

Unequal neighbours are invariant under an alphabet equivalence.

theorem Anderson4D.letterPositions_wordRename_map {α : Type u_1} {β : Type u_2} {m : ℕ} [DecidableEq α] [DecidableEq β] (e : α ≃ β) (w : Fin m → α) (S : Finset α) : letterPositions ((wordRenameEquiv e m) w) (Finset.map e.toEmbedding S) = letterPositions w S

A finite set of letters and its image under an equivalence occupy the same positions in a renamed word.

theorem Anderson4D.noProperLeafBlock_wordRename {α : Type u_1} {β : Type u_2} {m : ℕ} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ≃ β) (w : Fin m → α) (hw : NoProperLeafBlock w) : NoProperLeafBlock ((wordRenameEquiv e m) w)

The paper's proper-leaf-block restriction is invariant under renaming the alphabet.

theorem Anderson4D.noProperLeafBlock_wordRename_iff {α : Type u_1} {β : Type u_2} {m : ℕ} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ≃ β) (w : Fin m → α) : NoProperLeafBlock ((wordRenameEquiv e m) w) ↔ NoProperLeafBlock w

Iff form used to rewrite the indicator in the P-5.9 summand.

Position-chain statistic

noncomputable def Anderson4D.alphabetChainWeight {α : Type u_1} {m : ℕ} (z : α → Fin 4 → ℤ) (w : Fin m → α) : ℝ

The Hepp chain formula on an arbitrary finite alphabet equipped with lattice positions. On the actual Hepp-leaf alphabet this is definitionally heppChainWeight.

Equations

• Anderson4D.alphabetChainWeight z w = ∏ j : Anderson4D.AdjacentIndex m, Anderson4D.latticeEdgeWeight (z (w ↑j)) (z (w (Anderson4D.adjacentSucc j)))

@[simp]

theorem Anderson4D.alphabetChainWeight_heppLeaf {m : ℕ} {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : alphabetChainWeight z w = heppChainWeight z w

@[simp]

theorem Anderson4D.alphabetChainWeight_wordRename {α : Type u_1} {β : Type u_2} {m : ℕ} (e : α ≃ β) (z : α → Fin 4 → ℤ) (w : Fin m → α) : alphabetChainWeight (fun (b : β) => z (e.symm b)) ((wordRenameEquiv e m) w) = alphabetChainWeight z w

Pulling positions back by the inverse equivalence makes the chain product exactly invariant under word renaming.

@[simp]

theorem Anderson4D.heppChainWeight_wordRename {m : ℕ} {t u : PlaneTree} (e : HeppLeaf t ≃ HeppLeaf u) (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : heppChainWeight (fun (l : HeppLeaf u) => z (e.symm l)) ((wordRenameEquiv e m) w) = heppChainWeight z w

Direct Hepp-leaf form when both alphabets happen to be leaf types.

theorem Anderson4D.heppChainWeight_eq_renamed {m : ℕ} {t : PlaneTree} {γ : Type u_3} (e : HeppLeaf t ≃ γ) (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : heppChainWeight z w = alphabetChainWeight (fun (c : γ) => z (e.symm c)) ((wordRenameEquiv e m) w)

heppChainWeight expressed without loss on an arbitrary renamed alphabet.

noncomputable def Anderson4D.primitiveSeparatedAlphabetChainWeight {α : Type u_1} {m : ℕ} [Fintype α] [DecidableEq α] (z : α → Fin 4 → ℤ) (w : Fin m → α) : ℝ

The P-5.9 pointwise statistic on an arbitrary finite alphabet with lattice positions.

Equations

• Anderson4D.primitiveSeparatedAlphabetChainWeight z w = if Anderson4D.NoProperLeafBlock w ∧ Anderson4D.NoAdjacentEqual w then Anderson4D.alphabetChainWeight z w else 0

@[simp]

theorem Anderson4D.primitiveSeparatedAlphabetChainWeight_heppLeaf {m : ℕ} {t : PlaneTree} (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : primitiveSeparatedAlphabetChainWeight z w = primitiveSeparatedChainWeight z w

@[simp]

theorem Anderson4D.primitiveSeparatedAlphabetChainWeight_wordRename {α : Type u_1} {β : Type u_2} {m : ℕ} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] (e : α ≃ β) (z : α → Fin 4 → ℤ) (w : Fin m → α) : primitiveSeparatedAlphabetChainWeight (fun (b : β) => z (e.symm b)) ((wordRenameEquiv e m) w) = primitiveSeparatedAlphabetChainWeight z w

The complete primitive-and-separated chain statistic is exactly invariant under alphabet renaming.

@[simp]

theorem Anderson4D.primitiveSeparatedChainWeight_wordRename {m : ℕ} {t u : PlaneTree} (e : HeppLeaf t ≃ HeppLeaf u) (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : primitiveSeparatedChainWeight (fun (l : HeppLeaf u) => z (e.symm l)) ((wordRenameEquiv e m) w) = primitiveSeparatedChainWeight z w

Direct Hepp-leaf form of invariance for the complete P-5.9 summand.

theorem Anderson4D.primitiveSeparatedChainWeight_eq_renamed {m : ℕ} {t : PlaneTree} {γ : Type u_3} [Fintype γ] [DecidableEq γ] (e : HeppLeaf t ≃ γ) (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : primitiveSeparatedChainWeight z w = primitiveSeparatedAlphabetChainWeight (fun (c : γ) => z (e.symm c)) ((wordRenameEquiv e m) w)

primitiveSeparatedChainWeight expressed without loss on any renamed finite alphabet.

The canonical inside/outside leaf split

def Anderson4D.splitLeafPosition {t : PlaneTree} (r : t.VPos) (z : HeppLeaf t → Fin 4 → ℤ) : InsideLeaf r ⊕ OutsideLeaf r → Fin 4 → ℤ

The original Hepp embedding pulled back to the inside/outside alphabet.

Equations

• Anderson4D.splitLeafPosition r z l = z ((Anderson4D.leafInsideOutsideEquiv r).symm l)

theorem Anderson4D.primitiveSeparatedChainWeight_eq_splitLeafWord {m : ℕ} {t : PlaneTree} (r : t.VPos) (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → HeppLeaf t) : primitiveSeparatedChainWeight z w = primitiveSeparatedAlphabetChainWeight (splitLeafPosition r z) ((splitLeafWordEquiv r m) w)

Forward tree-facing form: renaming a Hepp-leaf word to the split alphabet does not alter its P-5.9 summand.

@[simp]

theorem Anderson4D.primitiveSeparatedChainWeight_splitLeafWord_symm {m : ℕ} {t : PlaneTree} (r : t.VPos) (z : HeppLeaf t → Fin 4 → ℤ) (w : Fin m → InsideLeaf r ⊕ OutsideLeaf r) : primitiveSeparatedChainWeight z ((splitLeafWordEquiv r m).symm w) = primitiveSeparatedAlphabetChainWeight (splitLeafPosition r z) w

Inverse orientation used after paperSum_eq_splitLeafAlphabet: the pulled-back original summand is directly the same statistic on a split word.

theorem Anderson4D.paperSum_primitiveSeparated_eq_splitLeafAlphabet {t : PlaneTree} {n : ℕ} (mu : t.Multiplicities) (r : t.VPos) (z : HeppLeaf t → Fin 4 → ℤ) : paperSum (leafMultiplicity mu) (primitiveSeparatedChainWeight z) = paperSum (splitLeafMultiplicity mu r) (primitiveSeparatedAlphabetChainWeight (splitLeafPosition r z))

Sum-level tree-facing corollary: after splitting the leaf alphabet, the P-5.9 summand is literally the same primitive-and-separated chain statistic with the pulled-back positions.