Shape ledger for the P-5.9 collapse sum

For a prescribed multiplicity, every valid raw collapse datum has the same inside-word length. Its ordered block lengths therefore form a positive composition of one fixed integer. This file enumerates only the shapes that actually occur and splits the finite raw-data sum exactly into their fibers.

theorem Anderson4D.RawCollapseData.collapseShape_pos {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) {k : ℕ} (hk : k ∈ d.collapseShape) : 0 < k

Every entry of the collapse shape is positive.

theorem Anderson4D.RawCollapseData.insideLength_eq_sum_insideMultiplicity {A : Type u_1} {B : Type u_2} [Fintype A] [DecidableEq A] [DecidableEq B] {mult : A ⊕ B → ℕ} {d : RawCollapseData A B} (h : CollapseMultiplicitySpec mult d) : d.insideLength = ∑ a : A, insideMultiplicity mult a

The multiplicity specification fixes the inside length.

def Anderson4D.RawCollapseData.collapseCompositionOfSpec {A : Type u_1} {B : Type u_2} [Fintype A] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (d : RawCollapseData A B) (h : CollapseMultiplicitySpec mult d) : Composition (∑ a : A, insideMultiplicity mult a)

A valid raw datum supplies a positive composition of the fixed total inside multiplicity.

Equations

• Anderson4D.RawCollapseData.collapseCompositionOfSpec mult d h = { blocks := d.collapseShape, blocks_pos := ⋯, blocks_sum := ⋯ }

theorem Anderson4D.RawCollapseData.collapseShape_ne_nil_of_spec {A : Type u_1} {B : Type u_2} [Fintype A] [DecidableEq A] [DecidableEq B] {mult : A ⊕ B → ℕ} {d : RawCollapseData A B} (h : CollapseMultiplicitySpec mult d) (hpos : 0 < ∑ a : A, insideMultiplicity mult a) : d.collapseShape ≠ []

Positive inside total forces the shape to be nonempty.

Tree-facing fixed-length statement

theorem Anderson4D.sum_insideMultiplicity_splitLeafMultiplicity {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) : ∑ l : InsideLeaf r, insideMultiplicity (splitLeafMultiplicity mu r) l = totalMultiplicity (restrictMultiplicities mu r)

The inside part of the split multiplicity has exactly the total multiplicity of the restricted subtree.

theorem Anderson4D.RawCollapseData.insideLength_eq_totalMultiplicity_restrict {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (h : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d) : d.insideLength = totalMultiplicity (restrictMultiplicities mu r)

For the canonical inside/outside split, the valid inside length is exactly the total multiplicity of the restricted subtree.

theorem Anderson4D.RawCollapseData.collapseShape_ne_nil_of_splitSpec {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (d : RawCollapseData (InsideLeaf r) (OutsideLeaf r)) (h : CollapseMultiplicitySpec (splitLeafMultiplicity mu r) d) : d.collapseShape ≠ []

In the tree-facing situation the selected inside subtree has positive total multiplicity, so every valid collapse shape is nonempty.

The finite family of occurring shapes

noncomputable def Anderson4D.specFixedRawCollapseData {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (n : ℕ) : Finset (FixedRawCollapseData A B n)

Fixed-length raw data satisfying the prescribed multiplicity.

Equations

• Anderson4D.specFixedRawCollapseData mult n = {d : Anderson4D.FixedRawCollapseData A B n | Anderson4D.CollapseMultiplicitySpec mult ↑d}

@[simp]

theorem Anderson4D.mem_specFixedRawCollapseData_iff {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (n : ℕ) (d : FixedRawCollapseData A B n) : d ∈ specFixedRawCollapseData mult n ↔ CollapseMultiplicitySpec mult ↑d

noncomputable def Anderson4D.validCollapseShapes {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (n : ℕ) : Finset (List ℕ)

Only shapes that are realized by a valid fixed-length raw datum.

Equations

• Anderson4D.validCollapseShapes mult n = Finset.image (fun (d : Anderson4D.FixedRawCollapseData A B n) => (↑d).collapseShape) (Anderson4D.specFixedRawCollapseData mult n)

theorem Anderson4D.mem_validCollapseShapes_iff {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (n : ℕ) (shape : List ℕ) : shape ∈ validCollapseShapes mult n ↔ ∃ (d : FixedRawCollapseData A B n), CollapseMultiplicitySpec mult ↑d ∧ (↑d).collapseShape = shape

theorem Anderson4D.validCollapseShape_pos {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (n : ℕ) {shape : List ℕ} (hshape : shape ∈ validCollapseShapes mult n) {k : ℕ} (hk : k ∈ shape) : 0 < k

Every entry of an occurring shape is positive.

theorem Anderson4D.validCollapseShape_sum {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (n : ℕ) {shape : List ℕ} (hshape : shape ∈ validCollapseShapes mult n) : shape.sum = ∑ a : A, insideMultiplicity mult a

Every occurring shape sums to the one fixed inside total.

theorem Anderson4D.validCollapseShape_ne_nil {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (n : ℕ) (hpos : 0 < ∑ a : A, insideMultiplicity mult a) {shape : List ℕ} (hshape : shape ∈ validCollapseShapes mult n) : shape ≠ []

If the fixed inside total is positive, every occurring shape is nonempty.

def Anderson4D.validCollapseShapeComposition {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (n : ℕ) (shape : ↥(validCollapseShapes mult n)) : Composition (∑ a : A, insideMultiplicity mult a)

An occurring shape, packaged as a genuine mathlib composition of the fixed inside total.

Equations

• Anderson4D.validCollapseShapeComposition mult n shape = { blocks := ↑shape, blocks_pos := ⋯, blocks_sum := ⋯ }

theorem Anderson4D.validCollapseShapeComposition_injective {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (n : ℕ) : Function.Injective (validCollapseShapeComposition mult n)

Different occurring shape lists give different compositions.

theorem Anderson4D.card_validCollapseShapes_le_two_pow {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (n : ℕ) : (validCollapseShapes mult n).card ≤ 2 ^ ∑ a : A, insideMultiplicity mult a

The occurring shape family costs at most the coarse paper factor 2^(inside total).

theorem Anderson4D.card_validCollapseShapes_split_le_two_pow_restrict {t : PlaneTree} (mu : t.Multiplicities) (r : t.VPos) (originalLength : ℕ) : (validCollapseShapes (splitLeafMultiplicity mu r) originalLength).card ≤ 2 ^ totalMultiplicity (restrictMultiplicities mu r)

Tree-facing count: the shape loss is controlled by the restricted inside multiplicity, exactly the n used in the collapse step.

Exact outer shape decomposition

theorem Anderson4D.sum_eq_sum_image_fibers {ι : Type u_3} {κ : Type u_4} {M : Type u_5} [DecidableEq κ] [AddCommMonoid M] (s : Finset ι) (key : ι → κ) (F : ι → M) : ∑ x ∈ s, F x = ∑ y ∈ Finset.image key s, ∑ x ∈ s with key x = y, F x

Any finite sum splits exactly into the fibers of a key map.

theorem Anderson4D.sum_specFixedRawCollapseData_eq_sum_shapes {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] {M : Type u_3} [AddCommMonoid M] (mult : A ⊕ B → ℕ) (n : ℕ) (F : FixedRawCollapseData A B n → M) : ∑ d ∈ specFixedRawCollapseData mult n, F d = ∑ shape ∈ validCollapseShapes mult n, ∑ d ∈ specFixedRawCollapseData mult n with (↑d).collapseShape = shape, F d

The valid fixed-length raw-data sum splits exactly by occurring shape.

theorem Anderson4D.sum_ite_collapseMultiplicitySpec_eq_sum_shapes {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] {M : Type u_3} [AddCommMonoid M] (mult : A ⊕ B → ℕ) (n : ℕ) (F : FixedRawCollapseData A B n → M) : (∑ d : FixedRawCollapseData A B n, if CollapseMultiplicitySpec mult ↑d then F d else 0) = ∑ shape ∈ validCollapseShapes mult n, ∑ d ∈ specFixedRawCollapseData mult n with (↑d).collapseShape = shape, F d

if spec then ... else 0, exactly as produced by CollapseSum, in outer-shape/fiber form.

theorem Anderson4D.spec_shape_fiber_subset_shape_fiber {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (n : ℕ) (shape : List ℕ) : {d ∈ specFixedRawCollapseData mult n | (↑d).collapseShape = shape} ⊆ {d : FixedRawCollapseData A B n | (↑d).collapseShape = shape}

A valid-spec shape fiber is a subset of the unrestricted shape fiber used by CollapseFubini.

theorem Anderson4D.sum_spec_shape_fiber_le_sum_shape_fiber {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] [DecidableEq A] [DecidableEq B] (mult : A ⊕ B → ℕ) (n : ℕ) (shape : List ℕ) (F : FixedRawCollapseData A B n → ℝ) (hF : ∀ (d : FixedRawCollapseData A B n), 0 ≤ F d) : ∑ d ∈ specFixedRawCollapseData mult n with (↑d).collapseShape = shape, F d ≤ ∑ d : FixedRawCollapseData A B n with (↑d).collapseShape = shape, F d

Nonnegative valid-spec fiber sums are bounded by the unrestricted fiber to which the Fubini lemma applies.