Small energy-enstrophy product implies small critical $L^3$ norm

Open

NavierStokes.small_eLpNorm_three_of_energy_enstrophy_small

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

analysisfunctional-analysisnavier-stokessobolev-inequality

There is an absolute constant $C>0$ such that every admissible velocity field $u_0$ on $\mathbb R^3$ and every $r>0$ satisfy

\left(\int_{\mathbb R^3}|u_0|^2\right)\left(\int_{\mathbb R^3}|\nabla u_0|^2\right)\le C r^4 \quad\Longrightarrow\quad \|u_0\|_{L^3}\le r.

This scale-critical interpolation statement converts Leray’s energy-enstrophy smallness condition into the critical $L^3$ hypothesis used by Kato’s global theorem.

Formalization Note The $L^3$ norm is Mathlib’s extended norm eLpNorm; admissible data ensure all displayed quantities are finite.

Preamble

import Definitions.Def_NavierStokes_Mild
import Mathlib

open MeasureTheory

Formal statement

namespace NavierStokes
theorem small_eLpNorm_three_of_energy_enstrophy_small :
    ∃ C : ℝ, 0 < C ∧ ∀ (r : ℝ), 0 < r → ∀ (u₀ : Vec 3 → Vec 3), IsInitialData u₀ →
      (∫ x, ‖u₀ x‖ ^ 2) * (∫ x, gradNormSq u₀ x) ≤ C * r ^ 4 →
      eLpNorm u₀ 3 volume ≤ ENNReal.ofReal r := by sorry
end NavierStokes

Source

Hölder interpolation together with the Sobolev inequality on R^3; used in the formal target NavierStokes.small_data_global_existence_R3. See 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, p. 472 and Theorem 2; J. Leray, Acta Math. 63 (1934), §§21–22, https://doi.org/10.1007/BF02547354.

View graph

Small energy-enstrophy product implies small critical L3L^3L3 norm

Small energy-enstrophy product implies small critical $L^3$ norm