The compactness statement prop:forced-limit #
For the forced regularized solutions of lem:regularised-forced, 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-forced. The subsequence, the limit fields and their local
convergence come from the compactness step
CKN.Leray.forcedLerayLimit_local_compactness; the whole-slab statements come
from the uniform spatial tails of lem:forced-tails, which enter as the
hypothesis htails. 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.
theorem
CKN.Leray.compactnessMollifiedLimit_comp_eq_of_tendsto
(F : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3)
(σ : ℕ → ℕ)
(hσ : Filter.Tendsto σ Filter.atTop Filter.atTop)
(z : Foundation.Parabolic.Vec3 × ℝ)
(hconv :
∀ (i : Fin 3) (m : ℕ),
∃ (L : ℝ),
Filter.Tendsto
(fun (k : ℕ) => mollify (fun (y : Foundation.Parabolic.Vec3) => F (σ k) (y, z.2) i) (sliceRadius m) ⋯ z.1)
Filter.atTop (nhds L))
:
The iterated mollified limit along σ of a subsequence F ∘ σ agrees
with the one of F at a point where the mollifications of F ∘ σ converge at
every scale.
theorem
CKN.Leray.forcedLerayLimit_of_spatialTails
(ρ : RegMollifierProfile)
(htails :
∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a)
(f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (hf : IsLocallySquareIntegrableForce f)
(εseq : ℕ → ℝ),
(∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1) →
∀ (σ : ℕ → ℕ) (v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3),
Measurable v →
∀ (T : ℝ),
0 < T →
(∀ (t : ℝ),
0 < t →
∀ (C : Set Foundation.Parabolic.Vec3),
IsCompact C →
∃ (hs :
∀ (k : ℕ),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
WithLp.toLp 2 (forcedRegVelocity ρ a ha f hf (εseq (σ k)) (x, t)))
2 (MeasureTheory.volume.restrict C))
(hvC :
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 (forcedRegVelocity ρ a ha f hf (εseq (σ k)) (x, t)))
⋯)
w)
Filter.atTop
(nhds
(inner ℝ
(MeasureTheory.MemLp.toLp
(fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (v (x, t))) hvC)
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 (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)
(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εseq : Filter.Tendsto εseq Filter.atTop (nhds 0))
:
∃ (σ : ℕ → ℕ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du :
Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3),
StrictMono σ ∧ Filter.Tendsto σ Filter.atTop Filter.atTop ∧ Filter.Tendsto (fun (n : ℕ) => εseq (σ n)) Filter.atTop (nhds 0) ∧ (∀ (x : Foundation.Parabolic.Vec3), u (x, 0) = a x) ∧ (∀ (T : ℝ),
0 < T →
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);
have Dseq := fun (n : ℕ) => forcedRegGradient ρ a ha f hf (εseq (σ n));
MeasureTheory.AEStronglyMeasurable u μ ∧ MeasureTheory.AEStronglyMeasurable Du μ ∧ MeasureTheory.MemLp u 2 μ ∧ MeasureTheory.MemLp Du 2 μ ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (U n - u) 2 μ) Filter.atTop (nhds 0) ∧ (∀ (i j : Fin 3) (w : Foundation.Parabolic.ParabolicPoint → ℝ),
MeasureTheory.MemLp w 2 μ →
Filter.Tendsto
(fun (n : ℕ) =>
∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), Dseq n z i j * w z)
Filter.atTop
(nhds
(∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Set.univ (Set.Ioo 0 T), Du z i j * w z))) ∧ (∀ (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) ∧ (∀ (t : ℝ),
0 < t →
∀ (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3),
MeasureTheory.MemLp w 2 MeasureTheory.volume →
Filter.Tendsto
(fun (n : ℕ) =>
∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, U n (x, t) i * w x i)
Filter.atTop
(nhds
(∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i))) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), ∀ (i : Fin 3),
HasWeakGradientOn Set.univ (fun (x : Vec 3) => u (x, t) i)
fun (x : Vec 3) => Du (x, t) i) ∧ ∀ (z : Foundation.Parabolic.Vec3 × ℝ),
0 < z.2 →
u (Foundation.Parabolic.parabolicHomeomorph.symm z) = compactnessMollifiedLimit
(fun (n : ℕ) (y : Foundation.Parabolic.Vec3 × ℝ) =>
forcedRegVelocity ρ a ha f hf (εseq (σ n)) (Foundation.Parabolic.parabolicHomeomorph.symm y))
σ z
prop:forced-limit for the forced regularized solutions with the
mollifier profile ρ, given the uniform spatial tails of lem:forced-tails
along the subsequence of the compactness step (htails).