The square of an Airy solution

For a solution u of the shifted Airy equation u'' = (x − E) u (the bouncer eigenstate is u(x) = Ai(x − E)), the square w = u² satisfies the third-order linear equation w''' = 4 (x − E) w' + 2 w. This identity underlies Crandall's sum rules for the Airy zeros.

Main results

• Airy.airySq_ode: the three HasDerivAt links w → w' → w'' → w''', with w' = 2 u u', w'' = 2 u'² + 2 (x − E) u² and w''' = 4 (x − E) w' + 2 w.

References

• R. E. Crandall, On the quantum zeta function, J. Phys. A: Math. Gen. 29 (1996) 6795–6816.
• O. Vallée, M. Soares, Airy Functions and Applications to Physics, Imperial College Press (2010).

theorem Airy.airySq_ode {u u' : ℝ → ℝ} {E : ℝ} (hu : ∀ (x : ℝ), HasDerivAt u (u' x) x) (hu2 : ∀ (x : ℝ), HasDerivAt u' ((x - E) * u x) x) (x : ℝ) : HasDerivAt (fun (y : ℝ) => u y * u y) (u' x * u x + u x * u' x) x ∧ HasDerivAt (fun (y : ℝ) => 2 * u y * u' y) (2 * (u' x * u' x) + 2 * ((x - E) * (u x * u x))) x ∧ HasDerivAt (fun (y : ℝ) => 2 * (u' y * u' y) + 2 * ((y - E) * (u y * u y))) (4 * (x - E) * (2 * u x * u' x) + 2 * (u x * u x)) x

The third-order ODE for the square of an Airy solution. If u' is the derivative of u and u'' = (x-E)·u (the shifted Airy equation), then with w = u², w' = 2 u u', w'' = 2 u'² + 2(x-E)u², one has w''' = 4(x-E)w' + 2w. Returned as the three HasDerivAt links w → w' → w'' → w'''.