Compactness Gradient Extract #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.exists_common_subsequence_gradient_weak_on_exhaustion
{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)
(hJ : ∀ (j : ℕ), IsCompact (J j) ∧ J j ⊆ I)
(hgradBound :
∀ (C : Set Foundation.Parabolic.Vec3),
IsCompact C →
C ⊆ U →
∀ (T : Set ℝ),
IsCompact T →
T ⊆ I →
∃ G < ⊤,
∀ (n : ℕ),
∫⁻ (t : ℝ) in T, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (spatialGradientSq (u n) (Du n) (x, t)) ≤ G)
:
∃ (τ : ℕ → ℕ),
StrictMono τ ∧ ∃ (D :
(j : ℕ) →
↥(MeasureTheory.Lp CompactnessGradientFiber 2
((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))),
∀ (j : ℕ),
∃ (hmem :
∀ (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))
One subsequence converges weakly for the matrix gradients on every compact rectangle of a countable exhaustion.