The pointwise scalar-vector product derivative
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.hasFDerivAt_smul_vectorField_of_hasFDerivAt · theorem · Teaching coverage
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.
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
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.
Corresponding Lean step
hχ.smul hG, followed by simpa, is Mathlib's HasFDerivAt.smul product rule.
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.
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)) xLean 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.
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 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
/-- Open-box/off-countable Frechet derivative wrapper for a scalar cutoff times
a Pi-space vector field.
This derives the `Hd` shape required by the finite-box divergence-theorem
handoffs from separate derivative hypotheses for the scalar cutoff and the
vector field on the same open-box minus exceptional set. It still does not
prove trace integrability or any no-boundary conclusion. -/Scope and omitted-condition boundaries
- No box, integration, or a.e. conclusion.
Source and reuse
ASTIS 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.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.