Statement file: spaceGrad (Roots). This file contains exactly one declaration of the formalization's public statement surface.

noncomputable def AVenhance.spaceGrad (f : Homogenization.Vec 2 → ℝ) : Homogenization.Vec 2 → Homogenization.Vec 2

Classical gradient of a differentiable function, coordinatewise.

Equations

• AVenhance.spaceGrad f x i = (fderiv ℝ f x) (Homogenization.basisVec i)