Formula about time derivative of pushforward of family of forms: where is it from? Proving Darboux's theorem, Hofer-Zehnder try to find, given $\omega$ a closed nondegenerate 2-form and $\omega_0$ the canonical symplectic form, a family of diffeomorphisms $\phi^t$ such that for all $t$, if $\omega_t=\omega_0+t(\omega-\omega_0)$, then $(\phi^t)^\ast\omega_t=\omega_0$, with $0\leq t\leq1$. To find them, the book tries to construct a time-dependent field $X_t$ such that $\phi^t$ is the flow of $X_t$. Differentiating the relation of $\phi^t$ and $\omega_t$ with $\omega_0$ given above, we get, according to the book:

$$0=\frac{d}{dt}(\varphi^t)^* \omega_t=(\varphi^t)^*\left\{L_{X_t}\omega_t+\frac{d}{dt}\omega_t\right\}.$$

The first equals sign is just the differentiation. It is the second equals that is obscure to me. $L_{X_t}\omega_t$ should be just the LHS, AFAIK. But then I think, $\omega_t$ also depends on $t$, so there must be a second term. I can guess the second term is $(\phi^t)^\ast\frac{d}{dt}\omega_t$, i.e. the derivative passed on the right of the pushforwards, whereas the first term should be differentiating "w.r.t. the flow". BUt still I can't see how I get that brace. How do I prove this formula really holds?
 A: When the vector field and the $2$-form are time independent I hope it is clear that:
$$(\phi^t)^*\circ\mathcal{L}_X(\omega)=\frac{\mathrm{d}}{\mathrm{d}s}(\phi^s)^*\omega\big|_{s=t}.$$
A simple change of variables $t-s$ proves this. 
Now, it is important to understand what it means to take the derivative of something which is not a function, as $(\phi^s)^*\omega$. The symbol $\frac{\mathrm{d}}{\mathrm{d}t}(\phi^t)^*\omega$ stands for the derivative of the following function: for each point $p\in M$ and pair of vector fields $Y,Z\in\mathfrak{X}(M;\mathbb{R})$ one has a smooth function:
$$\mathbb{R}\ni t\mapsto (\phi^t)^*\omega(Y,Z)(p)\in\mathbb{R},$$
and $\frac{\mathrm{d}}{\mathrm{d}t}(\phi^t)^*\omega\big|_{t=t_0}$ is the $2$-form defined by:
$$\frac{\mathrm{d}}{\mathrm{d}t}(\phi^t)^*\omega\big|_{t=t_0}(Y,Z)(p):=\frac{\mathrm{d}}{\mathrm{d}t}(\phi^t)^*\omega(Y,Z)(p)\big|_{t=t_0}.$$
Once this is clarified, the time dependent case follows. 

Update:
Let me show here how the computation works for time dependent functions.
If $f_t\in C^\infty(M;\mathbb{R})$ is a time dependent function (i.e.  $f(t,p):=f_t(p)$ defines a smooth function on $\mathbb{R}\times M$), then $((\phi^t)^*f_t)(p)=f(t,\phi^t(p))$ and $\frac{\mathrm{d}}{\mathrm{d}t}(\phi^t)^*f_t$ is obtained by computing:
\begin{align*}
\frac{\mathrm{d}}{\mathrm{d}t}((\phi^t)^*f_t)(p)\big|_{t=\tau}={}&\frac{\partial}{\partial x}f(x,y)\big|_{(x,y)=(\tau,\phi^\tau(p))}+\frac{\partial}{\partial y}f(x,y)\big|_{(x,y)=(\tau,\phi^\tau(p))}\frac{\mathrm{d}}{\mathrm{d}t}\phi^t(p)\big|_{t=\tau}={} \\
{}={}&\left(\frac{\mathrm{d}}{\mathrm{d}t}(f_t)\big|_{t=\tau}\right)\circ\phi^\tau(p)+X_\tau(f_\tau)\circ\phi^\tau(p).
\end{align*}
Therefore:
$$\frac{\mathrm{d}}{\mathrm{d}t}(\phi^t)^*f_t=(\phi^t)^*\left\{\mathcal{L}_{X_t}(f_t)+\frac{\mathrm{d}}{\mathrm{d}t}(f_t)\right\}.$$
A: CvZ's answer has done a good job. However, I wanted to add some calculations I prefer to have here. I'm posting this answer because:


*

*As CvZ noted in a comment, SX does not encourage long comment discussions, and we have already overused the comments to his/her answer, and I don't want to go to chat because I want this stuff on this page.

*Writing this stuff in a comment is anyway crazy because without displayed equations it becomes messy and because it would require far more than one comment, breaking it into pieces, besides overusing the comments even more, and thus going back to reason 1 above.


In case the comments get removed for any reasons, here are screenshots: 1 and 2, and this is the comment I referred to in point 1.
The first thing I want to do is make the proof explicit for an equation in CvZ's answer:
$$(\phi^t)^\ast\mathcal{L}_X(\omega)=\frac{d}{ds}(\phi^s)^\ast\omega\big|_{s=t}.$$
The key point here, as in the case with $X_t,\omega_t$, is to be clear about what this derivative means. We must get a 1-form, so the derivatives must take two arguments: a point and a vector tangent at that point. The derivative on the right will thus be, for any $(p,v)\in TM$, the derivative of the map $s\mapsto(\phi^s)^\ast\omega_p(v)$ evalued at $t$. This map is $\mathcal{C}^\infty$ because a 1-form must have $\mathcal{C}^\infty$ coefficients in a local basis and it is linear in its vector argument. Let us make that map even more explicit: $(\phi^s)^\ast\omega_p(v)=\omega_{\phi^s(p)}(d\phi^s(v))=\omega(\phi^s(p),d\phi^s(v))$. And we must derive it and evalue the derivative at $t$. The easiest thing here is to split $\phi^s$ as $\phi^t\circ\phi^{s-t}$, or rather $\phi^{s-t}\circ\phi^t$, then we rename $q:=\phi^t(p),w:=d\phi^t(v)$, and the map becomes $s\mapsto\omega(\phi^{s-t}(q),d\phi^{s-t}(w))$. We are deriving w.r.t $s$, but if we set $\tau:=s-t$ the derivative will be w.r.t. $\tau$ and evalued at 0, and we will have $\phi^\tau,d\phi^\tau$. So:
$$\left[\frac{d}{ds}(\phi^s)^\ast\omega\big|_{s=t}\right]_p(v)=\frac{d}{ds}\left[\omega(\phi^s(p),d\phi^s(v))\right]\big|_{s=t}=\frac{d}{d\tau}\left[\omega(\phi^\tau(q),d\phi^\tau(w))\right]\big|_{\tau=0},$$
but that RHS is exactly $(\mathcal{L}_X\omega)_q(w)$, which in turn is $((\phi^t)^\ast\mathcal{L}_X\omega)_p(v)$, so we have proved the above.
But I've already posted this as comments 1, 2, 3, 4. So why am I reposting? Well, to isolate it from the huge comment thread, but in fact the main reason for this answer is what follows. I was trying to extend CvZ's computation for functions to 1-forms, just to get an idea of how the general case of $k$-forms would be carried out, and I noticed it wasn't really all too clear what $\frac{\partial}{\partial y}\omega$ was supposed to mean. After all, the second ("$y$") argument of $\omega$ is a point on $M$, so how do I derive w.r.t. to that? I was thinking of a differential, something like $d_y\omega$. The map $\omega$, in the answer, is $\omega:\mathbb{R}\times M\to\mathbb{R}$. If $\dim M=m$, by choosing local coordinates we can make it into a function $\bar\omega:\mathbb{R}\times\mathbb{R}^m\to\mathbb{R}$. That would make me use partial derivatives w.r.t. all the $m+1$ coordinates, but in the end I would be making the derivative w.r.t. CvZ's $x$, and then a gradient w.r.t. the other coordinates, which would correspond to a differential of a function on $M$ obtained by fixing the first argument of $\omega$, i.e. considering $\omega_t(p):=\omega(t,p)$ with $t$ fixed. Oh well, he was using functions and had $f_t(p)$. So the second thing would be $df_\tau(\phi^\tau(p))$, which is a cotangent vector, applied to the tangent vector $\frac{d}{dt}\phi^t(p)\big|_{t=\tau}$, and that tangent vector is $X_\tau(p)$ by definition of flow, and $X_\tau(f_\tau)$ is precisely $df_\tau(p)(X_\tau(p))$, so we would have his equality without unclear partial derivatives, or rather with those derivatives interpreted as a differential.
I tried a similar approach for 1-forms but got stuck on a term $\frac{d}{d\tau}d\phi^\tau(v)\big|_{\tau=0}$. So I decided to go local and say well, my 1-form $\omega_t$ will locally be:
$$(\omega_t)_p(v)=\sum_{i=1}^na_i(t,p)dx^i(v).$$
Let us now explicitly write the derivative we want to compute in this local expression:
\begin{align*}
\left(\frac{d}{ds}(\phi^s)^\ast\omega_s\big|_{s=t}\right)_p(v)={}&\frac{d}{ds}[(\phi^s)^\ast\omega_s]_p(v)\big|_{s=t}=\frac{d}{ds}\omega_s(\phi^s(p),d\phi^s(v))\big|_{s=t}={} \\
{}={}&\frac{d}{ds}\sum_{i=1}^na_i(s,\phi^s(p))dx^i(d\phi^t(v))\big|_{s=t}={} \\
{}={}&\lim_{h\to0}\sum_{i=1}^n\frac{a_i(t+h,\phi^{t+h}(p))dx^i(d\phi^{t+h}(v))-a_i(t,\phi^t(p),d\phi^t(v))}{h}={} \\
{}={}&\sum_{i=1}^n\left[\lim_{h\to0}\frac{a_i(t+h,\phi^{t+h}(p))dx^i(d\phi^{t+h}(v))-a_i(t,\phi^{t+h}(p))dx^i(d\phi^{t+h}(v))}{h}\right.+{} \\
&{}+\left.\lim_{h\to0}\frac{a_i(t,\phi^{t+h}(p))dx^i(d\phi^{t+h}(v))-a_i(t,\phi^t(p))dx^i(d\phi^t(v))}{h}\right]={} \\
{}={}&\sum_{i=1}^n\frac{\partial a_i}{\partial x}(t,\phi^t(p))dx^i(d\phi^t(v))+{} \\
&{}+\sum_{i=1}^n\lim_{h\to0}\frac{a_i(t,\phi^{t+h}(p))dx^i(d\phi^{t+h}(v))-a_i(t,\phi^t(p))dx^i(d\phi^t(v))}{h}={} \\
{}={}&\sum_{i=1}^n\frac{d}{ds}a_i(\phi^t(p))\big|_{s=t}dx^i(d\phi^t(p))+{} \\
&{}+\lim_{h\to0}\frac{\omega_t(\phi^{t+h}(p),d\phi^{t+h}(v))-\omega_t(\phi^t(p),d\phi^t(v))}{h}={} \\
{}={}&\frac{d}{ds}\omega_s(\phi^t(p),d\phi^t(v))\big|_{s=t}+\lim_{h\to0}\frac{(\phi^{t+h})^\ast\omega_t(p,v)-(\phi^t)^\ast\omega_t(p,v)}{h}={} \\
{}={}&\left[(\phi^t)^\ast\frac{d}{ds}\omega_s\big|_{s=t}\right]_p(v)+\frac{d}{ds}(\phi^s)^\ast\omega_t(p,v)\big|_{s=t},
\end{align*}
but now the form $\omega_t$ no longer depends on $s$, the derivation variable, so we can behave as in the formula above, and the second term is thus $(\phi^t)^\ast\mathcal{L}_{X_t}\omega_t$, and the first term is exactly what we need to complete the formula I wanted to prove. THis is the case for 1-forms, but it is easily extended to $k$-forms, one but needs to put more vectors ($v_1,v_2,\dotsc$) and more $dx$'s ($dx^i,dx^j,d^k,\dotsc$), and wedges of course.
While I was at it, I tried to use this kind of approach to prove Cartan's magic formula for 1-forms. I know how to prove it in the general case, but I wanted to see if I could prove a special case this way, for the "fun" of it. And I got stuck. Indeed, I simplified things by removing dependency on time, so I just took a field $X$ with flow $\phi^t$ and a 1-form $\omega=\sum_{i=1}^na_idx^i$, and tried my luck. First of all, I wrote what the Lie derivative was:
\begin{align*}
(\mathcal{L}_X\omega)_p(v)={}&\frac{d}{dt}(\phi^t)^\ast\omega\big|_{t=0}\Big|_p(v)=\frac{d}{dt}[(\phi^t)^\ast\omega]_p(v)\big|_{t=0}={} \\
{}={}&\frac{d}{dt}\omega_{\phi^t(p)}(d\phi^t(v))\big|_{t=0}=\lim_{t\to0}\frac{\omega_{\phi^t(p)}(d\phi^t(v))-\omega_{\phi^0(p)}(d\phi^0(p))}{t}={} \\
{}={}&\sum_{i=1}^n\lim_{h\to0}\frac{a_i(\phi^t(p))dx^i(d\phi^t(v))-a_i(\phi^0(p))dx^i(d\phi^0(v))}{t}={} \\
{}={}&\sum_{i=1}^n\lim_{t\to0}\frac{a_i(\phi^t(p))dx^i(d\phi^t(v))-a_i(p)dx^i(d\phi^t(p))}{t}+{} \\
&{}+\sum_{i=1}^n\lim_{t\to0}\frac{a_i(p)dx^i(d\phi^t(v))-a_i(p)dx^i(v)}{t}={} \\
{}={}&\sum_{i=1}^ndx^i(v)\lim_{t\to0}\frac{a_i(\phi^t(p))-a_i(p)}{t}+\sum_{i=1}^na_i(p)\lim_{t\to0}\frac{dx^i(d\phi^t(v))-dx^i(v)}{t}={} \\
{}={}&\sum_{i=1}^nXa_i(p)dx^i(v)+\sum_{i=1}^na_i(p)\lim_{t\to0}\frac{dx^i(d\phi^t(v)-v)}{t},
\end{align*}
where I used the linearity of the $dx^i$ in the last passage, and somewhere up above the fact $\phi^0=id_M$ and $d\phi^0_p=id_{T_pM}$. Now I wrote out the terms of Cartan's formula. Remember the formula:
$$\mathcal{L}_X\omega=d(\iota_X\omega)+\iota_X(d\omega),$$
$\iota_X$ denoting the interior product with $X$, i.e. $\iota_X\omega=\omega(X)$, and $\iota_X(d\omega)=d\omega(X,\cdot)$. Let us start from the second term:
\begin{align*}
[\iota_X(d\omega)]_p(v)={}&d\omega_p(X(p),v)=d\left[\sum_{i=1}^na_idx^i)_p(X(p),v)\right]={} \\
{}={}&\sum_{i=1}^nda_i\wedge dx^i(X(p),v)=\sum_{i,j=1}^n\frac{\partial a_i}{\partial x_j}(p)(dx^j(X(p))dx^i(v)-dx^j(v)dx^i(X(p))={} \\
{}={}&\sum_{i=1}^n\left(Xa_i(p)dx^i(v)-\sum_{j=1}^n\frac{\partial a_i}{\partial x_j}(p)dx^j(v)dx^i(X(p))\right),
\end{align*}
and I just realized I had forgotten the $-$ term in these wedges, which might actually make things worse. Now, the above Lie derivative had this first term, so we need to show the other term, plus $d(\iota_X\omega)$, equals the rest of the derivative. Let us then write out the other term:
\begin{align*}
[d(\iota_X\omega)]_p(v)={}&\left[d\left(\sum_{i=1}^na_i(p)dx^i(X(p)\right)\right]_p(v)=\sum_{i=1}^n(da_i(p)(v)dx^i(X(p))+a_i(p)d(dx^i(X(p)))(v))={} \\
{}={}&\sum_{i=1}^n\left(\sum_{j=1}^n\frac{\partial a_i}{\partial x_j}(p)dx^j(v)dx^i(X(p))+a_i(p)\sum_{j=1}^n\frac{\partial dx^i(X(p))}{\partial x_j}(p)dx^j(v)\right).
\end{align*}
And another term I had forgotten to consider might get me done with this. So now the first term here cancels the $-$ term above, and Cartan's formula reduces to:
$$\sum_{i=1}^na_i(p)\lim_{t\to0}\frac{dx^i(d\phi^t(v)-v)}{t}=\sum_{i=1}^na_i(p)\sum_{j=1}^n\frac{\partial dx^i(X(p))}{\partial x_j}(p)dx^j(v).$$
I believe the LHS limits coincide with the RHS internal sums. So I will write that out, and undo the use of linearity of $dx^i$ I did above on the LHS:
$$\lim_{t\to0}\frac{dx^i(d\phi^t(v))-dx^i(v)}{t}=\sum_{j=1}^n\frac{\partial dx^i(X(p))}{\partial x_j}(p)dx^j(v).$$
This must hold for all $i=1,\dotsc,n$. The LHS is $\mathcal{L}_Xdx^i$. What about the RHS? Well, it's $d(\iota_Xdx^i)_p(v)$. How do I prove the equality? Basically the above is a reduction of the proof Cartan's formula to proving it for $dx^i$'s, since $ddx^i=0$ so the formula would say $\mathcal{L}_Xdx^i=d(\iota_Xdx^i)+\iota_X(ddx^i)=d(\iota_Xdx^i)+\iota_X(0)$, which is the above. Let me save this much and think about this.
