Weak spatial derivatives on individual time slices

Spatial weak-derivative identities pass to limits of smooth approximations on a fixed ball.

theorem ESS.vorticity_sliceWeakPartial_of_tendsto {B : Set CKN.Foundation.Parabolic.Vec3} {j : Fin 3} (hBmeas : MeasurableSet B) {f g : ℕ → CKN.Foundation.Parabolic.Vec3 → ℝ} {F G : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : ∀ (n : ℕ), ContDiff ℝ (↑⊤) (f n)) (hg : ∀ (n : ℕ), MeasureTheory.MemLp (f n) 2 (MeasureTheory.volume.restrict B)) (hDg : ∀ (n : ℕ), MeasureTheory.MemLp (g n) 2 (MeasureTheory.volume.restrict B)) (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict B)) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict B)) (hFconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (f n - F) 2 (MeasureTheory.volume.restrict B)) Filter.atTop (nhds 0)) (hGconv : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (g n - G) 2 (MeasureTheory.volume.restrict B)) Filter.atTop (nhds 0)) (hderiv : ∀ (n : ℕ), ∀ x ∈ B, CKN.spatialDeriv (f n) j x = g n x) : CKN.HasWeakPartialDerivOn B j F G

If smooth functions and their spatial derivatives converge in L² on a ball, the derivative limit is the weak spatial derivative of the function limit.