Uniform spatial tails in prop:leray-limit

The exterior estimate for the regularized solutions of thm:regularised (the hypothesis hregTails, in the form of lem:reg-tails) bounds the exterior slice energies ∫_{|x| > 2(m+1)} |u_ε(x,t)|² on every finite time interval by one sequence tending to zero. Weak lower semicontinuity on a compact exhaustion of the exterior transfers the bound to every local weak limit of the slices.

def CKN.Leray.lerayLimitFinalExteriorPiece (R : ℝ) (k : ℕ) : Set Foundation.Parabolic.Vec3

The compact pieces {R + 1/(k+1) ≤ |x|} ∩ closedBall(0,k) exhausting the Euclidean exterior {R < |x|}.

Equations

• CKN.Leray.lerayLimitFinalExteriorPiece R k = {x : CKN.Foundation.Parabolic.Vec3 | R + (↑k + 1)⁻¹ ≤ CKN.Foundation.Parabolic.vec3EuclideanNorm x} ∩ Metric.closedBall 0 ↑k

theorem CKN.Leray.lerayLimit_exterior_lintegral_le_of_local_weak (R : ℝ) (F : ℕ → Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (G : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (hGmeas : Measurable G) (B : ENNReal) (hB : B < ⊤) (hFbound : ∀ (n : ℕ), ∫⁻ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R < Foundation.Parabolic.vec3EuclideanNorm x}, ‖WithLp.toLp 2 (F n x)‖ₑ ^ 2 ≤ B) (hlocal : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ Set.univ → ∃ (hF : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (F n x)) 2 (MeasureTheory.volume.restrict C)) (hG : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (G x)) 2 (MeasureTheory.volume.restrict C)), ∀ (w : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict C))), Filter.Tendsto (fun (n : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (F n x)) ⋯) w) Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (G x)) hG) w))) : ∫⁻ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | R < Foundation.Parabolic.vec3EuclideanNorm x}, ‖WithLp.toLp 2 (G x)‖ₑ ^ 2 ≤ B

A bound on the exterior energy ∫_{|x|>R} |F_n|² uniform in n passes to a measurable field G that is the weak L² limit of F_n on every compact set.

theorem CKN.Leray.lerayLimit_regularised_spatialTails_with_limit (ρ : 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) (hSlice : ∀ (n : ℕ) (t : ℝ), 0 ≤ t → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => uε a ha (εseq n) (x, t)) 2 MeasureTheory.volume) (G : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hGu : ∀ (n : ℕ) (x : Foundation.Parabolic.Vec3) (t : ℝ), 0 < t → G n (x, t) = uε a ha (εseq n) (x, t)) (σ : ℕ → ℕ) (v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hv : Measurable v) (T : ℝ) (hlocal : ∀ (t : ↑(Set.Ioi 0)) (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ Set.univ → ∃ (hs : ∀ (k : ℕ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (G (σ k) (x, ↑t))) 2 (MeasureTheory.volume.restrict C)) (hl : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (v (x, ↑t))) 2 (MeasureTheory.volume.restrict C)), ∀ (w : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict C))), Filter.Tendsto (fun (k : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (G (σ k) (x, ↑t))) ⋯) w) Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (v (x, ↑t))) hl) w))) : ∃ (S : ℕ → ENNReal), Filter.Tendsto S Filter.atTop (nhds 0) ∧ (∀ (m n : ℕ), ∀ t ∈ Set.Ioo 0 T, ∫⁻ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | 2 * (↑m + 1) < Foundation.Parabolic.vec3EuclideanNorm x}, ‖WithLp.toLp 2 (uε a ha (εseq (σ n)) (x, t))‖ₑ ^ 2 ≤ S m) ∧ ∀ (m : ℕ), ∀ t ∈ Set.Ioo 0 T, ∫⁻ (x : Foundation.Parabolic.Vec3) in {x : Foundation.Parabolic.Vec3 | 2 * (↑m + 1) < Foundation.Parabolic.vec3EuclideanNorm x}, ‖WithLp.toLp 2 (v (x, t))‖ₑ ^ 2 ≤ S m

The uniform spatial tails in prop:leray-limit: under the exterior estimate hregTails of lem:reg-tails, for a sequence G agreeing with the regularized velocities at positive times and a subsequence σ along which v is the local weak limit of the positive-time slices of G, the exterior slice energies beyond the radius 2(m+1) of the regularized velocities and of v are bounded on (0,T) by one sequence S m → 0.