Weak derivatives as limits of smooth approximations

The bootstrap of thm:vorticity-regularity of the Escauriaza–Seregin–Šverák manuscript produces weak derivatives as L² limits of derivatives of smooth approximations. This file records the completeness step, the passage to the limit in the weak identities, and the pointwise form of constant-coefficient weak identities for backward mollifications at points whose kernel support lies inside the domain.

theorem CKN.vorticityL2_exists_limit {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ℝ} (hf : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 μ) (hcauchy : Filter.Tendsto (fun (p : ℕ × ℕ) => MeasureTheory.eLpNorm (f p.1 - f p.2) 2 μ) Filter.atTop (nhds 0)) : ∃ (g : α → ℝ), MeasureTheory.MemLp g 2 μ ∧ Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - g) 2 μ) Filter.atTop (nhds 0)

A sequence which is Cauchy in L² has an L² limit.

theorem CKN.vorticity_tendsto_integral_mul {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {a : ℕ → α → ℝ} {A φ : α → ℝ} (ha : ∀ (n : ℕ), MeasureTheory.MemLp (a n) 2 μ) (hA : MeasureTheory.MemLp A 2 μ) (hφ : MeasureTheory.MemLp φ 2 μ) (hconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (a n - A) 2 μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), a n x * φ x ∂μ) Filter.atTop (nhds (∫ (x : α), A x * φ x ∂μ))

Pairings against a fixed square-integrable function pass to L² limits.

theorem CKN.vorticity_memLp_two_of_continuous_compact {W : Set (Foundation.Parabolic.Vec3 × ℝ)} {φ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : Continuous φ) (hφc : HasCompactSupport φ) : MeasureTheory.MemLp φ 2 (MeasureTheory.volume.restrict W)

A continuous compactly supported function is square integrable for every restriction of Lebesgue measure.

theorem CKN.vorticity_setIntegral_mul_spatialPartial {W : Set (Foundation.Parabolic.Vec3 × ℝ)} {F ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : ContDiff ℝ (↑⊤) F) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψW : tsupport ψ ⊆ W) (j : Fin 3) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in W, F z * spatialPartial ψ j z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ) in W, spatialPartial F j z * ψ z

Smooth integration by parts in a spatial direction, restricted to a set containing the support of the test.

theorem CKN.vorticity_weakPartial_of_tendsto {W : Set (Foundation.Parabolic.Vec3 × ℝ)} {w : ℕ → Foundation.Parabolic.Vec3 × ℝ → ℝ} (hw : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (w n)) {f g : Foundation.Parabolic.Vec3 × ℝ → ℝ} {j : Fin 3} (hwL2 : ∀ (n : ℕ), MeasureTheory.MemLp (w n) 2 (MeasureTheory.volume.restrict W)) (hdwL2 : ∀ (n : ℕ), MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (w n) j z) 2 (MeasureTheory.volume.restrict W)) (hfL2 : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict W)) (hgL2 : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict W)) (hf : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (w n - f) 2 (MeasureTheory.volume.restrict W)) Filter.atTop (nhds 0)) (hg : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm ((fun (z : Foundation.Parabolic.Vec3 × ℝ) => spatialPartial (w n) j z) - g) 2 (MeasureTheory.volume.restrict W)) Filter.atTop (nhds 0)) (ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ) : ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ W → ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in W, f z * spatialPartial ψ j z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ) in W, g z * ψ z

If smooth functions converge in L²(W) together with one spatial derivative, then the limit of the derivatives is the weak derivative of the limit on W.