ASTIS mathematical exposition

Define pointwise coordinate divergence

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence · def · Teaching coverage

Statement

For a finite coordinate set ι, a vector field F:V→V and x∈V, define the coordinate divergence by summing the directional derivative of its i-th component along the i-th coordinate vector. Every summand is totalized: it is zero if that one-dimensional derivative does not exist.

\[\operatorname{Div}F(x):=\sum_{i\in\iota}\operatorname{deriv}_{t=0}\bigl[t\mapsto(F(x+t e_i))_i\bigr],\qquad e_i=\operatorname{single}(i,1).\]

All objects and hypotheses

ι is a finite type with chosen finite enumeration and decidable equality; V=EuclideanSpace ℝ ι carries the Euclidean ℓ² norm. Empty ι is allowed.
F:V→V and x∈V are arbitrary; no differentiability, measurability, or support hypothesis.

Construction and meaning

1. Evaluate and sum coordinate line derivatives

For each i, restrict the scalar component F_i to the line through x in direction e_i, take Mathlib's totalized real derivative at zero, and add these finitely many scalars. This constructs a value; it is not an integration theorem.

\[\partial_i^{\rm tot}F_i(x)=\operatorname{lineDeriv}_{\mathbb R}F_i(x,e_i),\qquad \operatorname{Div}F(x)=\sum_i\partial_i^{\rm tot}F_i(x).\]

Corresponding Lean step

Definition body: finite sum of lineDeriv ℝ (fun y => F y i) x (EuclideanSpace.single i 1).

Lean statement · coordinateDivergence

The inferred finite type supplies the index set. `noncomputable def` introduces a real-valued function; it does not assert any derivative exists.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

noncomputable def coordinateDivergence
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (F : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι)
    (x : EuclideanSpace ℝ ι) : ℝ

Exact module and namespace context

Lean construction · coordinateDivergence

The body takes one totalized line derivative for each coordinate and forms their finite sum. There is no theorem being proved, and no differentiation hypothesis is hidden in this construction.

noncomputable def coordinateDivergence
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (F : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι)
    (x : EuclideanSpace ℝ ι) : ℝ :=
  ∑ i, lineDeriv ℝ (fun y : EuclideanSpace ℝ ι => F y i) x
    (EuclideanSpace.single i (1 : ℝ))

/-- Unfold the ASTIS pointwise coordinate-divergence definition. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Do not replace this definition by a classical divergence formula without establishing the needed derivatives.
A finite sum over an empty coordinate type is zero.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

lineDeriv
EuclideanSpace.single

Mathematical sources

Current ASTIS source — Exact statement and actual proof/construction authority; raw code intentionally omitted from this packet.
Existing curated module card — Existing module overview only; not a new external-source claim.
Called library/source declaration: lineDeriv — Exact existing Mathlib theorem used by the documented argument.
Existing focused test — Definition occurs in an existing example statement; no test was run.

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.