Series coefficients valid in any characteristic

Stream: mathlib4

[Geoffrey Irving]

For power series purposes, I'm using the definition:

/-- The `n`th coefficient of the power series of `f` -/
noncomputable def series_coeff (n : ℕ) (f : 𝕜 → E) (x : 𝕜) : E :=
  (n.factorial : 𝕜)⁻¹ • iteratedDeriv n f x

One then has the natural formulas about series operations, such as

/-- Power series multiply by convolution (i.e., as polynomials) -/
lemma series_coeff_mul [CharZero 𝕜] {f g : 𝕜 → 𝕜} {x : 𝕜} {n : ℕ} (df : ContDiffAt 𝕜 n f x)
    (dg : ContDiffAt 𝕜 n g x) :
    series_coeff n (f * g) x =
      ∑ p ∈ antidiagonal n, series_coeff p.1 f x * series_coeff p.2 g x := by

The [CharZero 𝕜] bit is annoying, though: surely there is a natural definition that works over the p-adics too? I don't actually need this: downstream all my fields will be RCLike. But it's annoying to drag about the CharZero baggage.

Is there a clean way of defining series_coeff that works over any NontriviallyNormedField, and works nicely alongside Mathlib?

[Aaron Liu]

Geoffrey Irving said:

The [CharZero 𝕜] bit is annoying, though: surely there is a natural definition that works over the p-adics too?

Pretty sure the p-adics are char zero

[Geoffrey Irving]

Sorry, of course yes, p-adics are CharZero. Actually, are there any examples of NontriviallyNormedFields of finite characteristic?

[Aaron Liu]

over a char p field, the derivative of X^p is zero so I don't see how you could

[Sébastien Gouëzel]

$\mathbb{F}_p((t))$ is the standard example, where $t$ has norm $p^{-1}$.

[Aaron Liu]

Geoffrey Irving said:

Sorry, of course yes, p-adics are CharZero. Actually, are there any examples of NontriviallyNormedFields of finite characteristic?

Try 𝕜((X)) the formal laurent series over a field 𝕜 with char p?

[Aaron Liu]

just give X a norm that's between zero and one

[Aaron Liu]

and I guess 𝕜 can have whatever norm

[Scott Carnahan]

If positive integers up to n are not all invertible, the conditions of having continuous n-fold derivatives and having “good” degree n polynomial approximations are not equivalent. The latter seems “more natural” to me, but formalizing it may require more work.

[Antoine Chambert-Loir]

To define the Taylor series of an analytic function $f$ in positive characteristic, one would need to define the “divided derivatives”, that is the expressions that play the role of $f^{(n)}(x)/n!$ (and whose existence explains why $f^{(p)}\equiv 0$ in characteristic $p$). Similar questions exist for functions from $\mathbf Z_p$ to itself where analyticity is framed in terms of the Mahler expansion.