Leray Limit Tail Source

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lerayLimit_regularised_tail_tendsto (ρ : RegMollifierProfile) (uε : (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hregTails : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε), ε ≤ 1 → (∀ (R1 R2 t : ℝ), 0 < R1 → R1 < R2 → 0 ≤ t → ∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R2 < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (uε a ha ε (x, t)) ^ 2 ≤ (∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R1 < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (regUniformMollifiedInitial ρ ε hε a x) ^ 2) + C * ((MeasureTheory.eLpNorm a 2 MeasureTheory.volume).toReal ^ 2 * t ^ (1 / 2) + (MeasureTheory.eLpNorm a 2 MeasureTheory.volume).toReal ^ 3 * t ^ (1 / 4)) / (R2 - R1)) ∧ ∀ (R1 : ℝ), 0 < R1 → ∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R1 < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (regUniformMollifiedInitial ρ ε hε a x) ^ 2 ≤ ∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R1 - 1 < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (a x) ^ 2) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (εseq : ℕ → ℝ) (hseq : ∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1) (T : ℝ) : ∃ (b : ℕ → ℝ), Filter.Tendsto b Filter.atTop (nhds 0) ∧ ∀ (k n : ℕ), ∀ t ∈ Set.Icc 0 T, ∫ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | 2 * (↑n + 1) < Foundation.Parabolic.vec3EuclideanNorm x}, Foundation.Parabolic.vec3EuclideanNorm (uε a ha (εseq k) (x, t)) ^ 2 ≤ b n

The regularized exterior estimate and the initial L² tail give a uniformly vanishing spatial tail on every finite positive time interval, as in prop:leray-limit.