Finite Fubini bounds for collapse coordinates

The P-5.9 collapse sum must be separated into an inside-word sum and a collapsed-word sum without paying for the number of original words. The mechanism is an injective map into a product, applied separately on every fixed block-composition shape.

A generic injective finite Fubini bound

theorem Anderson4D.sum_comp_mul_le_sum_mul_sum_of_pair_injective {I : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype I] [Fintype X] [Fintype Y] (f : I → X) (g : I → Y) (hpair : Function.Injective fun (i : I) => (f i, g i)) (a : X → ℝ) (b : Y → ℝ) (ha : ∀ (x : X), 0 ≤ a x) (hb : ∀ (y : Y), 0 ≤ b y) : ∑ i : I, a (f i) * b (g i) ≤ (∑ x : X, a x) * ∑ y : Y, b y

An injectively indexed subfamily of a nonnegative product sum is bounded by the full product of the two marginal sums.

Fixed-shape collapse coordinates

def Anderson4D.RawCollapseData.collapseShape {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : List ℕ

The ordered positive block lengths of a raw collapse datum.

Equations

• d.collapseShape = List.map List.length d.blocks

@[simp]

theorem Anderson4D.RawCollapseData.collapseShape_length {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.collapseShape.length = d.blocks.length

@[simp]

theorem Anderson4D.RawCollapseData.collapseShape_sum {A : Type u_1} {B : Type u_2} (d : RawCollapseData A B) : d.collapseShape.sum = d.insideLength

theorem Anderson4D.RawCollapseData.eq_of_shape_insideList_collapsed {A : Type u_1} {B : Type u_2} (d e : RawCollapseData A B) (hshape : d.collapseShape = e.collapseShape) (hinside : d.insideList = e.insideList) (hcollapsed : d.collapsed = e.collapsed) : d = e

At fixed shape, the flattened inside word and collapsed word determine the complete raw datum.

@[reducible, inline]

abbrev Anderson4D.FixedRawCollapseShapeData (A : Type u_3) (B : Type u_4) (n : ℕ) (shape : List ℕ) : Type (max 0 u_3 u_4)

Fixed-original-length raw data in one block-composition shape fiber.

Equations

• Anderson4D.FixedRawCollapseShapeData A B n shape = { d : Anderson4D.FixedRawCollapseData A B n // (↑d).collapseShape = shape }

def Anderson4D.fixedShapeListPair {A : Type u_1} {B : Type u_2} {n : ℕ} {shape : List ℕ} (d : FixedRawCollapseShapeData A B n shape) : List A × List (Unit ⊕ B)

Coordinate pair on a fixed shape fiber, still in list form.

Equations

• Anderson4D.fixedShapeListPair d = ((↑↑d).insideList, (↑↑d).collapsed)

theorem Anderson4D.fixedShapeListPair_injective {A : Type u_1} {B : Type u_2} {n : ℕ} {shape : List ℕ} : Function.Injective fixedShapeListPair

No collapse datum multiplicity remains inside a fixed shape fiber.

theorem Anderson4D.fixedShape_insideLength {A : Type u_1} {B : Type u_2} {n : ℕ} {shape : List ℕ} (d : FixedRawCollapseShapeData A B n shape) : (↑↑d).insideLength = shape.sum

The common inside-word length in a fixed shape fiber.

theorem Anderson4D.fixedShape_collapsedLength {A : Type u_1} {B : Type u_2} {n : ℕ} {shape : List ℕ} (d : FixedRawCollapseShapeData A B n shape) : (↑↑d).collapsed.length = n - shape.sum + shape.length

The common collapsed-word length in a fixed shape fiber.

def Anderson4D.fixedShapeInsideWord {A : Type u_1} {B : Type u_2} {n : ℕ} {shape : List ℕ} (d : FixedRawCollapseShapeData A B n shape) : Fin shape.sum → A

The inside list regarded as a finite word on the shape-determined carrier.

Equations

• Anderson4D.fixedShapeInsideWord d = List.Vector.get ⟨(↑↑d).insideList, ⋯⟩

def Anderson4D.fixedShapeCollapsedWord {A : Type u_1} {B : Type u_2} {n : ℕ} {shape : List ℕ} (d : FixedRawCollapseShapeData A B n shape) : Fin (n - shape.sum + shape.length) → Unit ⊕ B

The collapsed list regarded as a finite word on its shape-determined carrier.

Equations

• Anderson4D.fixedShapeCollapsedWord d = List.Vector.get ⟨(↑↑d).collapsed, ⋯⟩

@[simp]

theorem Anderson4D.ofFn_fixedShapeInsideWord {A : Type u_1} {B : Type u_2} {n : ℕ} {shape : List ℕ} (d : FixedRawCollapseShapeData A B n shape) : List.ofFn (fixedShapeInsideWord d) = (↑↑d).insideList

@[simp]

theorem Anderson4D.ofFn_fixedShapeCollapsedWord {A : Type u_1} {B : Type u_2} {n : ℕ} {shape : List ℕ} (d : FixedRawCollapseShapeData A B n shape) : List.ofFn (fixedShapeCollapsedWord d) = (↑↑d).collapsed

theorem Anderson4D.fixedShapeWordPair_injective {A : Type u_1} {B : Type u_2} {n : ℕ} {shape : List ℕ} : Function.Injective fun (d : FixedRawCollapseShapeData A B n shape) => (fixedShapeInsideWord d, fixedShapeCollapsedWord d)

The pair of finite words is injective on a fixed shape fiber.

Fubini bounds on one shape fiber

theorem Anderson4D.sum_fixedRawCollapseShapeData_eq_filter {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] {n : ℕ} {shape : List ℕ} (F : FixedRawCollapseData A B n → ℝ) : ∑ d : FixedRawCollapseShapeData A B n shape, F ↑d = ∑ d : FixedRawCollapseData A B n with (↑d).collapseShape = shape, F d

A subtype sum over one shape is the corresponding filtered sum over all fixed-length raw data.

theorem Anderson4D.sum_fixedShape_wordWeights_le_product {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] {n : ℕ} {shape : List ℕ} (F₁ : (Fin shape.sum → A) → ℝ) (F₂ : (Fin (n - shape.sum + shape.length) → Unit ⊕ B) → ℝ) (hF₁ : ∀ (w : Fin shape.sum → A), 0 ≤ F₁ w) (hF₂ : ∀ (w : Fin (n - shape.sum + shape.length) → Unit ⊕ B), 0 ≤ F₂ w) : ∑ d : FixedRawCollapseShapeData A B n shape, F₁ (fixedShapeInsideWord d) * F₂ (fixedShapeCollapsedWord d) ≤ (∑ w₁ : Fin shape.sum → A, F₁ w₁) * ∑ w₂ : Fin (n - shape.sum + shape.length) → Unit ⊕ B, F₂ w₂

Finite-word form of the fixed-shape Fubini bound.

theorem Anderson4D.sum_fixedShape_listWeights_le_product {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] {n : ℕ} {shape : List ℕ} (F₁ : List A → ℝ) (F₂ : List (Unit ⊕ B) → ℝ) (hF₁ : ∀ (l : List A), 0 ≤ F₁ l) (hF₂ : ∀ (l : List (Unit ⊕ B)), 0 ≤ F₂ l) : ∑ d : FixedRawCollapseShapeData A B n shape, F₁ (↑↑d).insideList * F₂ (↑↑d).collapsed ≤ (∑ w₁ : Fin shape.sum → A, F₁ (List.ofFn w₁)) * ∑ w₂ : Fin (n - shape.sum + shape.length) → Unit ⊕ B, F₂ (List.ofFn w₂)

List-weight form consumed by collapse estimates. The right side uses the two independent finite-word carriers of the shape-determined lengths.

theorem Anderson4D.sum_fixedRaw_filter_shape_listWeights_le_product {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] {n : ℕ} {shape : List ℕ} (F₁ : List A → ℝ) (F₂ : List (Unit ⊕ B) → ℝ) (hF₁ : ∀ (l : List A), 0 ≤ F₁ l) (hF₂ : ∀ (l : List (Unit ⊕ B)), 0 ≤ F₂ l) : ∑ d : FixedRawCollapseData A B n with (↑d).collapseShape = shape, F₁ (↑d).insideList * F₂ (↑d).collapsed ≤ (∑ w₁ : Fin shape.sum → A, F₁ (List.ofFn w₁)) * ∑ w₂ : Fin (n - shape.sum + shape.length) → Unit ⊕ B, F₂ (List.ofFn w₂)

Filtered-data form used immediately after the exact collapse change of variables. No cardinality of the shape fiber appears.