Oscillatory integrals in Lean

This is a project on formalizing some of the standard theory on oscillatory integrals in Lean 4.

Completed

• The classical van der Corput lemma on the real line

  Oscillatory.norm_integral_exp_mul_I_le_of_order_one

  Oscillatory.norm_integral_exp_mul_I_le_of_order_ge_two

Future Goals

• sublevel set estimates
• van der Corput variants in higher dimensions
• oscillatory integral operators, Hörmander's theorem
• stationary phase principle

References

Elias M. Stein. Harmonic Analysis: Real-Variable Methods, Orthogonality, and Oscillatory Integrals.