Lie derivative w.r.t. time-dependent field Some time ago, I asked this question. CvZ answered, and with my additional answer I thought I had solved the problem. Yesterday evening, I copied those calculations into my thesis, and having $t$ and $s$ exchanged, I found myself in trouble as to whether I should have $\mathcal{L}_{X_t}$ or $\mathcal{L}_{X_s}$. This morning, I found this question, but it did not solve my problems, and actually it sparked more problems. It did confirm my problems were not only over-thinking. Now I have this time-dependent field $X_t$. I can defined its flow $\phi^s$ in the same way as always, i.e. by:
$$\frac{d}{ds}\phi^s(p)\Big|_{s=t}=X_t(\phi^t(p)),\qquad\phi^0=id.$$
This way, when I take $x(s)=\phi^s(p)$, I follow an integral curve of the field $X_t$. I can then define the Lie derivative along $X_t$ as:
$$\mathcal{L}_{X_t}\omega=\frac{d}{ds}(\phi^s)^\ast\omega\Big|_{s=0}.$$
But then, as the poster of the question I found this morning (second link) notices, $\mathcal{L}_{X_t}$ seems to be independent of $t$, i.e. for all $t,s\in\mathbb{R}$ it seems $\mathcal{L}_{X_t}=\mathcal{L}_{X_s}$ as an operator. Yet as soon as I try Cartan's formula I get an equality of this operator with something clearly time-dependent. My attempt to fix this brought me to something close to the poster of the above mentioned question. Precisely, I thought of $X_t$ as a family of fields, and defined a flow for each. So I ended up with $\phi^{s,t}$ satisfying:
$$\frac{d}{ds}\phi^{s,t}(p)\Big|_{s=\tau}=X_\tau(\phi^{\tau,t}(p)),\qquad\phi^{0,\tau}=id.$$
This is pretty different from what the poster of the question did, because he required $\phi^{s,s}=0$ for all $s$, not $\phi^{0,s}$. So I was wondering why he did that. I also found this other question. There, it is suggested in a comment to lift everything up to $M\times\mathbb{R}$ and apply Cartan over there. Which is basically identical to my approach, including the requirement, since we will then have a flow over there which satisfies $\phi^0(t,p)=(t,p)$ for all $(t,p)$, so going back down with two-parameter flows we have $\phi^{0,t}(p)=p$ for all $t$. But if all this is really necessary, why did Hofer-Zehnder completely gloss over this in the proof of Darboux's theorem on symplectic manifolds? I mean, doing all this really seems like inventing an alternate proof in the attempt to explain an existing one…
 A: Nobody answered. My teacher gave me some explanation. I trusted him. I let the problem fall. Now I'm back on it to prepare the presentation for my thesis. I thought about it, and here is the explanation I've come up with. With any field $X$ on a manifold $M$, it makes sense to define a two-index family of diffeomorphisms $\phi_s^t$, where $\phi_s^t(x)$ is where you end up at time $t$ if you are in $x$ at time $s$. We can then define:
$$\mathcal L_{X_s}\omega=\frac{d}{dt}(\phi_s^t)^\ast\omega\Big|_{t=s}.$$
This is the Lie derivative along a field that evolves like $X$, only reparametrizing time in such away that what $X$ sees as time $s$ is seen by this field as time 0. So I can call this field $X_s$. Naturally, if $X$ is constant, all these derivatives are identical, and $X_s\equiv X$. What this double index is useful for is when $X$ actually evolves. It is easy to see that, for any $t,s,u$:
$$\phi_s^t\circ\phi_u^s=\phi_u^t.$$
The LHS means you start in $x$ at $u$, and move till time $s$, then you call $y$ the result, and see where you end up at time $u$ if you start at $y$ at time $s$. The RHS does the two steps in one: start in $x$ at $u$ and see where you are in $t$. Of course, when the field is time-independent, this reduces to $\phi_0^t\circ\phi_0^s=\phi_0^{t+s}$, for the LHS's first function is $\phi_s^{t+s}$. That is, if $X$ does not evolve in time, $\phi_s^t=\phi_{u+s}^{u+t}$ for all $u\in\mathbb{R}$. Again, this changes in the time-dependent case.
With that in mind, we move to solving the problem that sparked this question. We have the family $\omega_t=\omega_0+t(\omega-\omega_0)$. We need to find $\phi^t:(\phi^t)^\ast\omega_t\equiv\omega_0$. We try to build a time-dependent $X$ such that:
$$(\phi_0^t)^\ast\omega_t\equiv\omega_0.$$
Deriving this at any time $s$ we have to get 0. But then:
\begin{align*}
\frac{d}{dt}\Big|_{t=s}(\phi_0^t)^\ast\omega_t={}&\lim_{h\to0}\frac{(\phi_0^{s+h})^\ast\omega_{s+h}-(\phi_0^s)^\ast\omega_s}{h}={} \\
{}={}&\lim_{h\to0}\frac{(\phi_0^{s+h})^\ast\omega_{s+h}-(\phi_0^s)^\ast\omega_{s+h}}{h}+\lim_{h\to0}\frac{(\phi_0^s)^\ast\omega_{s+h}-(\phi_0^s)^\ast\omega_s}{h}={} \\
{}={}&\lim_{h\to0}\frac{(\phi_s^{s+h}\circ\phi_0^s)^\ast\omega_{s+h}-(\phi_0^s)^\ast\omega_{s+h}}{h}+(\phi_0^s)^\ast\frac{d}{dt}\Big|_{t=s}\omega_t={} \\
{}={}&(\phi_0^s)^\ast\lim_{h\to0}\frac{((\phi_s^{s+h})^\ast-(\phi_s^s)^\ast)\omega_{s+h}}{h}={} \\
{}={}&(\phi_0^s)^\ast\left\{\mathcal{L}_{X_s}\omega_s+\frac{d}{dt}\omega_t\Big|_{t=s}\right\}.
\end{align*}
And this, except for a couple more indices, is precisely the desired formula. The proof I have of Cartan's magic formula readily generalizes to this case, so I am finally done on this.
Update
No. Cartan doesn't work as I expected, but rather I managed to show $\mathcal{L}_{X_s}$ as above define doesn't depend on $s$! It always gives $d\iota_{X_0}+\iota_{X_0}d$, where $X_0$ is the field at time 0. I'm really giving up on this. There is NO FUCKING WAY I can set that proof of Darboux straight, because Hofer's way I can justify neither the use of Cartan nor the passage in which $\mathcal{L}_{X_s}$ pops up, nor indeed how I define that derivative. The above way has no Cartan. The field family way (trying to construct a family of fields $X_t$ with flows with two indices, so $X_s$ would have flow $\phi_s^t$) gives a damn $\mathcal{L}_{X_s}\omega_u+\frac{d}{dt}\omega_t\Big|_{t=u}$, so having me conclude all fields are equal. I'm leaving this answer as an attempt to solve the problem, but it didn't solve it AT ALL. It just provided a third non-solution.
Update 2
Turns out all I had to do was define $\mathcal{L}_{X_s}$ in an arbitrary way so as to get the formula, and them prove a "Cartan formula" for $\mathcal{L}_{X_s}$ so defined, to get to the end without too much trouble. And the proof of this "Cartan formula" was identical to that for the real Cartan formula, the one with no time dependency. So I set this proof straight at last.
