Exact change of variables for collapse sums

The finite-word collapse is an Equiv, so sums over prescribed-multiplicity words can be reindexed by fixed-length raw collapse data without any fiber cardinality. This file also inserts the definitional factorial ledger pointwise. The resulting marker inverse factorial is precisely the ((s+1)!)⁻¹ in paper (5.45)(i).

@[implicit_reducible]

noncomputable instance Anderson4D.fixedRawCollapseDataFintype {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (n : ℕ) : Fintype (FixedRawCollapseData A B n)

Fixed-length raw collapse data are finite because they are equivalent to finite words.

Equations

• Anderson4D.fixedRawCollapseDataFintype n = Fintype.ofEquiv (Fin n → A ⊕ B) (Anderson4D.finWordRawCollapseEquiv A B n)

@[implicit_reducible]

noncomputable instance Anderson4D.collapseMultiplicitySpecDecidable {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) : DecidablePred (CollapseMultiplicitySpec mult)

The canonical collapse multiplicity specification is decidable on finite alphabets.

Equations

• Anderson4D.collapseMultiplicitySpecDecidable mult d = Classical.propDecidable (Anderson4D.CollapseMultiplicitySpec mult d)

def Anderson4D.outsideMultiplicity {A : Type u_1} {B : Type u_2} (mult : A ⊕ B → ℕ) : B → ℕ

The outside part of a multiplicity on a split alphabet.

Equations

• Anderson4D.outsideMultiplicity mult b = mult (Sum.inr b)

@[simp]

theorem Anderson4D.sumMultiplicity_inside_outside {A : Type u_1} {B : Type u_2} (mult : A ⊕ B → ℕ) : sumMultiplicity (insideMultiplicity mult) (outsideMultiplicity mult) = mult

@[simp]

theorem Anderson4D.collapsedMultiplicity_eq_markerMultiplicity {A : Type u_1} {B : Type u_2} (mult : A ⊕ B → ℕ) (d : RawCollapseData A B) : collapsedMultiplicity mult d = markerMultiplicity d.blocks.length (outsideMultiplicity mult)

theorem Anderson4D.collapse_factorialLedger_raw {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (mult : A ⊕ B → ℕ) (d : RawCollapseData A B) : ∏ x : A ⊕ B, ↑(mult x).factorial = (↑d.blocks.length.factorial)⁻¹ * ((∏ a : A, ↑(insideMultiplicity mult a).factorial) * ∏ x : Unit ⊕ B, ↑(collapsedMultiplicity mult d x).factorial)

The collapse factorial ledger specialized to the canonical inside and collapsed multiplicities of a raw collapse datum.

theorem Anderson4D.sum_validWords_eq_sum_fixedRawCollapseData {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] {n : ℕ} (mult : A ⊕ B → ℕ) (F : (Fin n → A ⊕ B) → ℝ) : ∑ w ∈ validWords mult, F w = ∑ d : FixedRawCollapseData A B n, if CollapseMultiplicitySpec mult ↑d then F ((finWordRawCollapseEquiv A B n).symm d) else 0

Exact reindexing of a prescribed-multiplicity word sum by the honest finite collapse equivalence.

theorem Anderson4D.sum_validWords_filter_eq_sum_fixedRawCollapseData {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] {n : ℕ} (mult : A ⊕ B → ℕ) (P : (Fin n → A ⊕ B) → Prop) [DecidablePred P] (F : (Fin n → A ⊕ B) → ℝ) : ∑ w ∈ validWords mult with P w, F w = ∑ d : FixedRawCollapseData A B n, if CollapseMultiplicitySpec mult ↑d ∧ P ((finWordRawCollapseEquiv A B n).symm d) then F ((finWordRawCollapseEquiv A B n).symm d) else 0

Predicate-filtered version of the exact collapse change of variables.

theorem Anderson4D.paperSum_eq_sum_fixedRawCollapseData {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] {n : ℕ} (mult : A ⊕ B → ℕ) (F : (Fin n → A ⊕ B) → ℝ) : paperSum mult F = ∑ d : FixedRawCollapseData A B n, if CollapseMultiplicitySpec mult ↑d then (↑(↑d).blocks.length.factorial)⁻¹ * ((∏ a : A, ↑(insideMultiplicity mult a).factorial) * ∏ x : Unit ⊕ B, ↑(collapsedMultiplicity mult (↑d) x).factorial) * F ((finWordRawCollapseEquiv A B n).symm d) else 0

paperSum after collapse reindexing. The inverse marker factorial is inserted pointwise, so it remains correct while the number of blocks varies between collapse data.

theorem Anderson4D.paperSumFiltered_eq_sum_fixedRawCollapseData {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] {n : ℕ} (mult : A ⊕ B → ℕ) (P : (Fin n → A ⊕ B) → Prop) [DecidablePred P] (F : (Fin n → A ⊕ B) → ℝ) : paperSumFiltered mult P F = ∑ d : FixedRawCollapseData A B n, if CollapseMultiplicitySpec mult ↑d ∧ P ((finWordRawCollapseEquiv A B n).symm d) then (↑(↑d).blocks.length.factorial)⁻¹ * ((∏ a : A, ↑(insideMultiplicity mult a).factorial) * ∏ x : Unit ⊕ B, ↑(collapsedMultiplicity mult (↑d) x).factorial) * F ((finWordRawCollapseEquiv A B n).symm d) else 0

Predicate-filtered paperSum after the same exact change of variables and factorial-ledger insertion.