ASTIS mathematical exposition

Unfold the coordinate-divergence convention

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence_eq_sum_lineDeriv · theorem · Teaching coverage

Statement

For arbitrary F:V→V and x∈V with a finite coordinate set, coordinate divergence is exactly the defining sum of totalized line derivatives.

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

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; no regularity assumptions.

Mathematical proof

1. Read the definition

Both sides are the same expression after expanding coordinateDivergence, so their equality requires no additional calculus.

\[\operatorname{Div}F(x)\equiv\sum_i\partial_i^{\rm tot}F_i(x).\]

Corresponding Lean step

rfl checks definitional equality.

Lean statement · coordinateDivergence_eq_sum_lineDeriv

This is an evaluation wrapper exposing the definition, not a new divergence identity.

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.

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

Exact module and namespace context

Lean proof · coordinateDivergence_eq_sum_lineDeriv

Both sides are the same expression after expanding coordinateDivergence, so their equality requires no additional calculus. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.

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

/-- If a vector field has Frechet derivative `F'` at `x`, then the ASTIS
coordinate divergence is the coordinate trace-style sum `∑ᵢ (F' eᵢ)ᵢ`.

This matches the pointwise divergence summand shape used by Mathlib's
box-integral divergence theorem.  It is still not an integration theorem or an
integration-by-parts result. -/

Exact module and namespace context

Scope and omitted-condition boundaries

No integral or derivative-existence result.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence

Mathlib API called (external library)

lineDeriv

Mathematical sources

Current ASTIS source — Exact statement and actual proof/construction authority; raw code intentionally omitted from this packet.
Existing curated module card — Existing declaration-specific attribution entry, read as documentation without a new source-equivalence verdict.
Called library/source declaration: AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
Called library/source declaration: lineDeriv — Exact existing Mathlib theorem used by the documented argument.
Existing focused test — Exact named declaration invocation located in an existing example; 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.