Until further notice regard F etc. as depending on RMS square slowness u rather than on interval velocity v. Dependence on v, through the relatively easily analyzed map , will be reintroduced at the end.
A short calculation shows that
Introduce the quantity , with units of time:
That is, is the zero offset time for which the time at offset x is the same in the slowness u as the time one obtains for t0,x in slowness u*.
Then introducing the expression for p, and changing variables from t to t0 in the integral above, yields
depends only on u* and .
It is now straightforward to compute the first order perturbation of J0 with respect to u. First,
Putting this all together,
depends on u, u*, and .To compute the gradient, change variables again to for each x. Since
Thus the L2 gradient of J0 is
Both expressions for J0 and its gradient suggest that these quantities are comparing the trial square slowness u and the target square slowness u* at different points (eg. t0 vs. ), and this in turn makes understanding of the implications for determination of u difficult. Fortunately this is not really the case:
Key Lemma: There exists a function h(t0,x), depending on velocity v (or slowness u) and also on u* and , having the following properties:
Proof of Key Lemma: Note first that since
It follows that since
This simple integral equation has the solution
has the properties claimed for it in the statement of the lemma. Q.E.D.
Now changing variables in the asymptotic formula for J0, and applying the above relation to both this and the formula for , you obtain
Now B0* and B1* differ at each point in the mute zone by factors or divisors of s, s*, T, and the like, and these are bounded over the mute zone uniformly in . Therefore there exists a constant C>0 depending only on for which
and we have proved the
Theorem: If u, the RMS square slowness for ,is a stationary point of J0[u], then .
That is, for noise free data, any stationary point of J0 is a global minimizer, up to an asymptotically vanishing error.