Samplinglib mathematical lesson

Unfold the coordinate-divergence convention

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

Read this first

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

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.

Download module (.lean)

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

Proof roadmap

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

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; 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 verification

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

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.

Download module (.lean)

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

Exact module and namespace context

Scope and omitted-condition boundaries

No integral or derivative-existence result.

Sources, dependencies, and reuse

Source and reuse

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

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