Divergence as the trace of a derivative

MathlibAnnex.divergence

def

Defines divergence without choosing coordinates.

Statement

Let be a finite-dimensional real normed vector space and . The divergence of at is the trace of its real Fréchet derivative:

Definition

Here denotes the continuous linear derivative when it exists, and the zero map otherwise, following the source’s total derivative convention. The RHS takes the trace of that endomorphism. Thus this definition still returns a value at a nondifferentiability point; it does not assert that the classical derivative exists there.

Assumptions

The definition accepts every function and every point . It imposes neither differentiability nor a measure. Finite dimensionality is part of the definition’s domain; dimension zero is allowed.

Conclusion

The output is a real number. At a point where is differentiable, it is the usual divergence. In coordinates with a finite index set and coordinate vectors , For a differentiable field, writing identifies the summand as . The empty sum in dimension zero is zero.

The trace is independent of a basis. The coordinate identity follows by representing the derivative in the coordinate basis and summing its diagonal entries; the exact coordinate lemma is cited below. This identity also holds for the library’s total derivative convention.

def divergence [FiniteDimensional ℝ E] (W : E → E) (x : E) : ℝ :=
  LinearMap.trace ℝ E (fderiv ℝ W x).toLinearMap

noncomputable section
open Set
open scoped BigOperators

namespace MathlibAnnex
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project