The gradient is an isometric conjugate-linear image of the Fréchet derivative

Mathlib defines gradient f x, written ∇ f x, as the Riesz representative (InnerProductSpace.toDual 𝕜 F).symm (fderiv 𝕜 f x) of the Fréchet derivative of a scalar function on an inner product space, and develops its differential calculus. This file records the three consequences of the defining formula that come from toDual being a conjugate-linear isometric equivalence: the gradient has the same norm as the derivative, it is additive, and it is conjugate-homogeneous. Since toDual is moreover continuous, the gradient of an arbitrary function is Borel measurable, as the Fréchet derivative is.

These are exactly what is needed to see a family of gradients as a conjugate-linear, norm-preserving image of the corresponding family of derivatives. Over ℝ it is linear; for instance, φ ↦ ∇ φ is linear on real-valued test functions, and ‖∇ φ‖ may be estimated by any theorem about ‖Dφ‖.

Main declarations

• TauCeti.norm_gradient_eq_norm_fderiv: ‖∇ f x‖ = ‖fderiv 𝕜 f x‖.
• TauCeti.gradient_add: additivity of the gradient at a point of differentiability.
• TauCeti.gradient_const_smul: ∇ (c • f) x = conj c • ∇ f x.
• TauCeti.gradient_of_notMem_tsupport: the gradient vanishes off the topological support.
• TauCeti.measurable_gradient: the gradient of any function is measurable.
• ContDiff.gradient_right: over ℝ, where toDual is linear, the gradient of a C^{m+1} function is Cᵐ.

theorem TauCeti.norm_gradient_eq_norm_fderiv {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (f : F → 𝕜) (x : F) : ‖gradient f x‖ = ‖fderiv 𝕜 f x‖

The gradient has the same norm as the Fréchet derivative it represents: toDual is an isometry.

theorem TauCeti.gradient_add {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f g : F → 𝕜} {x : F} (hf : DifferentiableAt 𝕜 f x) (hg : DifferentiableAt 𝕜 g x) : gradient (f + g) x = gradient f x + gradient g x

The gradient is additive wherever both summands are differentiable.

theorem TauCeti.gradient_const_smul {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} (c : 𝕜) : gradient (c • f) x = (starRingEnd 𝕜) c • gradient f x

The gradient is conjugate-homogeneous: toDual is conjugate-linear, so scaling the function by c scales the gradient by conj c. Over ℝ the conjugation is the identity.

@[simp]

theorem TauCeti.gradient_of_notMem_tsupport {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {f : F → 𝕜} {x : F} (h : x ∉ tsupport f) : gradient f x = 0

The gradient vanishes off the topological support of the function, as the Fréchet derivative does.

theorem TauCeti.measurable_gradient {𝕜 : Type u_1} {F : Type u_2} [RCLike 𝕜] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] [MeasurableSpace F] [BorelSpace F] (f : F → 𝕜) : Measurable (gradient f)

The gradient of an arbitrary function is Borel measurable, as is its Fréchet derivative (measurable_fderiv); no differentiability is assumed, the gradient being 0 where f is not differentiable.

theorem ContDiff.gradient_right {E : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {m n : WithTop ℕ∞} {f : E → ℝ} (hf : ContDiff ℝ n f) (hmn : m + 1 ≤ n) : ContDiff ℝ m (gradient f)

Over ℝ the Riesz isomorphism is a linear isometry, so the gradient of a C^{m+1} function is Cᵐ, just as its Fréchet derivative is.