Physlib

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`.

6 declarations

theorem

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

Let FF be a real Hilbert space and f:F→Rf: F \to \mathbb{R} be a function. For any constant c∈Rc \in \mathbb{R} and any point x∈Fx \in F, the gradient of the function y↦f(y)+cy \mapsto f(y) + c at xx is equal to the gradient of ff at xx. That is, ∇(f+c)(x)=∇f(x)\nabla (f + c)(x) = \nabla f(x).

theorem

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

Let FF be a real Hilbert space and f:F→Rf: F \to \mathbb{R} be a real-valued function. For any constant c∈Rc \in \mathbb{R} and any point x∈Fx \in F at which ff is differentiable, the gradient of the function y↦cf(y)y \mapsto c f(y) at xx is equal to the constant cc multiplied by the gradient of ff at xx. In symbols, ∇(cf)(x)=c⋅∇f(x)\nabla (c f)(x) = c \cdot \nabla f(x).

theorem

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

Let FF be a real Hilbert space. For any x∈Fx \in F, the gradient of the function f:F→Rf: F \to \mathbb{R} defined by f(y)=⟨y,y⟩f(y) = \langle y, y \rangle at the point xx is given by ∇f(x)=2x\nabla f(x) = 2x.

theorem

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

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

theorem

∇yi=ei\nabla y_i = e_i

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

theorem

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

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