Samplinglib mathematical lesson

The pointwise scalar-vector product derivative

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

Read this first

Mathematical statement

At x∈P, suppose χ:P→ℝ has derivative ℓ:P→L[ℝ]ℝ and G:P→P has derivative B:P→L[ℝ]P. Then H=χG has derivative M=χ(x)B+ℓ.smulRight(G(x)) at x.

\[D(\chi G)(x)[v]=\chi(x)B[v]+\ell[v]G(x).\]

Lean statement · hasFDerivAt_smul_vectorField_of_hasFDerivAt

`smulRight (G x)` sends v to ℓ(v)G(x). The theorem certifies a supplied derivative, not merely a formal product expression.

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 hasFDerivAt_smul_vectorField_of_hasFDerivAt
    {n : ℕ}
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (χ' : (Fin (n + 1) → ℝ) →L[ℝ] ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (G' : (Fin (n + 1) → ℝ) →L[ℝ] (Fin (n + 1) → ℝ))
    (x : Fin (n + 1) → ℝ)
    (hχ : HasFDerivAt χ χ' x)
    (hG : HasFDerivAt G G' x) :
    HasFDerivAt (fun y => χ y • G y)
      (χ x • G' + χ'.smulRight (G x)) x

Exact module and namespace context

Proof roadmap

1Differentiate the scalar-vector bilinear operation
In the increment v, the first-order change is the old scalar times the vector increment plus the scalar increment times the old vector. The product of two increments is higher order, yielding the displayed derivative.

Full assumptions and notation

All objects and hypotheses

n∈ℕ, d=n+1≥1, P=(Fin d→ℝ) with its usual supremum norm, V=EuclideanSpace ℝ (Fin d) with its ℓ² norm. T:P→V is WithLp.toLp 2, a continuous linear equivalence, and e=T⁻¹=WithLp.ofLp.
χ:P→ℝ, G:P→P, x∈P, ℓ:P→L[ℝ]ℝ and B:P→L[ℝ]P.
HasFDerivAt χ ℓ x and HasFDerivAt G B x. No endpoints, exceptional set, or continuity-on-box parameters.

Mathematical proof

1. Differentiate the scalar-vector bilinear operation

\[(\chi G)(x+v)-(\chi G)(x)=\chi(x)B[v]+\ell[v]G(x)+o(\|v\|).\]

Corresponding Lean step

hχ.smul hG, followed by simpa, is Mathlib's HasFDerivAt.smul product rule.

Lean verification

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

Lean proof · hasFDerivAt_smul_vectorField_of_hasFDerivAt

In the increment v, the first-order change is the old scalar times the vector increment plus the scalar increment times the old vector. The product of two increments is higher order, yielding the displayed derivative. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.

Download module (.lean)

theorem hasFDerivAt_smul_vectorField_of_hasFDerivAt
    {n : ℕ}
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (χ' : (Fin (n + 1) → ℝ) →L[ℝ] ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (G' : (Fin (n + 1) → ℝ) →L[ℝ] (Fin (n + 1) → ℝ))
    (x : Fin (n + 1) → ℝ)
    (hχ : HasFDerivAt χ χ' x)
    (hG : HasFDerivAt G G' x) :
    HasFDerivAt (fun y => χ y • G y)
      (χ x • G' + χ'.smulRight (G x)) x := by
  simpa using hχ.smul hG

Exact module and namespace context

Scope and omitted-condition boundaries

No box, integration, or a.e. conclusion.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

HasFDerivAt.smul
ContinuousLinearMap.smulRight_apply

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: HasFDerivAt.smul — 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.