Leray: global mild solution when $\|u_0\|_{L^2}\|\nabla u_0\|_{L^2} \le c\,\nu^2$

Open

NavierStokes.exists_mildSolutionOn_Ici_of_small

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

analysisfluid-dynamicsnavier-stokespartial-differential-equations

Leray's small-data global existence theorem, in mild form. There is an absolute constant $c>0$ such that for every viscosity $\nu>0$ and every admissible initial datum $u_0$ (IsInitialData) satisfying the scaling-invariant smallness condition

\Big(\int_{\mathbb R^3}|u_0|^2\,dx\Big)\Big(\int_{\mathbb R^3}|\nabla u_0|^2\,dx\Big) \le c\,\nu^4,

there is a velocity field $u$ that is a mild solution on the whole half-line $[0,\infty)$ (IsMildSolutionOn ν u₀ u (Set.Ici 0)): $u(0)=u_0$ , jointly $C^\infty$ on $[0,\infty)\times\mathbb R^3$ , divergence-free, with kinetic energy bounded uniformly in time and every $\|D^k u(t)\|_{L^2}$ bounded on each bounded time interval $[0,T']$ , and satisfying Kato's integral equation with integrable integrand for all $t>0$ .

This is Leray's theorem (Leray 1934, §§21–23, eq. (4.4): the solution is global when $\|u_0\|_{L^2}\|\nabla u_0\|_{L^2}$ is small compared with $\nu^2$ ), the result Fefferman cites on p. 2 ("(A) holds if $u^0$ is small in a suitable sense"). The mechanism: the energy inequality gives $\|u(t)\|_{L^2}\le\|u_0\|_{L^2}$ , and the differential inequality $\frac{d}{dt}\|\nabla u\|_{L^2}^2 \le -\nu\|\Delta u\|_{L^2}^2 + C\|\nabla u\|_{L^2}^{3}\|\Delta u\|_{L^2}$ (via the Gagliardo–Nirenberg inequality) shows $\|\nabla u\|_{L^2}$ is non-increasing once $\|u\|_{L^2}\|\nabla u\|_{L^2}\le c\nu^2$ , so the local solution never loses its $H^1$ control and extends for all time. Together with isSolutionOn_of_isMildSolutionOn it yields the mission milestone small_data_global_existence_R3.

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory

Formal statement

namespace NavierStokes
theorem exists_mildSolutionOn_Ici_of_small :
    ∃ c : ℝ, 0 < c ∧ ∀ (ν : ℝ), 0 < ν → ∀ (u₀ : Vec 3 → Vec 3), IsInitialData u₀ →
      (∫ x, ‖u₀ x‖ ^ 2) * (∫ x, gradNormSq u₀ x) ≤ c * ν ^ 4 →
      ∃ u : ℝ → Vec 3 → Vec 3, IsMildSolutionOn ν u₀ u (Set.Ici 0) := by sorry
end NavierStokes

Source

J. Leray, Sur le mouvement d'un liquide visqueux emplissant l'espace, Acta Math. 63 (1934) 193–248, https://doi.org/10.1007/BF02547354, §§21–23 (small-data global regular solutions); T. Kato, Math. Z. 187 (1984), Theorem 2 (small data). Mission context: C. Fefferman, Existence and smoothness of the Navier–Stokes equation, Clay Mathematics Institute (2000), p. 2 ('(A) holds if u⁰ is small in a suitable sense'), https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf

View graph

Leray: global mild solution when ∥u0∥L2∥∇u0∥L2≤c ν2\|u_0\|_{L^2}\|\nabla u_0\|_{L^2} \le c\,\nu^2∥u0​∥L2​∥∇u0​∥L2​≤cν2

Leray: global mild solution when $\|u_0\|_{L^2}\|\nabla u_0\|_{L^2} \le c\,\nu^2$