First-high finite telescoping identities

This file records the purely algebraic finite-slot decomposition used before the probabilistic Wick expansion. If every slot splits as full i = low i + high i, the product (or any multilinear expression) is the all-low term plus a sum indexed by the first high slot: slots before i are low, slot i is high, and slots after i remain full.

The product identity is the order-dual form of Finset.prod_add_ordered. The multilinear identity is proved directly by induction on the number of slots. Neither statement has any analytic or probabilistic hypotheses.

theorem Anderson4D.Finset.prod_add_ordered_firstHigh {A : Type u_1} {ι : Type u_2} [CommSemiring A] [LinearOrder ι] (s : Finset ι) (low high : ι → A) : ∏ i ∈ s, (low i + high i) = ∏ i ∈ s, low i + ∑ i ∈ s, (∏ j ∈ s with j < i, low j) * high i * ∏ j ∈ s with i < j, (low j + high j)

The first-high orientation of Finset.prod_add_ordered.

The summand at i has a low prefix, a high factor at i, and the unsplit full suffix. Passing to OrderDual ι turns mathlib's last-high orientation into this one.

theorem Anderson4D.Fin.prod_firstHigh {A : Type u_1} [CommSemiring A] {n : ℕ} (full low high : Fin n → A) (hfull : ∀ (i : Fin n), full i = low i + high i) : ∏ i : Fin n, full i = ∏ i : Fin n, low i + ∑ i : Fin n, (∏ j : Fin n with j < i, low j) * high i * ∏ j : Fin n with i < j, full j

A finite product split at its first high slot.

This is the form consumed by the finite-slot Wick telescope: the index is the original slot index, not a permutation or a reversed index.

def Anderson4D.firstHighSlot {M : Type u_2} {n : ℕ} (full low high : Fin n → M) (i : Fin n) : Fin n → M

The input tuple for the summand whose first high slot is i.

It equals low before i, high at i, and full after i.

Equations

• Anderson4D.firstHighSlot full low high i j = if j < i then low j else if j = i then high j else full j

@[simp]

theorem Anderson4D.firstHighSlot_zero {M : Type u_2} {n : ℕ} (full low high : Fin (n + 1) → M) : firstHighSlot full low high 0 = Fin.cons (high 0) (Fin.tail full)

@[simp]

theorem Anderson4D.firstHighSlot_succ {M : Type u_2} {n : ℕ} (full low high : Fin (n + 1) → M) (i : Fin n) : firstHighSlot full low high i.succ = Fin.cons (low 0) (firstHighSlot (Fin.tail full) (Fin.tail low) (Fin.tail high) i)

theorem Anderson4D.MultilinearMap.map_add_firstHigh {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {n : ℕ} (f : MultilinearMap R (fun (x : Fin n) => M) N) (full low high : Fin n → M) (hfull : ∀ (i : Fin n), full i = low i + high i) : f full = f low + ∑ i : Fin n, f (firstHighSlot full low high i)

A multilinear expression split at its first high slot.

Only additivity in each slot is used. In particular this applies directly to the deterministic multilinear carrier underneath a finite Wick expression.