Iterated gradients of a scalar function

The gradient of a scalar function on a real inner product space E is an E-valued field; its Fréchet derivative is an E →L[ℝ] E-valued field, and each further derivative adds one continuous-linear direction on the left. This file names these basis-free target spaces and the classical chain of derivative fields that lands in them.

TauCeti.IteratedGradient E j is the target after j derivatives of the gradient: E at j = 0 and E →L[ℝ] IteratedGradient E j at j + 1, with the operator norm. TauCeti.iteratedGradientChain f j is the corresponding field of f: the gradient at j = 0 and the Fréchet derivative of the previous field at j + 1. Its order-one member is the derivative of the gradient, which is the Hessian of f represented as an endomorphism of E.

Implementation notes

The target spaces are produced by the reducible recursion TauCeti.iteratedGradientModel, which bundles each space with its normed structure in a TauCeti.IteratedGradientModel. Both are public because TauCeti.IteratedGradient is indexed by them: at a concrete order the space and its normed, complete structures are recovered by unfolding the recursion rather than by transport.

Main declarations

• TauCeti.IteratedGradient: the basis-free target of an iterated gradient.
• TauCeti.iteratedGradientChain: the classical derivative fields of a scalar function.
• TauCeti.contDiffAt_iteratedGradientChain: the jth field of a Cⁿ function is Cᵐ when m + j + 1 ≤ n.
• TauCeti.hasCompactSupport_iteratedGradientChain: every field of a compactly supported function is compactly supported.

structure TauCeti.IteratedGradientModel : Type (u + 1)

The normed-space data underlying an iterated gradient.

• Space : Type u

  The carrier space for the iterated gradient.

• normedAddCommGroup : NormedAddCommGroup self.Space

  The normed additive commutative group structure on Space.

• normedSpace : NormedSpace ℝ self.Space

  The normed ℝ-space structure on Space.

@[reducible]

noncomputable def TauCeti.iteratedGradientModel (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] : ℕ → IteratedGradientModel

The recursively bundled target of an iterated gradient.

Equations

• One or more equations did not get rendered due to their size.
• TauCeti.iteratedGradientModel E 0 = { Space := E, normedAddCommGroup := inst✝¹, normedSpace := inst✝ }

@[reducible, inline]

abbrev TauCeti.IteratedGradient (E : Type u) [NormedAddCommGroup E] [NormedSpace ℝ E] (j : ℕ) : Type u

The target of an iterated gradient, indexed by the number of derivative directions added beyond the gradient. At j = 0 this is the gradient vector E; each successor adds one continuous-linear derivative direction on the left.

Equations

• TauCeti.IteratedGradient E j = (TauCeti.iteratedGradientModel E j).Space

@[instance_reducible]

noncomputable instance TauCeti.instNormedAddCommGroupIteratedGradient {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : ℕ) : NormedAddCommGroup (IteratedGradient E j)

Equations

• TauCeti.instNormedAddCommGroupIteratedGradient j = (TauCeti.iteratedGradientModel E j).normedAddCommGroup

@[instance_reducible]

noncomputable instance TauCeti.instNormedSpaceRealIteratedGradient {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] (j : ℕ) : NormedSpace ℝ (IteratedGradient E j)

Equations

• TauCeti.instNormedSpaceRealIteratedGradient j = (TauCeti.iteratedGradientModel E j).normedSpace

instance TauCeti.instCompleteSpaceIteratedGradient {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] (j : ℕ) : CompleteSpace (IteratedGradient E j)

noncomputable def TauCeti.iteratedGradientChain {F : Type u} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (f : F → ℝ) (j : ℕ) : F → IteratedGradient F j

The classical derivative fields of a scalar function, in the basis-free nested-linear-map types TauCeti.IteratedGradient. Index zero is the gradient and each successor is the Fréchet derivative of the preceding field.

Equations

• TauCeti.iteratedGradientChain f 0 = fun (x : F) => gradient f x
• TauCeti.iteratedGradientChain f j.succ = fderiv ℝ (TauCeti.iteratedGradientChain f j)

@[simp]

theorem TauCeti.iteratedGradientChain_zero {F : Type u} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (f : F → ℝ) : iteratedGradientChain f 0 = gradient f

@[simp]

theorem TauCeti.iteratedGradientChain_succ {F : Type u} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (f : F → ℝ) (j : ℕ) : iteratedGradientChain f (j + 1) = fderiv ℝ (iteratedGradientChain f j)

theorem TauCeti.contDiffAt_iteratedGradientChain {F : Type u} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {f : F → ℝ} {x : F} {m n : WithTop ℕ∞} (hf : ContDiffAt ℝ n f x) (j : ℕ) (h : m + ↑j + 1 ≤ n) : ContDiffAt ℝ m (iteratedGradientChain f j) x

The jth iterated-gradient field is C^m at a point whenever the scalar function is C^n there with m + j + 1 ≤ n.

theorem TauCeti.tsupport_iteratedGradientChain_subset {F : Type u} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] (f : F → ℝ) (j : ℕ) : tsupport (iteratedGradientChain f j) ⊆ tsupport f

Iterated gradients do not enlarge the topological support of a scalar function. No differentiability assumption is needed.

theorem TauCeti.hasCompactSupport_iteratedGradientChain {F : Type u} [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] {f : F → ℝ} (hf : HasCompactSupport f) (j : ℕ) : HasCompactSupport (iteratedGradientChain f j)

Every field in the iterated-gradient chain of a compactly supported function has compact support.