A mild solution satisfies Fefferman’s strict bounded-energy condition

Proved

NavierStokes.strictEnergyBound_of_isMildSolutionOn

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

analysisfluid-dynamicsnavier-stokespartial-differential-equations

Let $u$ be a mild Navier–Stokes solution on a set of times $S$ . Then there is a real constant $C$ such that

\int_{\mathbb R^3}\lVert u(t,x)\rVert^2\,dx<C \qquad\text{for every }t\in S.

This packages the non-strict uniform energy bound recorded by the mild-solution structure into the strict bounded-energy condition used by Fefferman’s notion of a physically reasonable solution.

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib
open scoped ContDiff Gradient
open Laplacian MeasureTheory

Formal statement

namespace NavierStokes
theorem strictEnergyBound_of_isMildSolutionOn (ν : ℝ) (u₀ : Vec 3 → Vec 3)
    (u : ℝ → Vec 3 → Vec 3) (S : Set ℝ)
    (hu : IsMildSolutionOn ν u₀ u S) :
    ∃ C : ℝ, ∀ t ∈ S, ∫⁻ x, ‖u t x‖ₑ ^ 2 < ENNReal.ofReal C := by sorry
end NavierStokes

Source

C. L. Fefferman, Existence and smoothness of the Navier–Stokes equation, Clay Mathematics Institute (2000), https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf, p. 1, condition (7). Exact formal context: Prove2Me definition NavierStokes_Mild, theorem id 22ac75d3-ebba-403c-ad68-a493ac2dd884, field IsMildSolutionOn.energy.

View graph