Pressure Gradient Slice

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.Core.Step4.pressure_hasWeakPartialDerivOn_of_contDiffOn {B : Set Foundation.Parabolic.Vec3} (hB : IsOpen B) {H : Foundation.Parabolic.Vec3 → ℝ} {i : Fin 3} (hH : ContDiffOn ℝ 1 H B) : HasWeakPartialDerivOn B i H fun (x : Vec 3) => (fderiv ℝ H x) (basisVec i)

A function which is (C^1) on an open set has its classical coordinate derivatives as weak derivatives on that set.