Alphabet transport for collapse sums

The structural leaf decomposition is an equivalence

HeppLeaf t ≃ InsideLeaf r ⊕ OutsideLeaf r.

This file proves that validWords, wordSum, and the definitional paperSum are invariant under an arbitrary finite alphabet equivalence, and then specializes the construction to that leaf decomposition.

def Anderson4D.renameMultiplicity {α : Type u_1} {β : Type u_2} (e : α ≃ β) (mult : α → ℕ) : β → ℕ

Transport a multiplicity function covariantly along an equivalence.

Equations

• Anderson4D.renameMultiplicity e mult b = mult (e.symm b)

@[simp]

theorem Anderson4D.renameMultiplicity_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (mult : α → ℕ) (a : α) : renameMultiplicity e mult (e a) = mult a

def Anderson4D.wordRenameEquiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) (n : ℕ) : (Fin n → α) ≃ (Fin n → β)

Apply an alphabet equivalence pointwise to a finite word.

Equations

• Anderson4D.wordRenameEquiv e n = { toFun := fun (w : Fin n → α) (i : Fin n) => e (w i), invFun := fun (w : Fin n → β) (i : Fin n) => e.symm (w i), left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Anderson4D.wordRenameEquiv_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (n : ℕ) (w : Fin n → α) (i : Fin n) : (wordRenameEquiv e n) w i = e (w i)

@[simp]

theorem Anderson4D.wordRenameEquiv_symm_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (n : ℕ) (w : Fin n → β) (i : Fin n) : (wordRenameEquiv e n).symm w i = e.symm (w i)

theorem Anderson4D.wordRename_mem_validWords_iff {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {n : ℕ} (e : α ≃ β) (mult : α → ℕ) (w : Fin n → α) : (wordRenameEquiv e n) w ∈ validWords (renameMultiplicity e mult) ↔ w ∈ validWords mult

Prescribed fiber cardinalities are invariant under renaming letters.

theorem Anderson4D.factorialLedger_rename {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (e : α ≃ β) (mult : α → ℕ) : ∏ b : β, ↑(renameMultiplicity e mult b).factorial = ∏ a : α, ↑(mult a).factorial

The product of multiplicity factorials is invariant under renaming the finite alphabet.

theorem Anderson4D.wordSum_rename {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {n : ℕ} (e : α ≃ β) (mult : α → ℕ) (F : (Fin n → α) → ℝ) : wordSum mult F = wordSum (renameMultiplicity e mult) fun (w : Fin n → β) => F ((wordRenameEquiv e n).symm w)

Raw word sums are unchanged by a finite alphabet equivalence.

theorem Anderson4D.paperSum_rename {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {n : ℕ} (e : α ≃ β) (mult : α → ℕ) (F : (Fin n → α) → ℝ) : paperSum mult F = paperSum (renameMultiplicity e mult) fun (w : Fin n → β) => F ((wordRenameEquiv e n).symm w)

The definitional paper sum is invariant under the same renaming.

The Hepp-leaf split alphabet

def Anderson4D.splitLeafMultiplicity {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) : InsideLeaf r ⊕ OutsideLeaf r → ℕ

Original leaf multiplicities expressed on the canonical inside/outside sum alphabet.

Equations

• Anderson4D.splitLeafMultiplicity mu r = Anderson4D.renameMultiplicity (Anderson4D.leafInsideOutsideEquiv r) (Anderson4D.leafMultiplicity mu)

@[simp]

theorem Anderson4D.splitLeafMultiplicity_inl {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (l : InsideLeaf r) : splitLeafMultiplicity mu r (Sum.inl l) = leafMultiplicity mu ↑l

@[simp]

theorem Anderson4D.splitLeafMultiplicity_inr {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (l : OutsideLeaf r) : splitLeafMultiplicity mu r (Sum.inr l) = leafMultiplicity mu ↑l

def Anderson4D.splitLeafWordEquiv {t : PlaneTree} (r : t.VPos) (n : ℕ) : (Fin n → HeppLeaf t) ≃ (Fin n → InsideLeaf r ⊕ OutsideLeaf r)

The original leaf word renamed to the inside/outside sum alphabet.

Equations

• Anderson4D.splitLeafWordEquiv r n = Anderson4D.wordRenameEquiv (Anderson4D.leafInsideOutsideEquiv r) n

theorem Anderson4D.paperSum_eq_splitLeafAlphabet {t : PlaneTree} {n : ℕ} (mu : t.Multiplicities) (r : t.VPos) (F : (Fin n → HeppLeaf t) → ℝ) : paperSum (leafMultiplicity mu) F = paperSum (splitLeafMultiplicity mu r) fun (w : Fin n → InsideLeaf r ⊕ OutsideLeaf r) => F ((splitLeafWordEquiv r n).symm w)

Tree-facing alphabet split for arbitrary paper-sum statistics.