Forced Leray Limit Prop Compactness #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.forcedLerayLimit_local_compactness
(ρ : 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)
:
∃ (σ : ℕ → ℕ),
StrictMono σ ∧ ∃ (v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (g :
Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber),
Measurable v ∧ Measurable g ∧ (∀ (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))
(hv :
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))) hv)
w))) ∧ (∀ (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)) ∧ (∀ (Q : Set (Foundation.Parabolic.Vec3 × ℝ)),
IsCompact Q →
Q ⊆ Set.univ ×ˢ Set.Ioi 0 →
∃ (hs :
∀ (k : ℕ),
MeasureTheory.MemLp
(fun (z : Foundation.Parabolic.ParabolicPoint) =>
toCompactnessGradientFiber (forcedRegGradient ρ a ha f hf (εseq (σ k)) z))
2 (MeasureTheory.volume.restrict Q))
(hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict Q)),
∀ (w : ↥(MeasureTheory.Lp CompactnessGradientFiber 2 (MeasureTheory.volume.restrict Q))),
Filter.Tendsto
(fun (k : ℕ) =>
inner ℝ
(MeasureTheory.MemLp.toLp
(fun (z : Foundation.Parabolic.ParabolicPoint) =>
toCompactnessGradientFiber (forcedRegGradient ρ a ha f hf (εseq (σ k)) z))
⋯)
w)
Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp g hg) w))) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioi 0), ∀ (i : Fin 3),
HasWeakGradientOn Set.univ (fun (x : Vec 3) => v (x, t) i) fun (x : Vec 3) (m : Fin 3) =>
((g (x, t)).ofLp i).ofLp m) ∧ (∀ (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) ∧ (∀ (C : Set Foundation.Parabolic.Vec3),
IsCompact C →
∀ (b₁ b₂ : ℝ),
Set.Icc b₁ b₂ ⊆ Set.Ioi 0 →
∀ G < ⊤,
(∀ (n : ℕ),
∫⁻ (t : ℝ) in Set.Icc b₁ b₂, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal
(spatialGradientSq (forcedRegVelocity ρ a ha f hf (εseq n))
(forcedRegGradient ρ a ha f hf (εseq n)) (x, t)) ≤ G) →
∫⁻ (t : ℝ) in Set.Icc b₁ b₂, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal
(spatialGradientSq (fun (x : Foundation.Parabolic.ParabolicPoint) => 0)
(fun (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) =>
((g z).ofLp i).ofLp j)
(x, t)) ≤ G) ∧ ∀ (z : Foundation.Parabolic.Vec3 × ℝ),
v z = compactnessMollifiedLimit (fun (n : ℕ) => forcedRegVelocity ρ a ha f hf (εseq n)) σ z
The forced regularized fields have a common local compactness limit on
positive time intervals, as required in prop:forced-limit.