Leray Limit Compactness #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.lerayLimit_local_compactness
(ρ : 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ε)
(hregEquicontinuity :
∀ (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (ha : IsInJ a) (εseq : ℕ → ℝ),
(∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1) →
∀ (C : Set Foundation.Parabolic.Vec3),
IsCompact C →
C ⊆ Set.univ →
∀ (s₀ s₁ : ℝ),
Set.Icc s₀ s₁ ⊆ Set.Ioi 0 →
∀ (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3),
ContDiff ℝ (↑⊤) w →
HasCompactSupport w →
tsupport w ⊆ C →
∃ (A : ℝ) (B : ℝ) (θ : ℝ),
0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ) (s t : ℝ),
s ∈ Set.Icc s₀ s₁ →
t ∈ Set.Icc s₀ s₁ →
|(∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, uε a ha (εseq n) (x, t) i * (w x).ofLp i) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, uε a ha (εseq n) (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ)
(a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3)
(ha : IsInJ a)
(εseq : ℕ → ℝ)
(hseq : ∀ (n : ℕ), 0 < εseq n ∧ εseq n ≤ 1)
:
have Ubar := fun (n : ℕ) (z : Foundation.Parabolic.Vec3 × ℝ) =>
lerayLimitPiecewise (spaceTimeSet Set.univ (Set.Ioi 0))
(fun (q : Foundation.Parabolic.ParabolicPoint) =>
uε a ha (εseq n) (Foundation.Parabolic.parabolicHomeomorph.symm q))
(fun (q : Foundation.Parabolic.ParabolicPoint) => regUniformMollifiedInitial ρ (εseq n) ⋯ a q.1) z;
have Dbar := fun (n : ℕ) (z : Foundation.Parabolic.Vec3 × ℝ) (i j : Fin 3) =>
lerayLimitPiecewise (spaceTimeSet Set.univ (Set.Ioi 0))
(fun (q : Foundation.Parabolic.ParabolicPoint) (k l : Fin 3) =>
spatialPartial (fun (y : Foundation.Parabolic.ParabolicPoint) => uε a ha (εseq n) y k) l q)
(fun (x : Foundation.Parabolic.ParabolicPoint) (x_1 x_2 : Fin 3) => 0)
(Foundation.Parabolic.parabolicHomeomorph.symm z) i j;
∃ (σ : ℕ → ℕ),
StrictMono σ ∧ ∃ (v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3) (g :
Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber),
Measurable v ∧ Measurable g ∧ (∀ (z : Foundation.Parabolic.Vec3 × ℝ), v z = compactnessMollifiedLimit Ubar σ z) ∧ (∀ (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 (Ubar (σ 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 (Ubar (σ k) (x, ↑t))) ⋯)
w)
Filter.atTop
(nhds
(inner ℝ
(MeasureTheory.MemLp.toLp
(fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (v (x, ↑t))) hl)
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 (Ubar (σ k) z)) - 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.Vec3 × ℝ) => toCompactnessGradientFiber (Dbar (σ k) z)) 2
(MeasureTheory.volume.restrict Q))
(hl : 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.Vec3 × ℝ) =>
toCompactnessGradientFiber (Dbar (σ k) z))
⋯)
w)
Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp g hl) 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) (j : Fin 3) =>
((g (x, t)).ofLp i).ofLp j) ∧ (∀ (C : Set Foundation.Parabolic.Vec3),
IsCompact C →
C ⊆ Set.univ →
∀ (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 (Ubar 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 →
C ⊆ Set.univ →
∀ (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 (Ubar n) (Dbar 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
Local compactness and slice energy bounds for regularized solutions.