ASTIS mathematical exposition

A supplied Fréchet derivative gives the coordinate trace

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

Statement

For finite-dimensional Euclidean V, if F:V→V has Fréchet derivative A:V→L[ℝ]V at x, its coordinate divergence at x is the sum of the diagonal components A(e_i)_i.

\[DF(x)=A\quad\Longrightarrow\quad\operatorname{Div}F(x)=\sum_i(Ae_i)_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, A:V→L[ℝ]V, x∈V, and HasFDerivAt F A x.

Mathematical proof

1. Differentiate each scalar component

Let p_i:V→ℝ be continuous linear coordinate projection. Composing p_i with the derivative of F gives the derivative p_i∘A of F_i at x.

\[D F_i(x)=p_i\circ A.\]

Corresponding Lean step

PiLp.proj; pr.hasFDerivAt.comp x hF.

2. Restrict the derivative to the coordinate line and sum

The derivative along e_i is (p_i∘A)(e_i)=(Ae_i)_i. Substitute these identities into the finite sum defining divergence.

\[\partial_iF_i(x)=(Ae_i)_i,\qquad\operatorname{Div}F(x)=\sum_i(Ae_i)_i.\]

Corresponding Lean step

hcomp.hasLineDerivAt (EuclideanSpace.single i 1); hline.lineDeriv; Finset.sum_congr.

Lean statement · coordinateDivergence_eq_sum_fderiv_apply_of_hasFDerivAt

`HasFDerivAt F F' x` supplies a concrete continuous linear derivative F′. The proof identifies each line derivative; it does not simply assume the trace formula.

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_fderiv_apply_of_hasFDerivAt
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    {F : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι}
    {F' : EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι}
    {x : EuclideanSpace ℝ ι}
    (hF : HasFDerivAt F F' x) :
    coordinateDivergence F x =
      ∑ i, F' (EuclideanSpace.single i (1 : ℝ)) i

Exact module and namespace context

Lean proof · coordinateDivergence_eq_sum_fderiv_apply_of_hasFDerivAt

The source first let p_i:V→ℝ be continuous linear coordinate projection. Composing p_i with the derivative of F gives the derivative p_i∘A of F_i at x. It finishes as follows: The derivative along e_i is (p_i∘A)(e_i)=(Ae_i)_i. Substitute these identities into the finite sum defining divergence. Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem coordinateDivergence_eq_sum_fderiv_apply_of_hasFDerivAt
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    {F : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι}
    {F' : EuclideanSpace ℝ ι →L[ℝ] EuclideanSpace ℝ ι}
    {x : EuclideanSpace ℝ ι}
    (hF : HasFDerivAt F F' x) :
    coordinateDivergence F x =
      ∑ i, F' (EuclideanSpace.single i (1 : ℝ)) i := by
  dsimp [coordinateDivergence]
  refine Finset.sum_congr rfl ?_
  intro i _hi
  let pr : EuclideanSpace ℝ ι →L[ℝ] ℝ :=
    PiLp.proj (p := 2) (𝕜 := ℝ) (fun _ : ι => ℝ) i
  have hcomp : HasFDerivAt (fun y : EuclideanSpace ℝ ι => F y i)
      (pr.comp F') x := by
    simpa [pr, Function.comp_def] using (pr.hasFDerivAt.comp x hF)
  have hline := hcomp.hasLineDerivAt (EuclideanSpace.single i (1 : ℝ))
  simpa [pr] using hline.lineDeriv

/-- If a vector field is differentiable at `x`, then the ASTIS coordinate
divergence is the Mathlib divergence-theorem summand with `fderiv ℝ F x`.

This is the pointwise bridge needed before instantiating Mathlib's integral
divergence theorem.  It does not assert integrability, face terms, boundary
decay, integration by parts, generator domains, or invariant-law consequences. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Pointwise only: no trace integrability or boundary statement.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence

Mathlib API called (external library)

PiLp.proj
ContinuousLinearMap.hasFDerivAt
HasFDerivAt.comp
HasFDerivAt.hasLineDerivAt
HasLineDerivAt.lineDeriv
Finset.sum_congr

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: HasFDerivAt.hasLineDerivAt — Exact existing Mathlib theorem used by the documented argument.
Called library/source declaration: HasLineDerivAt.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.