English
Given a sequence X of length order, tupleSucc(X) is the next-tuple where the first order-1 coordinates are shifted, and the last coordinate is the linear combination of all coordinates with coefficients E.coeffs.
Русский
Для последовательности X длины order определяем следующую последовательность: первые order-1 координаты сдвигаются на одну позицию, а последняя координата равна линейной комбинации координат с коэффициентами E.coeffs.
LaTeX
$$$(\text{tupleSucc}\, X)_i = \begin{cases} X_{i+1} & (i+1) < \mathrm{order} \\ \sum_{j=0}^{\mathrm{order}-1} E.coeffs_j X_j & \text{иначе} \end{cases}$$$
Lean4
/-- `E.tupleSucc` maps `![s₀, s₁, ..., sₙ]` to `![s₁, ..., sₙ, ∑ (E.coeffs i) * sᵢ]`,
where `n := E.order`. -/
def tupleSucc : (Fin E.order → R) →ₗ[R] Fin E.order → R
where
toFun X i := if h : (i : ℕ) + 1 < E.order then X ⟨i + 1, h⟩ else ∑ i, E.coeffs i * X i
map_add' x
y := by
ext i
split_ifs with h <;> simp [h, mul_add, sum_add_distrib]
map_smul' x
y := by
ext i
split_ifs with h <;> simp [h, mul_sum]
exact sum_congr rfl fun x _ ↦ by ac_rfl
