Samplinglib mathematical lesson

Use the canonical Fréchet derivative in the trace formula

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

Read this first

Mathematical statement

If F:V→V is Fréchet differentiable at x, its coordinate divergence equals the coordinate trace sum of the canonical fderiv ℝ F x.

\[F\text{ differentiable at }x\quad\Longrightarrow\quad\operatorname{Div}F(x)=\sum_i(D F(x)e_i)_i.\]

Lean statement · coordinateDivergence_eq_sum_fderiv_apply_of_differentiableAt

This removes a separately supplied derivative map only because `DifferentiableAt` is assumed; totalization alone would not justify the replacement.

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

Exact module and namespace context

Proof roadmap

1Supply the canonical derivative to the existing trace identity
Differentiability certifies that fderiv is an actual derivative at x. Substitute this witness in the preceding 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, x∈V, and DifferentiableAt ℝ F x.

Mathematical proof

1. Supply the canonical derivative to the existing trace identity

Differentiability certifies that fderiv is an actual derivative at x. Substitute this witness in the preceding theorem.

\[A:=\operatorname{fderiv}_{\mathbb R}F(x),\qquad DF(x)=A.\]

Corresponding Lean step

coordinateDivergence_eq_sum_fderiv_apply_of_hasFDerivAt hF.hasFDerivAt.

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_fderiv_apply_of_differentiableAt

Differentiability certifies that fderiv is an actual derivative at x. Substitute this witness in the preceding theorem. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.

Download module (.lean)

theorem coordinateDivergence_eq_sum_fderiv_apply_of_differentiableAt
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    {F : EuclideanSpace ℝ ι → EuclideanSpace ℝ ι}
    {x : EuclideanSpace ℝ ι}
    (hF : DifferentiableAt ℝ F x) :
    coordinateDivergence F x =
      ∑ i, fderiv ℝ F x (EuclideanSpace.single i (1 : ℝ)) i :=
  coordinateDivergence_eq_sum_fderiv_apply_of_hasFDerivAt hF.hasFDerivAt

Exact module and namespace context

Scope and omitted-condition boundaries

No claim of differentiability at other points.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence_eq_sum_fderiv_apply_of_hasFDerivAt

Mathlib API called (external library)

DifferentiableAt.hasFDerivAt

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_eq_sum_fderiv_apply_of_hasFDerivAt — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
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.