Skip to content
DraconiticResearch
Search Sources API
203,234 studies31 sourcesUpdated 23 min ago
PreprintCC BY 4.0arXiv

Formalization of the Galerkin Construction for the Two-Dimensional Navier--Stokes Equations in Lean

  • Weinan Wang
Open at sourcePDFDOICite

Abstract

We formalize in Lean 4 the Galerkin construction of global Leray--Hopf weak solutions for the unforced two-dimensional Navier--Stokes equations on arbitrary bounded open domains with no-slip boundary conditions. For every initial datum in the solenoidal L2 velocity space, the solution has a weakly continuous velocity path, satisfies the weak equation locally in time, and obeys the energy inequality at every time. For rectangles, we also formalize finite-horizon solutions with continuous forcing in the dual energy space. The development includes divergence-free graph spaces, compact spectral coordinates, transport cancellation, Ladyzhenskaya estimates, and simultaneous space--time compactness. The abstract Hilbert-space results apply to evolution equations with a compact energy-to-velocity embedding and a skew trilinear nonlinearity.

Related

  1. Global Regularity for the 3D Incompressible Navier–Stokes Equations via the Frohmanian Symplectic Tether: Lean 4 Formalization and Conditional Cubic Comparison Framework (v2.1)
    Benjamin Frohman
    Zenodo (CERN European Organization for Nuclear Research)PreprintLicence not stated6 citedGeneral mathematicsOpenAlex
  2. The Generative Mechanism of Dimension: An Axiomatic Construction of Dimensional Conventions (Constructive Mathematics Series, Paper 6; Lean formalization, model-pair independence, numerical evidence)
    Chao Qin
    Zenodo (CERN European Organization for Nuclear Research)PreprintCC BY8 citedGeometry & topologyOpenAlex
  3. The sharp CFL condition of the piecewise constant sparse grid discontinuous Galerkin method for high-dimensional transport equations
    Juntao Huang
    arXivPreprintCC BY 4.0Full textNumerical analysis & scientific computingComputational physicsarXiv
  4. A Viscous Cascade Construction of Nonunique Leray--Hopf Solutions to the Unforced 3D Navier--Stokes Equations
    Thomas Y. Hou, Xiang Qin, Peicong Song +1
    arXivPreprintarXiv licenceFull textAnalysis & PDEsarXiv
  5. Ergodicity for the Two-Dimensional Stochastic Navier-Stokes Equations with Shear-Thickening Viscosity
    Christopher Bunting
    arXivPreprintarXiv licenceFull textProbabilityarXiv

Cite

BibTeXRIS
BibTeX
@misc{wang2026formalization,
  title = {{Formalization of the Galerkin Construction for the Two-Dimensional Navier--Stokes Equations in Lean}},
  author = {Weinan Wang},
  howpublished = {arXiv},
  year = {2026},
  month = sep,
  doi = {10.48550/arxiv.2609.33033},
  eprint = {2609.33033},
  archivePrefix = {arXiv},
  url = {https://arxiv.org/abs/2609.33033},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - Formalization of the Galerkin Construction for the Two-Dimensional Navier--Stokes Equations in Lean
AU  - Weinan Wang
PY  - 2026
DA  - 2026/09/27
PB  - arXiv
DO  - 10.48550/arxiv.2609.33033
UR  - https://arxiv.org/abs/2609.33033
AB  - We formalize in Lean 4 the Galerkin construction of global Leray--Hopf weak solutions for the unforced two-dimensional Navier--Stokes equations on arbitrary bounded open domains with no-slip boundary conditions. For every initial datum in the solenoidal L^2 velocity space, the solution has a weakly continuous velocity path, satisfies the weak equation locally in time, and obeys the energy inequality at every time. For rectangles, we also formalize finite-horizon solutions with continuous forcing in the dual energy space. The development includes divergence-free graph spaces, compact spectral coordinates, transport cancellation, Ladyzhenskaya estimates, and simultaneous space--time compactness. The abstract Hilbert-space results apply to evolution equations with a compact energy-to-velocity embedding and a skew trilinear nonlinearity.
ER  -