Gradient Chain Rule for a Continuous Linear Map

This is a technical gradient chain rule for composition with a continuous linear map.

Let $E$ and $F$ be complete real inner-product normed additive groups, and let $q:E\to F$ be a continuous linear map. Let $f:F\to\mathbb R$ and $x\in E$, and assume that $f$ is differentiable at $q(x)$. Then

where $q^*:F\to E$ is the Hilbert-space adjoint of $q$.

The result provides the differential identity needed to transport smooth test functions and their gradient energies between inner-product spaces.

Formalization Note: The map is represented by ContinuousLinearMap, its adjoint by q.adjoint, and the conclusion uses the Mathlib gradient.

Original Lean declaration header

Within namespace FunctionalInequalities.Poincare.SmoothTest. Shown in its original module context. Proof omitted.

theorem gradient_comp_projection {f : F → ℝ} {x : E}
    (hf : DifferentiableAt ℝ f (q x)) :
    gradient (f ∘ q) x = q.adjoint (gradient f (q x))

Module navigation

Module: Poincare/SmoothTest/Transport.

Next: admissible_map_linearIsometryEquiv_iff.

Source excerpt, lines 47–49 · Frozen source 408915f.