The Airy equation for formal power series

The power-series solutions y = Σ cₖ xᵏ of the Airy equation y'' = x y satisfy (k + 2)(k + 1) c_{k+2} = c_{k-1} and c₂ = 0, i.e. c_{k+3} = cₖ / ((k + 2)(k + 3)) with c₀, c₁ free. This file defines these coefficients over ℚ and proves that the resulting power series satisfies d²/dX² y = X · y in ℚ⟦X⟧.

Main results

• Airy.coeff: the coefficients with y(0) = c0, y'(0) = c1; Airy.f, Airy.g the two standard solutions (c0, c1 = 1, 0 and 0, 1).
• Airy.coeff_airy_ode: d⁄dX (d⁄dX (mk (coeff c0 c1))) = X * mk (coeff c0 c1).
• Airy.Fps_airy, Airy.Gps_airy: the same for the two standard solutions.

The real-analytic function, its entireness and its zeros are in Formalizations.Analysis.SpecialFunctions.Airy.Basic.

References

• NIST Digital Library of Mathematical Functions, Chapter 9 (Airy and Related Functions), https://dlmf.nist.gov/9.
• O. Vallée, M. Soares, Airy Functions and Applications to Physics, Imperial College Press (2010).
• C. Marín, How a Falling Particle Counts Its Floors: the Airy function as a verified entire solution of y''=xy, its oscillation, and the quantum-bouncer spectrum, machine-checked in Lean 4 (2026), doi:10.5281/zenodo.20787671. Ported from Airy.lean of karlesmarin/airy-bouncer-lean (Lean v4.30.0-rc2).

def Airy.coeff (c0 c1 : ℚ) : ℕ → ℚ

Power-series coefficients of a solution of y''=xy with y(0)=c0, y'(0)=c1.

Equations

• Airy.coeff c0 c1 0 = c0
• Airy.coeff c0 c1 1 = c1
• Airy.coeff c0 c1 2 = 0
• Airy.coeff c0 c1 k.succ.succ.succ = Airy.coeff c0 c1 k / ((↑k + 2) * (↑k + 3))

def Airy.f (k : ℕ) : ℚ

First entire solution f: f(0)=1, f'(0)=0. f = 1 + x³/6 + x⁶/180 + x⁹/12960 + ⋯

Equations

• Airy.f k = Airy.coeff 1 0 k

def Airy.g (k : ℕ) : ℚ

Second entire solution g: g(0)=0, g'(0)=1. g = x + x⁴/12 + x⁷/504 + ⋯

Equations

• Airy.g k = Airy.coeff 0 1 k

theorem Airy.coeff_two (c0 c1 : ℚ) : coeff c0 c1 2 = 0

Definitional base case: c₂ = 0.

theorem Airy.coeff_succ3 (c0 c1 : ℚ) (k : ℕ) : coeff c0 c1 (k + 3) = coeff c0 c1 k / ((↑k + 2) * (↑k + 3))

Definitional recurrence: c_{k+3} = c_k / ((k+2)(k+3)).

noncomputable def Airy.Fps : PowerSeries ℚ

The two entire solutions of y''=xy, as power series over ℚ.

Equations

• Airy.Fps = PowerSeries.mk (Airy.coeff 1 0)

noncomputable def Airy.Gps : PowerSeries ℚ

The second standard solution of y''=xy, as a power series over ℚ.

Equations

• Airy.Gps = PowerSeries.mk (Airy.coeff 0 1)

theorem Airy.coeff_airy_ode (c0 c1 : ℚ) : PowerSeries.derivative (PowerSeries.derivative (PowerSeries.mk (coeff c0 c1))) = PowerSeries.X * PowerSeries.mk (coeff c0 c1)

The Airy equation y'' = x·y, verified at the power-series level, for the solution with y(0)=c0, y'(0)=c1.

theorem Airy.Fps_airy : PowerSeries.derivative (PowerSeries.derivative Fps) = PowerSeries.X * Fps

theorem Airy.Gps_airy : PowerSeries.derivative (PowerSeries.derivative Gps) = PowerSeries.X * Gps

Examples: the classical series f = 1 + x³/6 + x⁶/180 + x⁹/12960 + ⋯,

g = x + x⁴/12 + x⁷/504 + ⋯.