secondDeriv
plain-language theorem explainer
Definition of the second directional derivative ∂_μ ∂_ν f at x as the real derivative at zero of the first directional derivative in the μ direction, evaluated along the coordinate ray in the ν direction. Researchers deriving Laplacians and radial potentials in relativistic field equations cite this operator. It is realized as a direct one-line composition of the real derivative with the first partial along the shifted ray.
Claim. $∂_μ ∂_ν f(x) := d/ds|_{s=0} ∂_μ f(x + s e_ν)$, where ∂_μ is the directional derivative of f along the μ-th coordinate axis and e_ν the corresponding standard basis vector.
background
The module builds calculus operators on maps from four-dimensional space to the reals by means of directional derivatives along straight coordinate rays. The ray in direction ν from base point x is the affine line obtained by adding the parameter times the ν-th standard basis vector. The first directional derivative is recovered as the real derivative at parameter zero of the function composed with this ray.
proof idea
The definition is a one-line wrapper that applies the real derivative operator to the map sending parameter s to the first directional derivative of f in the μ direction evaluated at the point shifted from x along the ν ray by s.
why it matters
This supplies the primitive for the Laplacian, formed by summing the three spatial diagonal instances. It is invoked in the proofs that the Laplacian of 1/r^n equals n(n-1)/r^{n+2} away from the origin, discharging calculus axioms required for potential theory. In the Recognition framework it furnishes the second-order operators appearing in the Hamiltonian and field equations, aligned with the forced spatial dimension of three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.