English
There is an explicit expression for frobeniusPolyAux(p,n) as X(n+1) minus a double sum over indices i and j of products involving X(i), frobeniusPolyAux(p,i), and binomial-type coefficients.
Русский
Существуют явное выражение frobeniusPolyAux(p,n) как X(n+1) минус двойной суммы по i и j, включающей X(i), frobeniusPolyAux(p,i) и биномиальные коэффициенты.
LaTeX
$$$\text{frobeniusPolyAux}(p,n) = X(n+1) - \sum_{i=0}^{n-1} \sum_{j=0}^{p^{n-i}-1} (X(i)^{p})^{p^{n-i}-(j+1)} \cdot (\text{frobeniusPolyAux}(p,i))^{(j+1)} \cdot C(\text{...}).$$$
Lean4
theorem frobeniusPolyAux_eq (n : ℕ) :
frobeniusPolyAux p n =
X (n + 1) -
∑ i ∈ range n,
∑ j ∈ range (p ^ (n - i)),
(X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * ↑p ^ (j - v p (j + 1)) : ℕ) :=
by rw [frobeniusPolyAux, ← Fin.sum_univ_eq_sum_range]
