The strong convergence clauses of prop:forced-limit

On every finite slab ℝ³ × (0,T), the forced regularized velocities along the subsequence of the compactness step converge strongly to the limit in L², in every L^q with 2 ≤ q < 10/3, and in L³, and their spatial mollifications converge in L³ to the same limit. The local strong convergence on compact subsets of ℝ³ × (0,∞) comes from the compactness step; the uniform spatial tails (lem:forced-tails, in the form of a hypothesis supplied by the tail estimate) and the uniform slice energy of lem:forced-energy-bounds control the complement of large compact cylinders; the uniform L^{10/3} bound eq:forced-ten-thirds gives the intermediate exponents.

def CKN.Leray.forcedLerayLimitStrongCylinder (T R δ : ℝ) : Set Foundation.Parabolic.ParabolicPoint

The compact cylinder closedBall(0, R) × [δ, T - δ] of the slab.

Equations

• CKN.Leray.forcedLerayLimitStrongCylinder T R δ = CKN.spaceTimeSet (Metric.closedBall 0 R) (Set.Icc δ (T - δ))

theorem CKN.Leray.forcedLerayLimit_strong_clauses (ρ : RegMollifierProfile) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f) (εseq : ℕ → ℝ) (hseq : ∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1) (σ : ℕ → ℕ) (hεsub : Filter.Tendsto (fun (n : ℕ) => εseq (σ n)) Filter.atTop (nhds 0)) (v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (hv : Measurable v) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (huv : ∀ (x : Foundation.Parabolic.Vec3) (t : ℝ), 0 < t → u (x, t) = v (x, t)) (hstrong : ∀ (Q : Set (Foundation.Parabolic.Vec3 × ℝ)), IsCompact Q → Q ⊆ Set.univ ×ˢ Set.Ioi 0 → Filter.Tendsto (fun (k : ℕ) => MeasureTheory.eLpNorm ((fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (forcedRegVelocity ρ a ha f hf (εseq (σ k)) (z.1, z.2))) - fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (v z)) 2 (MeasureTheory.volume.restrict Q)) Filter.atTop (nhds 0)) (hSliceBound : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → ∀ (b₁ b₂ : ℝ), Set.Icc b₁ b₂ ⊆ Set.Ioi 0 → ∀ M < ⊤, (∀ (n : ℕ), ∀ t ∈ Set.Icc b₁ b₂, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (forcedRegVelocity ρ a ha f hf (εseq n) (x, t))) ^ 2 ≤ M) → ∀ t ∈ Set.Icc b₁ b₂, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (v (x, t))) ^ 2 ≤ M) (T : ℝ) (hT : 0 < T) (htails : ∃ (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 (forcedRegVelocity ρ a ha f hf (ε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) : have μ := MeasureTheory.volume.restrict (spaceTimeSet Set.univ (Set.Ioo 0 T)); have U := fun (n : ℕ) => forcedRegVelocity ρ a ha f hf (εseq (σ n)); have J := fun (n : ℕ) => regUniformMollifiedVelocity ρ (εseq (σ n)) ⋯ (U n); MeasureTheory.AEStronglyMeasurable u μ ∧ MeasureTheory.MemLp u 2 μ ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) 2 μ) Filter.atTop (nhds 0) ∧ (∀ (q : ℝ), 2 ≤ q → q < 10 / 3 → Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) (ENNReal.ofReal q) μ) Filter.atTop (nhds 0)) ∧ (∀ (n : ℕ), MeasureTheory.MemLp (U n) 3 μ) ∧ (∀ (n : ℕ), MeasureTheory.MemLp (J n) 3 μ) ∧ MeasureTheory.MemLp u 3 μ ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (J n - u) 3 μ) Filter.atTop (nhds 0)

The strong convergence clauses of prop:forced-limit on one slab ℝ³ × (0,T). The hypotheses are the local strong convergence and the limit slice bound of CKN.Leray.forcedLerayLimit_local_compactness (its second and fifth outputs, verbatim), the positive-time identification of u with the compactness limit v, and the uniform spatial tails htails of the forced regularized velocities and of v on (0,T). The conclusion is the strong convergence part of the forced compactness statement: u ∈ L² ∩ L³ on the slab, U_n → u in L² and in every L^q with 2 ≤ q < 10/3, U_n ∈ L³, and the spatial mollifications J_n U_n lie in L³ and converge to u in L³.