Compactness Limit Bounds #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.compactness_limit_slice_bound
{U : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
(hI : IsOpen I)
(u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3)
(σ : ℕ → ℕ)
(huMeas : ∀ (n : ℕ), Measurable (u n))
(K : ℕ → Set Foundation.Parabolic.Vec3)
(χ : ℕ → Foundation.Parabolic.Vec3 → ℝ)
(hK : ∀ (j : ℕ), IsCompact (K j) ∧ K j ⊆ U ∧ K j ⊆ K (j + 1) ∧ K j ⊆ interior (K (j + 1)))
(hKcover : ⋃ (j : ℕ), K j = U)
(hχ : ∀ (j : ℕ), ∀ x ∈ K j, χ j x = 1)
(hbound :
∀ (C : Set Foundation.Parabolic.Vec3),
IsCompact C →
C ⊆ U →
∀ (J : Set ℝ),
IsCompact J →
J ⊆ I →
∃ M < ⊤,
∀ (n : ℕ),
∀ t ∈ J,
∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u n (x, t))) ^ 2 ≤ M)
(hmem :
∀ (n j : ℕ) (t : ↑I),
MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ j x • WithLp.toLp 2 (u n (x, ↑t))) 2
MeasureTheory.volume)
(V : ℕ → ↑I → ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume))
(hweak :
∀ (j : ℕ) (t : ↑I) (x : ↥(MeasureTheory.Lp (WithLp 2 Foundation.Parabolic.Vec3) 2 MeasureTheory.volume)),
Filter.Tendsto
(fun (k : ℕ) =>
inner ℝ
(MeasureTheory.MemLp.toLp (fun (y : Foundation.Parabolic.Vec3) => χ j y • WithLp.toLp 2 (u (σ k) (y, ↑t))) ⋯)
x)
Filter.atTop (nhds (inner ℝ (V j t) x)))
(C : Set Foundation.Parabolic.Vec3)
(hC : IsCompact C)
(hCU : C ⊆ U)
(T : Set ℝ)
(hTI : T ⊆ I)
(M : ENNReal)
(hM : M < ⊤)
(hMb :
∀ (n : ℕ),
∀ t ∈ T,
∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u n (x, t))) ^ 2 ≤ M)
(t : ℝ)
:
t ∈ T →
∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (compactnessMollifiedLimit u σ (x, t))) ^ 2 ≤ M
The all-time local slice energy bound passes to the selected limit.
theorem
CKN.Leray.compactness_limit_gradient_bound
{U : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
(u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3)
(Du : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3)
(hDuMeas : ∀ (n : ℕ), Measurable (Du n))
(σ : ℕ → ℕ)
(K : ℕ → Set Foundation.Parabolic.Vec3)
(J : ℕ → Set ℝ)
(hK : ∀ (j : ℕ), IsCompact (K j) ∧ K j ⊆ U ∧ K j ⊆ K (j + 1) ∧ K j ⊆ interior (K (j + 1)))
(hKcover : ⋃ (j : ℕ), K j = U)
(hJ : ∀ (j : ℕ), IsCompact (J j) ∧ J j ⊆ I ∧ J j ⊆ J (j + 1) ∧ J j ⊆ interior (J (j + 1)))
(hJcover : ⋃ (j : ℕ), J j = I)
(D :
(j : ℕ) →
↥(MeasureTheory.Lp CompactnessGradientFiber 2
((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j)))))
(hDweak :
∀ (j : ℕ),
∃ (hgrad :
∀ (k : ℕ),
MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du (σ k) z)) 2
((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j)))),
∀
(w :
↥(MeasureTheory.Lp CompactnessGradientFiber 2
((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))),
Filter.Tendsto
(fun (k : ℕ) =>
inner ℝ
(MeasureTheory.MemLp.toLp
(fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du (σ k) z)) ⋯)
w)
Filter.atTop (nhds (inner ℝ (D j) w)))
(g : Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber)
(hg : Measurable g)
(hgEq :
∀ (j : ℕ),
g =ᵐ[(MeasureTheory.volume.restrict (interior (K j))).prod (MeasureTheory.volume.restrict (J j))]
compactnessGradientLocalRepresentative K J D j)
(C : Set Foundation.Parabolic.Vec3)
(hC : IsCompact C)
(hCU : C ⊆ U)
(T : Set ℝ)
(hT : IsCompact T)
(hTI : T ⊆ I)
(G : ENNReal)
(hG : G < ⊤)
(hGb :
∀ (n : ℕ),
∫⁻ (t : ℝ) in T, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (spatialGradientSq (u n) (Du n) (x, t)) ≤ G)
:
∫⁻ (t : ℝ) in T, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal
(spatialGradientSq (fun (x : Foundation.Parabolic.ParabolicPoint) => 0)
(fun (z : Foundation.Parabolic.ParabolicPoint) (i m : Fin 3) => ((g z).ofLp i).ofLp m) (x, t)) ≤ G
The local matrix energy bound passes to the measurable weak limit.