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

URI	`m2://res/AJWBAHJ8VD`
Kind	preprint
Creators	Weinan Wang
Date	2026-09-27
MSC	35-XX
Subjects	arxiv math.AP
Scope	in

Expressions

e1: version, preprint

Language	en
Date	2026-09-27
Ids	arXiv 2609.33033

Items in this resource

The mentions of the inventory that name this resource. Each name links to the card of its inventory row.

Item	Kind	Where	Source
Galerkin projectors from a Hilbert basis	statement	proposition 7.1	arxiv
Two-dimensional Ladyzhenskaya estimate and convection form	statement	proposition 5.4	arxiv
Reduction to a vector-valued Rellich embedding	statement	proposition 5.6	arxiv
Global solution on a bounded open domain	statement	theorem 2.1	arxiv
Unforced two-dimensional Leray--Hopf solution	statement	theorem 2.2	arxiv
Unforced spectral Galerkin solutions	statement	proposition 6.3	arxiv
Poincar\'e inequality and forcing estimate on a rectangle	statement	proposition 5.5	arxiv
Two-dimensional spectral dual estimate	statement	proposition 6.2	arxiv
Scalar Rellich compactness on rectangles	statement	proposition 5.8	arxiv
Energy and velocity spaces on a rectangular domain	statement	proposition 5.3	arxiv
Finite-mode regularity from a dual \(L^2\) derivative	statement	proposition 6.4	arxiv
Singular-value bases for a compact embedding	statement	proposition 5.10	arxiv
Finite-dimensional variational Galerkin theorem	statement	theorem 6.1	arxiv
Forced spectral Galerkin solutions	statement	theorem 9.1	arxiv
Spectral Galerkin spaces on a rectangular domain	statement	proposition 5.11	arxiv
Finite-dimensional transport cancellation	statement	proposition 5.2	arxiv
Reduction to scalar Rellich compactness	statement	proposition 5.7	arxiv
Forced two-dimensional Leray--Hopf solution	statement	theorem 2.3	arxiv
Transport integration by parts on a rectangular domain	statement	proposition 5.1	arxiv
Compact Gelfand triple and Galerkin energy bound	statement	proposition 5.9	arxiv
Spectral compactness in \(L^2(I;H)\	statement	theorem 7.2	arxiv

Catalogue records

arxiv: 2609.33033 (work)
arxiv_text: 2609.33033 (work)