Prove2Me

Kato: global mild solution for small critical L3L^3 data

Open
NavierStokes.exists_mildSolutionOn_Ici_of_eLpNorm_three_small

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

analysisfluid-dynamicsnavier-stokespartial-differential-equations

There is an absolute constant ε>0\varepsilon>0 such that, for every viscosity ν>0\nu>0 and every admissible divergence-free initial field u0u_0 on R3\mathbb R^3,

∥u0∥L3≤εν\|u_0\|_{L^3}\le \varepsilon\nu

implies the existence of a mild Navier–Stokes solution on the full half-line [0,∞)[0,\infty). The solution satisfies the mission bundle’s Duhamel equation, smoothness, divergence-free, energy, Sobolev, and integrability requirements.

This is the scale-critical small-data theorem that supplies global existence after the preceding interpolation lemma.

Preamble
import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory
Formal statement
namespace NavierStokes
theorem exists_mildSolutionOn_Ici_of_eLpNorm_three_small :
    ∃ ε : ℝ, 0 < ε ∧ ∀ (ν : ℝ), 0 < ν → ∀ (u₀ : Vec 3 → Vec 3), IsInitialData u₀ →
      eLpNorm u₀ 3 volume ≤ ENNReal.ofReal (ε * ν) →
      ∃ u : ℝ → Vec 3 → Vec 3, IsMildSolutionOn ν u₀ u (Set.Ici 0) := by sorry
end NavierStokes
Source
T. Kato, Strong L^p-solutions of the Navier–Stokes equation in R^m, with applications to weak solutions, Math. Z. 187 (1984), 471–480, https://doi.org/10.1007/BF01174182, Theorem 2 with m=p=3; smooth admissible data specialization. Mission context: C. L. Fefferman, Clay problem description (2000), p. 2, https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf.

View graph