Classical Fourier analysis in Lean 4: Littlewood–Paley, paraproducts, Kato–Ponce commutator, Sobolev embeddings for 𝕋². Upstream of sqg-lean-proofs and future NS/Euler/MHD formalizations.
theorem-proving partial-differential-equations formalization fourier-analysis mathematical-physics mathlib harmonic-analysis lean4 sobolev-spaces littlewood-paley paraproducts kato-ponce
-
Updated
Apr 23, 2026 - Lean