Stability Slice Gradient Common

Supporting estimates for the Navier–Stokes development.

theorem CKN.stability_ae_slice_weak_partial_of_forall_test {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} (hΩ : IsOpen Ω) {u g : Foundation.Parabolic.ParabolicPoint → ℝ} (j : Fin 3) (hloc : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => u (x, s)) Ω MeasureTheory.volume ∧ MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => g (x, s)) Ω MeasureTheory.volume) (hslice : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ Ω → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∫ (x : Foundation.Parabolic.Vec3) in Ω, u (x, s) * (fderiv ℝ ψ x) (basisVec j) + g (x, s) * ψ x = 0) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, HasWeakPartialDerivOn Ω j (fun (x : Vec 3) => u (x, s)) fun (x : Vec 3) => g (x, s)

A slice integration-by-parts identity known separately for each spatial test function holds simultaneously for all tests outside one null set.