Linear combinations of $$t^ke^{λt}$$

Stream: maths

[Yury G. Kudryashov]

I'm going to add some facts about functions of the form $f(t)=\sum_j a_jt^{k_j}e^{λ_jt}$. Two use cases I have in mind are

• solutions of linear differential equations $\dot x(t)=Ax(t)+f(t)$;
• they naturally appear as partial sums of asymptotic series expansion of the correspondence map of a hyperbolic saddle point.

I have a few questions:

1. How should I call them? I saw the name "quasi polynomials" in some sources (mostly in Russian) but wiki disagrees.

2. How general should be the definition? I know about applications in these cases:

   • all $a_j$, $λ_j$, and $t$ are numbers (real or a complex);
   • $a_j$ is a matrix, $λ_j$ and $t$ are real or complex numbers;
   • $a_j$ and $t$ are numbers, $λ_j$ is a matrix (actually, it is $λ_jA$).

[Kevin Buzzard]

Is this finite sums you're talking about?

[Yury G. Kudryashov]

Yes.

[Yury G. Kudryashov]

Let me elaborate on applications.

Linear ODEs

If $A$ is a matrix with eigenvalues $λ_j$ with multiplicities $r_j$, then $x(t)=e^{At}x(0)$. If we rewrite this in coordinates, $x_k(t)=\sum_j P_{k,j}(t)e^{λ_jt}$, where $P_{k,j}$ is a polynomial of degree at most $r_j-1$.

Dulac series

Let $Δ\colon (\mathbb R_+, 0) → (\mathbb R_+, 0)$ be the correspondence map of an analytic hyperbolic saddle and $F(t)=-\ln Δ(e^{-t})$, $F\colon (\mathbb R_+, \infty)\to(\mathbb R_+, \infty)$, be the same map written in the logarithmic chart. Then for each $Λ>0$ we have

$$F(t)=at+b+\sum_{j=1}^{N(Λ)} P_j(t)e^{-λ_jt}+o(e^{-Λt})$$

as $t\to\infty$, where $0<λ_j\le Λ$ and $P_j$ are polynomials. The functions in the RHS can be glued into an asymptotic series

$$at+b+\sum_{j=1}^∞ P_j(t)e^{-λ_jt}.$$

This series may diverge but it is an asymptotic series for $F$.

Moreover, the same asymptotic expansion holds true in the image $\Omega_C$ of the complex right half-plane under the map $z\mapsto z+C\sqrt{1+z}$ for sufficiently large positive $C$. The latter fact together with a special version of the Phragmen-Lindelöf principle implies that the Poincaré map of a hyperbolic polycycle is either the identity map, or has an isolated fixed point at zero (Ilyashenko, about 1990).

[Eric Wieser]

Note I've made a bunch of progress on matrix exponentials specifically with (the first half of) that first example in mind

[Yury G. Kudryashov]

My main goal is the second application but IMHO we should have a definition that works in both cases.

[Yury G. Kudryashov]

For the second application, I want to have theorems like

$$\sum_{j=1}^{N}P_j(t)e^{-λ_jt} = a_1t^{d_1}e^{-λ_1t}+o(t^{d_1}e^{-λ_1t})$$

as $t\to\infty$, where $a_1t^{d_1}$ is the leading term of $P_1(t)$ and $λ_1>λ_2>…$

[Yury G. Kudryashov]

Actually, I need this as re t → ∞ or abs t → ∞ while $t∈\Omega_C$.

[Yury G. Kudryashov]

#13178 is ready for review; this kind of quasi polynomials is the next item on my Lean TODO list. Any ideas about the name and typeclass assumptions?