Compactness Local Pairing

Supporting estimates for the Navier–Stokes development.

theorem CKN.Leray.inner_toLp_vec3_eq_integral_dot_measure (μ : MeasureTheory.Measure Foundation.Parabolic.Vec3) (f g : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3) (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) : inner ℝ (MeasureTheory.MemLp.toLp f hf) (MeasureTheory.MemLp.toLp g hg) = ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, (f x).ofLp i * (g x).ofLp i ∂μ

The Hilbert pairing in vector-valued L² is the coordinatewise spatial dot-product integral for an arbitrary measure.

theorem CKN.Leray.inner_cutoff_indicator_eq_local_inner {C : Set Foundation.Parabolic.Vec3} (hC : MeasurableSet C) (f : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (χ : Foundation.Parabolic.Vec3 → ℝ) (hχone : ∀ x ∈ C, χ x = 1) (hfGlobal : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (f x)) 2 MeasureTheory.volume) (hfLocal : MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (f x)) 2 (MeasureTheory.volume.restrict C)) (w : Foundation.Parabolic.Vec3 → Foundation.Parabolic.L2Vec3) (hwLocal : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict C)) : inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (f x)) hfGlobal) (MeasureTheory.MemLp.toLp (C.indicator w) ⋯) = inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (f x)) hfLocal) (MeasureTheory.MemLp.toLp w hwLocal)

A test extended by zero turns a global cutoff pairing into the local pairing wherever the cutoff equals one.

theorem CKN.Leray.weak_local_slices_of_weak_cutoff {C : Set Foundation.Parabolic.Vec3} (hC : MeasurableSet C) (u : ℕ → Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (χ : Foundation.Parabolic.Vec3 → ℝ) (hχone : ∀ x ∈ C, χ x = 1) (hglobal : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (u n x)) 2 MeasureTheory.volume) (hlocal : ∀ (n : ℕ), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u n x)) 2 (MeasureTheory.volume.restrict C)) (V : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 MeasureTheory.volume)) (hweak : ∀ (w : ↥(MeasureTheory.Lp (WithLp 2 ((i : Fin 3) → (fun (x : Fin 3) => ℝ) i)) 2 MeasureTheory.volume)), Filter.Tendsto (fun (n : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => χ x • WithLp.toLp 2 (u n x)) ⋯) w) Filter.atTop (nhds (inner ℝ V w))) (w : ↥(MeasureTheory.Lp Foundation.Parabolic.L2Vec3 2 (MeasureTheory.volume.restrict C))) : Filter.Tendsto (fun (n : ℕ) => inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => WithLp.toLp 2 (u n x)) ⋯) w) Filter.atTop (nhds (inner ℝ (MeasureTheory.MemLp.toLp (fun (x : Foundation.Parabolic.Vec3) => ↑↑V x) ⋯) w))

Weak convergence of global cutoff slices restricts to weak convergence on any measurable region where the cutoff is one.