Compactness Main

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.lem_compactness {U : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hU : IsOpen U) (hI : IsOpen I) (hIconn : I.OrdConnected) (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 → ∀ (a b : ℝ), Set.Icc a b ⊆ I → ∃ M < ⊤, ∀ (n : ℕ), ∀ t ∈ Set.Icc a b, ∫⁻ (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 → ∀ (a b : ℝ), Set.Icc a b ⊆ I → ∃ G < ⊤, ∀ (n : ℕ), ∫⁻ (t : ℝ) in Set.Icc a b, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (spatialGradientSq (u n) (Du n) (x, t)) ≤ G) (hmod : ∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ U → ∀ (a b : ℝ), Set.Icc a b ⊆ I → ∀ (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 a b → t ∈ Set.Icc a b → |(∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u n (x, t) i * (w x).ofLp i) - ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, u n (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ) : ∃ (σ : ℕ → ℕ), StrictMono σ ∧ ∃ (v : Foundation.Parabolic.Vec3 × ℝ → Foundation.Parabolic.Vec3), Measurable v ∧ ∃ (g : Foundation.Parabolic.Vec3 × ℝ → CompactnessGradientFiber), Measurable g ∧ (∀ (t : ↑I) (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ U → ∃ (hs : ∀ (k : ℕ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u (σ 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 (u (σ 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 ⊆ U ×ˢ I → 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 (v z)) 2 (MeasureTheory.volume.restrict Q)) Filter.atTop (nhds 0)) ∧ (∀ (Q : Set (Foundation.Parabolic.Vec3 × ℝ)), IsCompact Q → Q ⊆ U ×ˢ I → ∃ (hs : ∀ (k : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => toCompactnessGradientFiber (Du (σ 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 (Du (σ k) z)) ⋯) w) Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp g hl) w))) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), HasWeakGradientOn U (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 → C ⊆ U → ∀ (w : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict C))), Continuous fun (t : ↑I) => ∫ (x : Foundation.Parabolic.Vec3) in C, ∑ i : Fin 3, v (x, ↑t) i * (↑↑w x).ofLp i) ∧ (∀ (C : Set Foundation.Parabolic.Vec3), IsCompact C → C ⊆ U → ∀ (a b : ℝ), Set.Icc a b ⊆ I → ∀ M < ⊤, (∀ (n : ℕ), ∀ t ∈ Set.Icc a b, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u n (x, t))) ^ 2 ≤ M) → ∀ t ∈ Set.Icc a 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 ⊆ U → ∀ (a b : ℝ), Set.Icc a b ⊆ I → ∀ G < ⊤, (∀ (n : ℕ), ∫⁻ (t : ℝ) in Set.Icc a b, ∫⁻ (x : Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (spatialGradientSq (u n) (Du n) (x, t)) ≤ G) → ∫⁻ (t : ℝ) in Set.Icc a b, ∫⁻ (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

Local energy, gradient, and time-pairing bounds yield a subsequence with every-time weak slices, local strong L² convergence, and a jointly measurable weak spatial gradient. This is lem:compactness.