Uniform energy bound for a global smooth two-dimensional Navier–Stokes solution

Open

NavierStokes.boundedEnergy_of_global_smooth_core_R2

by Yuning · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

analysisenergy-estimatefluid-dynamicsnavier-stokespartial-differential-equations

Let $u,p$ be a global smooth solution of the two-dimensional incompressible Navier–Stokes equations with positive viscosity and admissible initial velocity $u_0$ . Then its kinetic energy is uniformly bounded: there is a finite constant $C$ such that

\int_{\mathbb R^2}|u(t,x)|^2\,dx<C\qquad(t\ge0).

The estimate comes from pairing the momentum equation with $u$ . The divergence-free condition makes the convection term and pressure term integrate to zero, while integration by parts turns the viscous term into $-\nu\int|\nabla u|^2$ . Consequently the kinetic energy is nonincreasing. This statement isolates the analytic justification of those integrations, including spatial decay or approximation arguments, from construction of the smooth solution itself.

Preamble

import Definitions.Def_NavierStokes
import Mathlib

Formal statement

namespace NavierStokes

open scoped ContDiff InnerProductSpace Gradient
open Laplacian MeasureTheory

theorem boundedEnergy_of_global_smooth_core_R2
    (ν : ℝ) (hν : 0 < ν) (u₀ : Vec 2 → Vec 2) (h₀ : IsInitialData u₀)
    (u : ℝ → Vec 2 → Vec 2) (p : ℝ → Vec 2 → ℝ)
    (hsmooth_u : ContDiffOn ℝ ∞ (Function.uncurry u) (Set.Ici 0 ×ˢ Set.univ))
    (hsmooth_p : ContDiffOn ℝ ∞ (Function.uncurry p) (Set.Ici 0 ×ˢ Set.univ))
    (hmomentum : ∀ t ∈ Set.Ici (0 : ℝ), 0 < t → ∀ x,
      deriv (fun s => u s x) t + fderiv ℝ (u t) x (u t x) =
        ν • Laplacian.laplacian (u t) x - gradient (p t) x)
    (hspatial : ∀ t ∈ Set.Ici (0 : ℝ), IsInitialData (u t))
    (hinitial : u 0 = u₀) :
    ∃ C : ℝ, ∀ t ∈ Set.Ici (0 : ℝ),
      ∫⁻ x, ‖u t x‖ₑ ^ 2 < ENNReal.ofReal C := by sorry

end NavierStokes

Source

O. A. Ladyzhenskaya, The Mathematical Theory of Viscous Incompressible Flow, 2nd ed. (1969), energy estimate for incompressible Navier–Stokes; C. L. Fefferman, Clay Navier–Stokes problem description (2000), equations (1), (2), and condition (7).

View graph