Kato: local existence of a mild solution on $[0,T)$ for smooth decaying data

Open

NavierStokes.exists_mildSolutionOn_Ico

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

analysisfluid-dynamicsnavier-stokespartial-differential-equations

Kato's local existence theorem, in mild form. Let $\nu>0$ and let $u_0$ be admissible initial data (IsInitialData: $C^\infty$ , divergence-free, with all derivatives decaying faster than any power of $|x|$ ). Then there is a time $T>0$ and a velocity field $u$ which is a mild solution of the Navier–Stokes equations on $[0,T)$ (IsMildSolutionOn ν u₀ u (Set.Ico 0 T)): $u(0)=u_0$ , $u$ is jointly $C^\infty$ on $[0,T)\times\mathbb R^3$ , divergence-free, with kinetic energy bounded on $[0,T)$ and every $\|D^k u(t)\|_{L^2}$ bounded on $[0,T)\cap(-\infty,T']$ for each $T'$ , and $u$ satisfies Kato's integral equation

u(t) = e^{\nu t\Delta}u_0 - \int_0^t e^{\nu(t-s)\Delta}\,P\big((u(s)\cdot\nabla)u(s)\big)\,ds, \qquad 0<t<T,

with an integrable integrand.

This is the fixed-point half of the Kato–Fujita theory (Fujita–Kato 1964, Theorem 4.1; Kato 1984, Theorem 1 with $m=3$ ), specialised to smooth rapidly decaying data: a contraction argument in $C([0,T];H^1)$ (or $C([0,T];L^3)$ ) gives a unique mild solution for $T \gtrsim \nu^3/\|\nabla u_0\|_{L^2}^4$ , and the standard bootstrap shows it lies in $C([0,T'];H^k)$ for every $k$ and $T'<T$ and is jointly smooth up to $t=0$ . Together with isSolutionOn_of_isMildSolutionOn it yields the mission milestone local_existence_R3 (Fefferman, p. 2: statement (A) on a small time interval).

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

Formal statement

namespace NavierStokes
theorem exists_mildSolutionOn_Ico (ν : ℝ) (hν : 0 < ν) (u₀ : Vec 3 → Vec 3)
    (h₀ : IsInitialData u₀) :
    ∃ T : ℝ, 0 < T ∧ ∃ u : ℝ → Vec 3 → Vec 3, IsMildSolutionOn ν u₀ u (Set.Ico 0 T) := 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, §1 eq. (1.3)–(1.5) and Theorem 1 (m = 3); H. Fujita, T. Kato, On the Navier–Stokes initial value problem I, Arch. Rational Mech. Anal. 16 (1964) 269–315, https://doi.org/10.1007/BF00276188, Theorem 4.1. Mission context: C. Fefferman, Existence and smoothness of the Navier–Stokes equation, Clay Mathematics Institute (2000), p. 2, https://www.claymath.org/wp-content/uploads/2022/06/navierstokes.pdf

View graph

Kato: local existence of a mild solution on [0,T)[0,T)[0,T) for smooth decaying data

Kato: local existence of a mild solution on $[0,T)$ for smooth decaying data