Smoothness of the Leray pressure associated with a mild solution

Open

NavierStokes.pressureOf_smooth_on_of_isMildSolutionOn

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

analysisfluid-dynamicsnavier-stokespartial-differential-equations

Let $\nu>0$ , let $u$ be a smooth mild Navier–Stokes solution on a time set $S$ equal either to $[0,\infty)$ or to $[0,T)$ , and define its Leray pressure by

p(t)=(-\Delta)^{-1}\operatorname{div}((u(t)\cdot\nabla)u(t)).

Then $(t,x)\mapsto p(t,x)$ is $C^\infty$ on $S\times\mathbb R^3$ , with smoothness understood relative to the half-line or half-open interval at its boundary.

This isolates the pressure-regularity obligation in the passage from a Kato–Fujita mild solution to a classical solution.

Preamble

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

Formal statement

namespace NavierStokes
theorem pressureOf_smooth_on_of_isMildSolutionOn (ν : ℝ) (hν : 0 < ν)
    (u₀ : Vec 3 → Vec 3) (u : ℝ → Vec 3 → Vec 3) (S : Set ℝ)
    (hS : S = Set.Ici 0 ∨ ∃ T : ℝ, S = Set.Ico 0 T)
    (hu : IsMildSolutionOn ν u₀ u S) :
    ContDiffOn ℝ ∞ (Function.uncurry (pressureOf u)) (S ×ˢ Set.univ) := by sorry
end NavierStokes

Source

T. Kato, Strong L^p-solutions of the Navier–Stokes equation in R^m, Math. Z. 187 (1984), 471–480, https://doi.org/10.1007/BF01174182, §1 and Theorem 1 prime (regularity of mild solutions); J. Leray, Acta Math. 63 (1934), §§14–16 (pressure as Newton potential). Exact formal context: Prove2Me definition NavierStokes_Mild, theorem id 22ac75d3-ebba-403c-ad68-a493ac2dd884.

View graph