Coord Deriv

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

theorem CKN.coordFDeriv_eq_deriv_update {d : ℕ} {f : Vec d → ℝ} {x : Vec d} (hf : DifferentiableAt ℝ f x) (i : Fin d) : (fderiv ℝ f x) (basisVec i) = deriv (fun (s : ℝ) => f (Function.update x i s)) (x i)

The ith coordinate component of the Fréchet derivative of f at x equals the ordinary derivative, at x i, of the one-variable function obtained from f by varying the ith coordinate alone: s ↦ f (Function.update x i s).