Physlib.Mathematics.Calculus.Gradient

Elementary rules for the gradient

i. Overview

Mathlib defines the gradient `∇ f x` of a real-valued function on a real Hilbert space as the Riesz representative of its Fréchet derivative, but records no rules for the algebraic operations on `f` beyond constants. This file collects the elementary rules used throughout the classical mechanics of Physlib: a gradient is unchanged by adding a constant, it commutes with multiplication by a constant, the gradient of the quadratic form `⟪y, y⟫` is `2 • y`, and the gradient of a coordinate functional on Euclidean space is the corresponding basis vector.

These are the rules needed to differentiate Lagrangians and Hamiltonians of the form `kinetic − potential` with respect to positions and velocities.

These are rules for Mathlib's `gradient` on an abstract real Hilbert space. They are distinct from `Physlib.SpaceAndTime.Space.Derivatives.Grad`, whose `Space.grad` is a coordinate-valued operator on the structure `Space d`; nothing there applies to `EuclideanSpace ℝ (Fin 1)` or to a general inner product space. The file is deliberately real: two of its rules (`gradient_const_mul` and `gradient_inner_self`) are specific to real scalars, so the remaining ones are stated over `ℝ` as well.

ii. Key results

- `gradient_add_const` : `∇ (f + c) = ∇ f`. - `gradient_const_mul` : `∇ (c * f) = c • ∇ f` for differentiable `f`. - `gradient_inner_self` : `∇ (fun y => ⟪y, y⟫) x = 2 • x`. - `gradient_const_mul_inner_self` : `∇ (fun y => c * ⟪y, y⟫) x = (2 * c) • x`. - `gradient_coord` : `∇ (fun y => y i) x = EuclideanSpace.single i 1`. - `gradient_comp_coord` : `∇ (fun y => f (y i)) x = f' • EuclideanSpace.single i 1` when `HasDerivAt f f' (x i)`.

iii. Table of contents

A. Gradients and constants
B. Gradients of quadratic forms
C. Coordinate functionals on Euclidean space

iv. References

Mathlib, `Mathlib.Analysis.Calculus.Gradient.Basic`.

A. Gradients and constants

Adding a constant does not change the Fréchet derivative, hence not the gradient; multiplying by a constant scales both.

B. Gradients of quadratic forms

The quadratic form `y ↦ ⟪y, y⟫` has derivative `v ↦ 2 ⟪x, v⟫` at `x`, whose Riesz representative is `2 • x`.

C. Coordinate functionals on Euclidean space

The coordinate functional `y ↦ y i` on `EuclideanSpace ℝ ι` is the continuous linear map `EuclideanSpace.proj i`, whose Riesz representative is the basis vector `EuclideanSpace.single i 1`.

12 declarations

theorem

$\nabla (f + c) = \nabla f$

#gradient_add_const

Let $F$ be a real Hilbert space and $f: F \to \mathbb{R}$ be a function. For any constant $c \in \mathbb{R}$ and any point $x \in F$ , the gradient of the function $y \mapsto f(y) + c$ at $x$ is equal to the gradient of $f$ at $x$ . That is, $\nabla (f + c)(x) = \nabla f(x)$ .

theorem

$\nabla(cf) = c \nabla f$ for Differentiable $f$

#gradient_const_mul

Let $F$ be a real Hilbert space and $f: F \to \mathbb{R}$ be a real-valued function. For any constant $c \in \mathbb{R}$ and any point $x \in F$ at which $f$ is differentiable, the gradient of the function $y \mapsto c f(y)$ at $x$ is equal to the constant $c$ multiplied by the gradient of $f$ at $x$ . In symbols, $\nabla (c f)(x) = c \cdot \nabla f(x)$ .

theorem

$\nabla \langle y, y \rangle = 2x$

#gradient_inner_self

Let $F$ be a real Hilbert space. For any $x \in F$ , the gradient of the function $f: F \to \mathbb{R}$ defined by $f(y) = \langle y, y \rangle$ at the point $x$ is given by $\nabla f(x) = 2x$ .

theorem

$\nabla (c \langle y, y \rangle) = (2c)x$

#gradient_const_mul_inner_self

Let $F$ be a real inner product space. For any scalar $c \in \mathbb{R}$ and any point $x \in F$ , the gradient of the function $y \mapsto c \langle y, y \rangle$ at $x$ is given by $\nabla (c \langle y, y \rangle)(x) = (2c)x.$

theorem

$\nabla y_i = e_i$

#gradient_coord

Let $\iota$ be a finite index set and let $\mathbb{R}^\iota$ denote the real Euclidean space. For any index $i \in \iota$ and any point $x \in \mathbb{R}^\iota$ , the gradient of the $i$ -th coordinate functional $y \mapsto y_i$ is equal to the $i$ -th standard basis vector $e_i$ (where $e_i$ has a $1$ at index $i$ and $0$ elsewhere).

theorem

$\nabla (f(y_i)) = f' \mathbf{e}_i$

#gradient_comp_coord

Let $\iota$ be a finite index set and $x$ be a point in the Euclidean space $\mathbb{R}^\iota$ . Let $f: \mathbb{R} \to \mathbb{R}$ be a function that has a derivative $f'$ at the $i$ -th coordinate $x_i$ of $x$ . Then the gradient of the function mapping $y$ to $f(y_i)$ at the point $x$ is given by $\nabla (y \mapsto f(y_i))|_x = f' \mathbf{e}_i$ where $\mathbf{e}_i$ is the $i$ -th standard basis vector (represented by `EuclideanSpace.single i 1`).

theorem

Chain Rule for Gradients: $\nabla (\phi \circ f) = \phi' \cdot \nabla f$

#comp_hasGradientAt

Let $f$ be a real-valued function defined on a real Hilbert space that has a gradient $f'$ at the point $x$ . Let $\phi: \mathbb{R} \to \mathbb{R}$ be a function with a derivative $\phi'$ at the value $f(x)$ . Then the composite function $y \mapsto \phi(f(y))$ has a gradient at $x$ given by $\nabla (\phi \circ f)(x) = \phi' \cdot f'$ where $\phi' \cdot f'$ denotes the scaling of the vector $f'$ by the scalar $\phi'$ .

theorem

The gradient of $y \mapsto \langle a, y \rangle$ is $a$

#hasGradientAt_inner_left

Let $F$ be a real Hilbert space. For any vectors $a, x \in F$ , the gradient of the linear functional $y \mapsto \langle a, y \rangle$ at the point $x$ is $a$ .

theorem

The gradient of $y \mapsto \langle y, a \rangle$ is $a$

#hasGradientAt_inner_right

Let $F$ be a real Hilbert space. For any vectors $a, x \in F$ , the gradient of the function $y \mapsto \langle y, a \rangle$ at the point $x$ is $a$ .

theorem

$\nabla \langle y, y \rangle = 2x$

#hasGradientAt_inner_self

Let $F$ be a real Hilbert space. For any $x \in F$ , the gradient of the function $f(y) = \langle y, y \rangle$ at the point $x$ is $2x$ .

theorem

$\nabla \|x\| = \|x\|^{-1} x$ for $x \neq 0$

#hasGradientAt_norm

Let $F$ be a real Hilbert space. For any $x \in F$ such that $x \neq 0$ , the gradient of the norm function $y \mapsto \|y\|$ at the point $x$ is the unit vector in the direction of $x$ , given by $\|x\|^{-1} x$ .

theorem

The gradient of the coordinate functional $y \mapsto y_i$ is the basis vector $e_i$

#hasGradientAt_coord

Let $\iota$ be a finite index set and $E = \text{EuclideanSpace } \mathbb{R} \iota$ be the corresponding real Euclidean space. For any index $i \in \iota$ and any point $x \in E$ , the gradient of the $i$ -th coordinate functional $f(y) = y_i$ at $x$ is the $i$ -th standard basis vector $e_i$ (represented by `EuclideanSpace.single i 1`), which has a value of $1$ at index $i$ and $0$ elsewhere.

Physlib.Mathematics.Calculus.Gradient

Elementary rules for the gradient

i. Overview

ii. Key results

iii. Table of contents

iv. References

A. Gradients and constants

B. Gradients of quadratic forms

C. Coordinate functionals on Euclidean space

∇(f+c)=∇f\nabla (f + c) = \nabla f∇(f+c)=∇f

∇(cf)=c∇f\nabla(cf) = c \nabla f∇(cf)=c∇f for Differentiable fff

∇⟨y,y⟩=2x\nabla \langle y, y \rangle = 2x∇⟨y,y⟩=2x

∇(c⟨y,y⟩)=(2c)x\nabla (c \langle y, y \rangle) = (2c)x∇(c⟨y,y⟩)=(2c)x

∇yi=ei\nabla y_i = e_i∇yi​=ei​

∇(f(yi))=f′ei\nabla (f(y_i)) = f' \mathbf{e}_i∇(f(yi​))=f′ei​

Chain Rule for Gradients: ∇(ϕ∘f)=ϕ′⋅∇f\nabla (\phi \circ f) = \phi' \cdot \nabla f∇(ϕ∘f)=ϕ′⋅∇f

The gradient of y↦⟨a,y⟩y \mapsto \langle a, y \rangley↦⟨a,y⟩ is aaa

The gradient of y↦⟨y,a⟩y \mapsto \langle y, a \rangley↦⟨y,a⟩ is aaa

∇⟨y,y⟩=2x\nabla \langle y, y \rangle = 2x∇⟨y,y⟩=2x

∇∥x∥=∥x∥−1x\nabla \|x\| = \|x\|^{-1} x∇∥x∥=∥x∥−1x for x≠0x \neq 0x=0

The gradient of the coordinate functional y↦yiy \mapsto y_iy↦yi​ is the basis vector eie_iei​

$\nabla (f + c) = \nabla f$

$\nabla(cf) = c \nabla f$ for Differentiable $f$

$\nabla \langle y, y \rangle = 2x$

$\nabla (c \langle y, y \rangle) = (2c)x$

$\nabla y_i = e_i$

$\nabla (f(y_i)) = f' \mathbf{e}_i$

Chain Rule for Gradients: $\nabla (\phi \circ f) = \phi' \cdot \nabla f$

The gradient of $y \mapsto \langle a, y \rangle$ is $a$

The gradient of $y \mapsto \langle y, a \rangle$ is $a$

$\nabla \langle y, y \rangle = 2x$

$\nabla \|x\| = \|x\|^{-1} x$ for $x \neq 0$

The gradient of the coordinate functional $y \mapsto y_i$ is the basis vector $e_i$