Compactness Strong Representative #
Supporting estimates for the Navier–Stokes development.
theorem
CKN.Leray.strong_l2_to_compactnessMollifiedLimit_on_exhaustion
{U : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
(hU : IsOpen U)
(hI : IsOpen I)
(u : ℕ → Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3)
(Du : ℕ → Foundation.Parabolic.Vec3 × ℝ → Fin 3 → Foundation.Parabolic.Vec3)
(huMeas : ∀ (n : ℕ), Measurable (u n))
(hDuMeas : ∀ (n : ℕ), Measurable (Du n))
(hweakGrad :
∀ (n : ℕ),
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), HasWeakGradientOn U (fun (x : Vec 3) => u n (x, t) i) fun (x : Vec 3) => Du n (x, t) i)
(hbound :
∀ (C : Set Foundation.Parabolic.Vec3),
IsCompact C →
C ⊆ U →
∀ (T : Set ℝ),
IsCompact T →
T ⊆ I →
∃ M < ⊤,
∀ (n : ℕ),
∀ t ∈ T,
∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u n (x, t))) ^ 2 ≤ M)
(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)
(K : ℕ → Set Foundation.Parabolic.Vec3)
(χ : ℕ → 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)
(hχ :
∀ (j : ℕ),
ContDiff ℝ (↑⊤) (χ j) ∧ HasCompactSupport (χ j) ∧ tsupport (χ j) ⊆ U ∧ (∀ (x : Foundation.Parabolic.Vec3), χ j x ∈ Set.Icc 0 1) ∧ ∀ x ∈ K j, χ j x = 1)
(hJ : ∀ (j : ℕ), IsCompact (J j) ∧ J j ⊆ I)
(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)))
(hVcont :
∀ (j : ℕ) (x : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)),
Continuous fun (t : ↑I) => inner ℝ (V j t) x)
(huniform :
∀ (j : ℕ) (p : RationalCompactTimeWindow I)
(x : ↥(MeasureTheory.Lp (WithLp 2 Foundation.Parabolic.Vec3) 2 MeasureTheory.volume)) (ε : ℝ),
0 < ε →
∀ᶠ (k : ℕ) in Filter.atTop, ∀ (t : RationalTimeSlice p),
dist
(inner ℝ
(MeasureTheory.MemLp.toLp
(fun (y : Foundation.Parabolic.Vec3) => χ j y • WithLp.toLp 2 (u (σ k) (y, ↑t))) ⋯)
x)
(inner ℝ (V j ⟨↑t, ⋯⟩) x) < ε)
(j : ℕ)
:
∃ (_ :
∀ (k : ℕ),
MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (u (σ k) z)) 2
((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j)))),
Filter.Tendsto
(fun (k : ℕ) =>
MeasureTheory.eLpNorm
((fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (u (σ k) z)) - fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (compactnessMollifiedLimit u σ z))
2 ((MeasureTheory.volume.restrict (K j)).prod (MeasureTheory.volume.restrict (J j))))
Filter.atTop (nhds 0)
The strong local L² limit selected by compactness agrees with the
mollified representative on every rectangle of the exhaustion.