Samplinglib mathematical lesson

Define pointwise coordinate divergence

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

Read this first

Mathematical 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).\]

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.

Download module (.lean)

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

Exact module and namespace context

Proof roadmap

1Evaluate 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.

Full assumptions and notation

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 verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

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.

Download module (.lean)

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

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.

Sources, dependencies, and reuse

Source and reuse

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

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