Eighth derivative of a finite scalar product

This module records the numerical Leibniz ledger needed for the fixed-cutoff relative-translation argument. The factors are indexed by slot IDs in a finset; equal function values therefore remain distinct when their slot IDs are distinct.

Mathlib's symmetric-power bound groups the ordered choices of a differentiated slot. The multiplicity Multiset.countPerms is retained until the final sum, where the multinomial theorem shows that its total is exactly the eighth power of the number of slots. Thus no additional 8! loss is introduced.

theorem Anderson4D.symEight_count_le {ι : Type u_1} [DecidableEq ι] (p : Sym ι 8) (j : ι) : Multiset.count j ↑p ≤ 8

A component of an eighth-order symmetric allocation assigns at most eight derivatives to any one slot.

theorem Anderson4D.abs_iteratedDeriv_eight_finsetProd_le_sym {ι : Type u_1} [DecidableEq ι] {u : Finset ι} {f : ι → ℝ → ℝ} (hf : ∀ j ∈ u, ContDiff ℝ 8 (f j)) (x : ℝ) : |iteratedDeriv 8 (fun (t : ℝ) => ∏ j ∈ u, f j t) x| ≤ ∑ p ∈ u.sym 8, ↑(↑p).countPerms * ∏ j ∈ u, |iteratedDeriv (Multiset.count j ↑p) (f j) x|

Scalar specialization of mathlib's finite-product iterated Fréchet derivative bound.

The carrier u.sym 8 is the collection of weak derivative allocations. Its countPerms weight remembers how many ordered sequences of eight single-slot differentiations give the same allocation.

theorem Anderson4D.sum_countPerms_symEight_eq_card_pow {ι : Type u_1} [DecidableEq ι] (u : Finset ι) : ∑ p ∈ u.sym 8, ↑(↑p).countPerms = ↑u.card ^ 8

The total multiplicity of all weak allocations of eight derivative slots is exactly the number of ordered slot choices.

theorem Anderson4D.abs_iteratedDeriv_eight_finsetProd_le_card_pow {ι : Type u_1} [DecidableEq ι] {u : Finset ι} {f : ι → ℝ → ℝ} (hf : ∀ j ∈ u, ContDiff ℝ 8 (f j)) (B : ι → ℝ) (x : ℝ) (hderiv : ∀ j ∈ u, ∀ r ≤ 8, |iteratedDeriv r (f j) x| ≤ B j) : |iteratedDeriv 8 (fun (t : ℝ) => ∏ j ∈ u, f j t) x| ≤ ↑u.card ^ 8 * ∏ j ∈ u, B j

Uniform eighth-derivative product bound without factorial loss.

If every derivative through order eight of the factor in slot j is bounded at x by B j, then the eighth derivative of the whole product is bounded by card(u)^8 times the product of those majorants.