Compactness data for the local strong solution

This file starts the compactness step of prop:lps-local-strong from the exact uniform spatial H¹ and H² bounds. The Leray limit supplies its canonical trace, weak gradient convergence, and strong velocity convergence (prop:leray-limit of the CKN manuscript).

theorem ESS.LPS.lps_vec3EuclideanNorm_sq_eq_sum_sq (v : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.vec3EuclideanNorm v ^ 2 = ∑ i : Fin 3, v i ^ 2

The squared Euclidean norm of a vector is the sum of its squared coordinates.

theorem ESS.LPS.lps_regR12_second_memLp_open_slab (ρ : CKN.Leray.RegMollifierProfile) (ε : ℝ) (hε : 0 < ε) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hb : CKN.IsInJ b) (T : ℝ) (hT : 0 < T) (i j k : Fin 3) : MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12Velocity ρ ε hε b hb x i) j y) k z) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

The ordered second spatial derivatives of one regularized velocity are in space-time L² on the full open slab, including times arbitrarily close to zero. The Bessel path controls the Fourier multiplier at the initial endpoint; the pointwise derivative is identified with that path on positive times.

theorem ESS.LPS.lps_hessian_component_norm_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f S : α → ℝ} {M : ℝ} (hM : 0 ≤ M) (hmem : MeasureTheory.MemLp f 2 μ) (hfsq : MeasureTheory.Integrable (fun (z : α) => f z ^ 2) μ) (hSint : MeasureTheory.Integrable S μ) (hle : ∀ (z : α), f z ^ 2 ≤ S z) (henergy : ∫ (z : α), S z ∂μ ≤ M) : ‖MeasureTheory.MemLp.toLp f hmem‖ ≤ √M

A square-integrable scalar component controlled pointwise by an integrable nonnegative energy density inherits its global L² bound.

theorem ESS.LPS.lps_scalar_lp_inner_left_eq_integral {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F : ↥(MeasureTheory.Lp ℝ 2 μ)} {g : α → ℝ} (hg : MeasureTheory.MemLp g 2 μ) : inner ℝ F (MeasureTheory.MemLp.toLp g hg) = ∫ (z : α), ↑↑F z * g z ∂μ

The inner product of an L² class with a class represented by a function.

theorem ESS.LPS.lps_h1_scalar_weak_limit (fseq : ℕ → CKN.Foundation.Parabolic.Vec3 → ℝ) (gseq : ℕ → CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (f : CKN.Foundation.Parabolic.Vec3 → ℝ) (C : ℝ) (hC : 0 ≤ C) (hgseq : ∀ (n : ℕ) (j : Fin 3), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => gseq n x j) 2 MeasureTheory.volume) (hbound : ∀ (n : ℕ) (j : Fin 3), ‖MeasureTheory.MemLp.toLp (fun (x : CKN.Foundation.Parabolic.Vec3) => gseq n x j) ⋯‖ ≤ C) (hweakf : ∀ (w : CKN.Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp w 2 MeasureTheory.volume → Filter.Tendsto (fun (n : ℕ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), fseq n x * w x) Filter.atTop (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), f x * w x))) (hweakD : ∀ (n : ℕ), CKN.HasWeakGradientOn Set.univ (fseq n) (gseq n)) : ∃ (G : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (hG : MeasureTheory.MemLp G 2 MeasureTheory.volume), CKN.HasWeakGradientOn Set.univ f G ∧ ∀ (j : Fin 3), ‖MeasureTheory.MemLp.toLp (fun (x : CKN.Foundation.Parabolic.Vec3) => G x j) ⋯‖ ≤ C

A weakly convergent L² scalar sequence with uniformly bounded weak gradients has a weak gradient limit with the same coordinate bounds.

theorem ESS.LPS.lps_strong_limit_compactness_base (ρ : CKN.Leray.RegMollifierProfile) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hb : (∀ (i : Fin 3), ∃ (h : CKN.H1Function Set.univ), (h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) => Db x i) ∧ CKN.IsInJ b) (T M : ℝ) (hT : 0 < T) (hUniformBounds : ∀ (ε : ℝ) (hε : 0 < ε), have Uε := CKN.Leray.regR12Velocity ρ ε hε b ⋯; have Dε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Uε y i) j z; have D2ε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => Uε x i) j y) k z; (∀ t ∈ Set.Icc 0 T, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (Uε (x, t)) ^ 2 + CKN.spatialGradientSq Uε Dε (x, t) ≤ M) ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3, ∑ j : Fin 3, CKN.Foundation.Parabolic.vec3EuclideanNorm (D2ε z i j) ^ 2 ≤ M) : ∃ (σ : ℕ → ℕ), StrictMono σ ∧ ∃ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3), (∀ (x : CKN.Foundation.Parabolic.Vec3), u (x, 0) = b x) ∧ CKN.IsLerayHopfSolution T b u Du ∧ MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (CKN.Leray.regR12Uε ρ b ⋯ ((fun (m : ℕ) => 1 / (↑m + 1)) (σ n)) - u) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0) ∧ (∀ (i j : Fin 3) (w : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) → Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12Uε ρ b ⋯ ((fun (m : ℕ) => 1 / (↑m + 1)) (σ n)) y i) j z * w z) Filter.atTop (nhds (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), Du z i j * w z))) ∧ (∀ (n : ℕ), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3, ∑ j : Fin 3, (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (k : Fin 3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12Velocity ρ ((fun (m : ℕ) => 1 / (↑m + 1)) (σ n)) ⋯ b ⋯ x i) j y) k z) ^ 2 ≤ M) ∧ (∀ (t : ℝ), 0 < t → ∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), MeasureTheory.MemLp w 2 MeasureTheory.volume → Filter.Tendsto (fun (n : ℕ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.Leray.regR12Uε ρ b ⋯ ((fun (m : ℕ) => 1 / (↑m + 1)) (σ n)) (x, t) i * w x i) Filter.atTop (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i))) ∧ ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), 0 < z.2 → u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) = CKN.Leray.compactnessMollifiedLimit (fun (n : ℕ) (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Leray.regR12Uε ρ b ⋯ ((fun (m : ℕ) => 1 / (↑m + 1)) (σ n)) (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y)) σ z

The canonical Leray limit, together with the inherited uniform second derivative bound, for the sequence εₙ = 1 / (n + 1).

theorem ESS.LPS.lps_strong_limit_hessian_weak_compactness (ρ : CKN.Leray.RegMollifierProfile) (b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (Db : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hb : (∀ (i : Fin 3), ∃ (h : CKN.H1Function Set.univ), (h.toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => b x i) ∧ h.grad = fun (x : CKN.Foundation.Parabolic.Vec3) => Db x i) ∧ CKN.IsInJ b) (T M : ℝ) (hT : 0 < T) (hM : 0 ≤ M) (hUniformBounds : ∀ (ε : ℝ) (hε : 0 < ε), have Uε := CKN.Leray.regR12Velocity ρ ε hε b ⋯; have Dε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => Uε y i) j z; have D2ε := fun (z : CKN.Foundation.Parabolic.ParabolicPoint) (i j k : Fin 3) => CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => Uε x i) j y) k z; (∀ t ∈ Set.Icc 0 T, ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.Foundation.Parabolic.vec3EuclideanNorm (Uε (x, t)) ^ 2 + CKN.spatialGradientSq Uε Dε (x, t) ≤ M) ∧ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ∑ i : Fin 3, ∑ j : Fin 3, CKN.Foundation.Parabolic.vec3EuclideanNorm (D2ε z i j) ^ 2 ≤ M) : ∃ (σ : ℕ → ℕ), StrictMono σ ∧ ∃ (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3), (∀ (x : CKN.Foundation.Parabolic.Vec3), u (x, 0) = b x) ∧ CKN.IsLerayHopfSolution T b u Du ∧ MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (CKN.Leray.regR12Uε ρ b ⋯ ((fun (m : ℕ) => 1 / (↑m + 1)) (σ n)) - u) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) Filter.atTop (nhds 0) ∧ (∀ (i j : Fin 3) (w : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) → Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12Uε ρ b ⋯ ((fun (m : ℕ) => 1 / (↑m + 1)) (σ n)) y i) j z * w z) Filter.atTop (nhds (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), Du z i j * w z))) ∧ ∃ (D2u : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3), MeasureTheory.MemLp D2u 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) ∧ (∀ (i j k : Fin 3) (w : CKN.Foundation.Parabolic.ParabolicPoint → ℝ), MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))) → Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialPartial (fun (x : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Leray.regR12Velocity ρ (1 / (↑(σ n) + 1)) ⋯ b ⋯ x i) j y) k z * w z) Filter.atTop (nhds (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), D2u z i j k * w z))) ∧ ∃ (σ₀ : ℕ → ℕ), StrictMono σ₀ ∧ (∀ (t : ℝ), 0 < t → ∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3), MeasureTheory.MemLp w 2 MeasureTheory.volume → Filter.Tendsto (fun (n : ℕ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, CKN.Leray.regR12Uε ρ b ⋯ (1 / (↑(σ₀ n) + 1)) (x, t) i * w x i) Filter.atTop (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, u (x, t) i * w x i))) ∧ ∀ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), 0 < z.2 → u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm z) = CKN.Leray.compactnessMollifiedLimit (fun (n : ℕ) (y : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Leray.regR12Uε ρ b ⋯ (1 / (↑(σ₀ n) + 1)) (CKN.Foundation.Parabolic.parabolicHomeomorph.symm y)) σ₀ z

On a finite slab, the regularized ordered Hessians have one global space-time weak L² limit along a further subsequence of the Leray limit.