Samplinglib mathematical lesson

Full field continuity implies continuity of the product-rule trace

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

Read this first

Mathematical statement

For endpoints a,b and fields χ,G,ℓ,B, if all four maps are continuous on K (ℓ and B in their operator norm topologies), then σ, the product-rule trace expression, is continuous on K.

\[M(x)v=\chi(x)B(x)v+\ell(x)[v]G(x),\qquad \sigma(x)=\sum_i\left[\chi(x)(B(x)e_i)_i+\ell(x)[e_i]G_i(x)\right],\qquad \chi,\ell,G,B\in C^0(K)\Longrightarrow\sigma\in C^0(K).\]

Lean statement · continuousOn_smul_vectorField_trace_of_components

This wrapper strengthens the inputs to full field continuity for convenience; it does not change the output trace 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 continuousOn_smul_vectorField_trace_of_components
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (χ' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (G' : (Fin (n + 1) → ℝ) →
      (Fin (n + 1) → ℝ) →L[ℝ] (Fin (n + 1) → ℝ))
    (hχc : ContinuousOn χ (Set.Icc a b))
    (hχ'c : ContinuousOn χ' (Set.Icc a b))
    (hGc : ContinuousOn G (Set.Icc a b))
    (hG'c : ContinuousOn G' (Set.Icc a b)) :
    ContinuousOn
      (fun x => ∑ i, ((χ x • G' x + (χ' x).smulRight (G x))
        (Pi.single i (1 : ℝ))) i)
      (Set.Icc a b)

Exact module and namespace context

Proof roadmap

1Extract the needed scalar component continuities
Coordinate projections preserve continuity of G. Evaluation at fixed e_i preserves continuity of ℓ and B; composing the latter with coordinate i gives continuity of (B e_i)_i.
2Apply the scalar-component trace theorem
The preceding lemma now assembles the continuous products and finite sum into σ.

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.
a,b∈P; K=[a,b]={x:∀i,a_i≤x_i≤b_i} is the closed box and O=∏_i(a_i,b_i) is the open box. All unspecified integrals and a.e. assertions use Lebesgue volume on P, restricted to K when indicated.
χ:P→ℝ, G:P→P, ℓ:P→(P→L[ℝ]ℝ), and B:P→(P→L[ℝ]P). Set M(x)=χ(x)B(x)+ℓ(x).smulRight(G(x)); thus M(x)v=χ(x)B(x)v+ℓ(x)[v]G(x). Set σ(x)=Σ_i(M(x)e_i)_i.
χ, ℓ, G and B are each ContinuousOn K as maps into their stated scalar, vector, or continuous-linear-map spaces.
No derivative correctness or a≤b hypothesis.

Mathematical proof

1. Extract the needed scalar component continuities

Coordinate projections preserve continuity of G. Evaluation at fixed e_i preserves continuity of ℓ and B; composing the latter with coordinate i gives continuity of (B e_i)_i.

\[G,\ell,B\in C^0(K)\Longrightarrow G_i,\ \ell[e_i],\ (B e_i)_i\in C^0(K).\]

Corresponding Lean step

(continuous_apply i).comp_continuousOn hGc; hχ'c.clm_apply continuousOn_const; (continuous_apply i).comp_continuousOn (hG'c.clm_apply continuousOn_const).

2. Apply the scalar-component trace theorem

The preceding lemma now assembles the continuous products and finite sum into σ.

\[\sigma\in C^0(K).\]

Corresponding Lean step

continuousOn_smul_vectorField_trace_of_component_continuousOn a b χ χ' G G' hχc ....

Lean verification

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

Lean proof · continuousOn_smul_vectorField_trace_of_components

The source first coordinate projections preserve continuity of G. Evaluation at fixed e_i preserves continuity of ℓ and B; composing the latter with coordinate i gives continuity of (B e_i)_i. It finishes as follows: The preceding lemma now assembles the continuous products and finite sum into σ. Intermediate steps below identify the actual helper calls and the conditions each one needs.

Download module (.lean)

theorem continuousOn_smul_vectorField_trace_of_components
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (χ' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (G' : (Fin (n + 1) → ℝ) →
      (Fin (n + 1) → ℝ) →L[ℝ] (Fin (n + 1) → ℝ))
    (hχc : ContinuousOn χ (Set.Icc a b))
    (hχ'c : ContinuousOn χ' (Set.Icc a b))
    (hGc : ContinuousOn G (Set.Icc a b))
    (hG'c : ContinuousOn G' (Set.Icc a b)) :
    ContinuousOn
      (fun x => ∑ i, ((χ x • G' x + (χ' x).smulRight (G x))
        (Pi.single i (1 : ℝ))) i)
      (Set.Icc a b) := by
  exact continuousOn_smul_vectorField_trace_of_component_continuousOn a b χ χ' G G' hχc
    (fun i => (continuous_apply i).comp_continuousOn hGc)
    (fun i => hχ'c.clm_apply continuousOn_const)
    (fun i =>
      (continuous_apply i).comp_continuousOn
        (hG'c.clm_apply continuousOn_const))

Exact module and namespace context

Scope and omitted-condition boundaries

Continuity of a named derivative field is not proof that it is an actual derivative.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.continuousOn_smul_vectorField_trace_of_component_continuousOn

Mathlib API called (external library)

continuous_apply
Continuous.comp_continuousOn
ContinuousOn.clm_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: AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.continuousOn_smul_vectorField_trace_of_component_continuousOn — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
Called library/source declaration: ContinuousOn.clm_apply — 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.