Skip to content

README.md

Latest commit

 

History

History
22 lines (13 loc) · 630 Bytes

README.md

File metadata and controls

22 lines (13 loc) · 630 Bytes
Raw

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.