Lean 4 + mathlib formalization of the SQG shear-vorticity identity (D14 Theorem 1)
theorem-proving partial-differential-equations formalization fluid-dynamics mathematical-physics mathlib harmonic-analysis regularity-theory sqg lean4 quasi-geostrophic sobolev-spaces
-
Updated
Jul 5, 2026 - Lean