Local Slope Equals Gradient Norm

This is the pointwise identification of the one-moving-point local slope with the canonical Hilbert-space gradient norm.

Let $E$ be a complete real inner-product normed space, let $f:E\to\mathbb R$, and let $x\in E$. Assume that $f$ is Fréchet differentiable at $x$. Then the local slope apply of $f$ at $x$ equals the extended nonnegative real number obtained from the norm of the gradient:

Here $\nabla f(x)$ is the canonical Hilbert gradient and the right-hand side is an ENNReal value in $[0,\infty]$. The Lean declaration is apply_eq_norm_gradient_readable; no nontriviality assumption on $E$ or on the derivative is imposed.

Original Lean declaration header

Within namespace FunctionalInequalities.Energy.LocalSlope. Shown in its original module context. Proof omitted.

theorem apply_eq_norm_gradient
    (f : E → ℝ) (x : E) (hf : DifferentiableAt ℝ f x) :
    apply f x = ENNReal.ofReal ‖gradient f x‖

Module navigation

Module: Energy/LocalSlope/Gradient.

Definition modules: Energy/LocalSlope/Basic.

Next: admissible_iff_memLp_gradient.

Source excerpt, lines 31–33 · Frozen source 408915f.