Compactness Local Strong

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.memLp_two_finite_rank_of_bounded_coefficients {ι : Type u_1} [Fintype ι] {K : Set Foundation.Parabolic.Vec3} {J : Set ℝ} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict K)] [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict J)] (hK : MeasurableSet K) (hJ : MeasurableSet J) (φ : ι → Foundation.Parabolic.Vec3 → ℝ) (hφ : ∀ (i : ι), Measurable (φ i)) (hφbound : ∀ (i : ι) (x : Foundation.Parabolic.Vec3), |φ i x| ≤ 1) (a : ι → ℝ → Foundation.Parabolic.Vec3) (haMeas : ∀ (i : ι), AEMeasurable (a i) (MeasureTheory.volume.restrict J)) (C : ι → ℝ) (haBound : ∀ (i : ι), ∀ t ∈ J, Foundation.Parabolic.vec3EuclideanNorm (a i t) ≤ C i) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (∑ i : ι, φ i z.1 • a i z.2)) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))

Bounded measurable time coefficients yield an L² finite-rank field on a finite space-time rectangle.

theorem CKN.Leray.l2_distance_le_of_lintegral_sq_le {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f g : α → E} {δ : ℝ} (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) (hδ : 0 ≤ δ) (herror : ∫⁻ (x : α), ‖f x - g x‖ₑ ^ 2 ∂μ ≤ ENNReal.ofReal δ ^ 2) : dist (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.MemLp.toLp g hg) ≤ δ

The space-time squared-integral error controls distance in L².

theorem CKN.Leray.tendsto_toLp_of_tendsto_lintegral_sq {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {f : ℕ → α → E} {g : α → E} (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 μ) (hg : MeasureTheory.MemLp g 2 μ) (herror : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : α), ‖f n x - g x‖ₑ ^ 2 ∂μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.MemLp.toLp (f n) ⋯) Filter.atTop (nhds (MeasureTheory.MemLp.toLp g hg))

Convergence of the squared-integral errors gives strong convergence in L² on a finite-measure region.

theorem CKN.Leray.exists_strong_l2_limit_of_lintegral_approximations {α : Type u_1} {E : Type u_2} [MeasurableSpace α] [NormedAddCommGroup E] [CompleteSpace E] {μ : MeasureTheory.Measure α} (f : ℕ → α → E) (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 μ) (P : ℕ → ℕ → α → E) (hPmem : ∀ (m n : ℕ), MeasureTheory.MemLp (P m n) 2 μ) (hP : ∀ (m : ℕ), ∃ (g : ↥(MeasureTheory.Lp E 2 μ)), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.MemLp.toLp (P m n) ⋯) Filter.atTop (nhds g)) (happrox : ∀ (ε : ℝ), 0 < ε → ∃ (m : ℕ), ∀ (n : ℕ), ∫⁻ (x : α), ‖f n x - P m n x‖ₑ ^ 2 ∂μ ≤ ENNReal.ofReal ε ^ 2) : ∃ (g : ↥(MeasureTheory.Lp E 2 μ)), Filter.Tendsto (fun (n : ℕ) => MeasureTheory.MemLp.toLp (f n) ⋯) Filter.atTop (nhds g)

Uniformly accurate finite-rank approximations that converge at each fixed rank make the original L² sequence converge.

theorem CKN.Leray.tendsto_lintegral_prod_sq_finite_rank_of_uniform_coefficients {ι : Type u_1} [Fintype ι] {K : Set Foundation.Parabolic.Vec3} {J : Set ℝ} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict K)] [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict J)] (hK : MeasurableSet K) (hJ : MeasurableSet J) (φ : ι → Foundation.Parabolic.Vec3 → ℝ) (hφ : ∀ (i : ι) (x : Foundation.Parabolic.Vec3), |φ i x| ≤ 1) (a : ℕ → ι → ℝ → Foundation.Parabolic.Vec3) (b : ι → ℝ → Foundation.Parabolic.Vec3) (hcoef : ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ t ∈ J, Foundation.Parabolic.vec3EuclideanNorm (a n i t - b i t) ≤ ε) : Filter.Tendsto (fun (n : ℕ) => ∫⁻ (z : Foundation.Parabolic.Vec3 × ℝ), ‖WithLp.toLp 2 (∑ i : ι, φ i z.1 • a n i z.2 - ∑ i : ι, φ i z.1 • b i z.2)‖ₑ ^ 2 ∂(MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J)) Filter.atTop (nhds 0)

Uniform convergence of finitely many time coefficients implies convergence of the corresponding finite-rank fields in space-time squared integral.

theorem CKN.Leray.tendsto_toLp_finite_rank_of_uniform_coefficients {ι : Type u_1} [Fintype ι] {K : Set Foundation.Parabolic.Vec3} {J : Set ℝ} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict K)] [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict J)] (hK : MeasurableSet K) (hJ : MeasurableSet J) (φ : ι → Foundation.Parabolic.Vec3 → ℝ) (hφ : ∀ (i : ι) (x : Foundation.Parabolic.Vec3), |φ i x| ≤ 1) (a : ℕ → ι → ℝ → Foundation.Parabolic.Vec3) (b : ι → ℝ → Foundation.Parabolic.Vec3) (hcoef : ∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop, ∀ t ∈ J, Foundation.Parabolic.vec3EuclideanNorm (a n i t - b i t) ≤ ε) (hf : ∀ (n : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (∑ i : ι, φ i z.1 • a n i z.2)) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))) (hg : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (∑ i : ι, φ i z.1 • b i z.2)) 2 ((MeasureTheory.volume.restrict K).prod (MeasureTheory.volume.restrict J))) : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (∑ i : ι, φ i z.1 • a n i z.2)) ⋯) Filter.atTop (nhds (MeasureTheory.MemLp.toLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => WithLp.toLp 2 (∑ i : ι, φ i z.1 • b i z.2)) hg))

Finite-rank fields with uniformly convergent time coefficients converge strongly in L² on a finite space-time rectangle.