order and leading coefficient of analytic functions

Stream: mathlib4

[Geoffrey Irving]

Given an analytic function at a point, https://github.com/girving/ray/blob/main/Ray/Analytic/Analytic.lean defines orderAt to be the least n s.t. the nth power series coefficient is nonzero, and leadingCoeff to be that nonzero coefficient. Currently both are defined only for 1D power series:

/-- The order of a zero at a point.
    We define this in terms of the function alone so that expressions involving order can
    depend only on `f`. -/
def orderAt (f : 𝕜 → E) (c : 𝕜) : ℕ :=
  if p : AnalyticAt 𝕜 f c then (choose p).order else 0

/-- The leading nonzero coefficient of `f`'s power series -/
def leadingCoeff (f : 𝕜 → E) (c : 𝕜) : E :=
  ((Function.swap dslope c)^[orderAt f c]) f c

I also prove a variety of lemmas about that, such as that factoring out a monomial power does what one expects.

1. Do these already exist?
2. If not, should I upstream them in some form?

I think the formulations are a bit weird unless one is living only in analytic function land: I could certainly define them more generally to apply to not-necessarily-analytic functions. So I expect if I should upstream them, I need to refactor a significant amount first.

[Vincent Beffara]

There is docs#HasFPowerSeriesAt.iterate_dslope_fslope_ne_zero which would benefit from leadingCoeff, and docs#HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope is a factoring.

About generalizing, what would make more sense, setting it to 0 if the function is not analytic, or doing some complicated incantations so that a C^5 functions can e.g. have order 3 it its first few derivatives vanish?

[Geoffrey Irving]

I'm not sure about the generalizations: one problem is that nonanalytic functions can vanish to fractional orders (or worse). But it does seem pretty annoying if the definition doesn't apply to just differentiable functions at least some of the time.