The compactness statement prop:leray-limit

For the regularized solutions of thm:regularised, every sequence ε_n → 0 in (0,1] has a subsequence along which the velocities converge to a limit u with weak gradient Du in all the senses used by the proof of thm:leray. The subsequence, the limit fields and their local convergence come from the compactness step CKN.Leray.lerayLimit_local_compactness, whose time-pairing modulus follows from the regularized contract; the whole-slab statements come from the uniform spatial tails of lem:reg-tails, which enter as the hypothesis hregTails. The limit velocity is the compactness limit at positive times and the datum at time zero; its value at every positive time is the iterated limit of spatial mollifications along the subsequence.

def CKN.Leray.lerayLimitFinalCylinder (T : ℝ) (m : ℕ) : Set (Foundation.Parabolic.Vec3 × ℝ)

The compact cylinders closedBall(0,m) × [T/(m+2), T - T/(m+2)] exhausting the slab ℝ³ × (0,T).

Equations

• CKN.Leray.lerayLimitFinalCylinder T m = Metric.closedBall 0 ↑m ×ˢ Set.Icc (T / (↑m + 2)) (T - T / (↑m + 2))

theorem CKN.Leray.lerayLimit_prop_of_regularised_tails (ρ : RegMollifierProfile) (uε : (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (pε : (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) → IsInJ a → ℝ → Foundation.Parabolic.ParabolicPoint → ℝ) (hregularised : ∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (ε : ℝ) (hε : 0 < ε), lerayAssemblyRegularisedConditions ρ uε pε a ha ε hε) (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) : lerayAssemblyCompactnessLimitContract ρ uε

prop:leray-limit for the regularized solutions uε with pressures pε of thm:regularised (the contract hregularised), given the exterior estimate hregTails of lem:reg-tails. The conclusion is the compactness statement used by CKN.lerayExistence_of_limits.