Directional Derivative of the Tensor Energy Form

This is a first-order directional derivative formula for the coordinate-tensor energy form.

Let $n,r\in\mathbb{N}$. Let $T,X:(\mathrm{Fin}\,r\to\mathrm{Fin}\,n)\to\mathbb{R}$, and let $H$ be a continuous linear map from $\mathrm{EuclideanSpace}\,\mathbb{R}\,(\mathrm{Fin}\,n)$ to itself. Writing energyForm for the energy functional, inner for the tensor inner product, stdMatrix H for the standard matrix of $H$, and actSum for its induced tensor action, the derivative at $\varepsilon=0$ of

is

This technical line-derivative identity can be reused in first-order variations of tensor energy expressions.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.CoordinateTensor. Shown in its original module context. Proof omitted.

theorem hasDerivAt_energyForm_line (T : (Fin r → Fin n) → ℝ)
    (H : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) (X : (Fin r → Fin n) → ℝ) :
    HasDerivAt (fun ε : ℝ => energyForm (1 + ε • H) (T + ε • X))
      (2 * inner T X - inner T (actSum (stdMatrix H) T)) 0

Module navigation

Module: Analysis/Tensor/EnergyForm.

Definition modules: Analysis/Tensor/SlotAction.

Supporting theorems: slot_derivative_sum.

Previous: slot_derivative_sum · Next: sum_mul_prod_delta_erase_erase.

Source excerpt, lines 295–298 · Frozen source 408915f.