ASTIS mathematical exposition

The trace of a rank-one derivative term is its scalar evaluation

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

Statement

For a finite coordinate type ι, a continuous real linear functional ℓ:(ι→ℝ)→ℝ and a vector g∈(ι→ℝ), the diagonal sum of the rank-one operator v↦ℓ(v)g equals ℓ(g).

\[\sum_i\bigl((\ell\otimes g)e_i\bigr)_i=\ell(g),\qquad(\ell\otimes g)(v):=\ell(v)g.\]

All objects and hypotheses

ι is a finite type with Fintype and DecidableEq; empty ι is allowed.
P=(ι→ℝ), ℓ:P→L[ℝ]ℝ, and g∈P; no differentiability or measure.

Mathematical proof

1. Identify each diagonal term

The i-th component of ℓ(e_i)g is ℓ(e_i)g_i. By linearity and commutativity of real multiplication this equals ℓ(g_i e_i).

\[\bigl((\ell\otimes g)e_i\bigr)_i=\ell(e_i)g_i=\ell(g_i e_i).\]

Corresponding Lean step

ContinuousLinearMap.smulRight_apply; Pi.smul_apply; smul_eq_mul; mul_comm.

2. Reassemble the vector inside the linear functional

Move the finite sum inside ℓ. The standard coordinate expansion gives Σ_i g_i e_i=g, yielding ℓ(g).

\[\sum_i\ell(g_i e_i)=\ell\!\left(\sum_i g_i e_i\right)=\ell(g).\]

Corresponding Lean step

map_sum; pi_eq_sum_univ' G.

Lean statement · sum_smulRight_apply_pi_single_eq_apply

`smulRight G` constructs the rank-one continuous linear map. The prime in χ′ is merely a variable name here; no scalar function with that derivative is assumed.

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 sum_smulRight_apply_pi_single_eq_apply
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (χ' : (ι → ℝ) →L[ℝ] ℝ) (G : ι → ℝ) :
    ∑ i, ((χ'.smulRight G) (Pi.single i (1 : ℝ))) i = χ' G

Exact module and namespace context

Lean proof · sum_smulRight_apply_pi_single_eq_apply

The source first the i-th component of ℓ(e_i)g is ℓ(e_i)g_i. By linearity and commutativity of real multiplication this equals ℓ(g_i e_i). It finishes as follows: Move the finite sum inside ℓ. The standard coordinate expansion gives Σ_i g_i e_i=g, yielding ℓ(g). Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem sum_smulRight_apply_pi_single_eq_apply
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (χ' : (ι → ℝ) →L[ℝ] ℝ) (G : ι → ℝ) :
    ∑ i, ((χ'.smulRight G) (Pi.single i (1 : ℝ))) i = χ' G := by
  calc
    ∑ i, ((χ'.smulRight G) (Pi.single i (1 : ℝ))) i =
        ∑ i, χ' ((G i) • Pi.single (M := fun _ : ι => ℝ) i (1 : ℝ)) := by
      apply Finset.sum_congr rfl
      intro i _hi
      simp [ContinuousLinearMap.smulRight_apply, Pi.smul_apply, smul_eq_mul,
        mul_comm]
    _ = χ' (∑ i, (G i) • Pi.single (M := fun _ : ι => ℝ) i (1 : ℝ)) := by
      rw [map_sum]
    _ = χ' G := by rw [← pi_eq_sum_univ' G]

/-- Pointwise bridge from Mathlib's Pi-space derivative to ASTIS
`EuclideanSpace` coordinate divergence for a wrapped vector field.

This is the pointwise core needed to discharge the `hdiv_ae` assumption in the
box face-term wrapper when differentiability is available almost everywhere.
It does not prove that differentiability holds a.e. on a box, prove
integrability, prove boundary-null facts, perform integration by parts, or
prove invariant-law consequences. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Pure linear algebra, not a divergence product theorem by itself.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ContinuousLinearMap.smulRight_apply
map_sum
pi_eq_sum_univ'

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: pi_eq_sum_univ' — 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.