ASTIS mathematical exposition

Continuity of a scalar times a vector field on the closed box

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

Statement

For endpoints a,b and functions χ:P→ℝ and G:P→P continuous on K, the product H(x)=χ(x)G(x) is continuous on K.

\[\chi,G\in C^0(K)\quad\Longrightarrow\quad H=\chi G\in C^0(K).\]

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→ℝ and G:P→P are continuous on K; no a≤b hypothesis.

Mathematical proof

1. Apply continuity of scalar multiplication

The map x↦(χ(x),G(x)) is continuous on K, and scalar multiplication ℝ×P→P is continuous. Their composition is H.

\[H=\operatorname{smul}\circ(\chi,G).\]

Corresponding Lean step

hχ.smul hG, the ContinuousOn.smul rule.

Lean statement · continuousOn_smul_vectorField_of_continuousOn

This is a direct finite-box specialization of continuity under scalar multiplication; no derivative or face term is involved.

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 continuousOn_smul_vectorField_of_continuousOn
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hχ : ContinuousOn χ (Set.Icc a b))
    (hG : ContinuousOn G (Set.Icc a b)) :
    ContinuousOn (fun x => χ x • G x) (Set.Icc a b)

Exact module and namespace context

Lean proof · continuousOn_smul_vectorField_of_continuousOn

The map x↦(χ(x),G(x)) is continuous on K, and scalar multiplication ℝ×P→P is continuous. Their composition is H. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.

theorem continuousOn_smul_vectorField_of_continuousOn
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hχ : ContinuousOn χ (Set.Icc a b))
    (hG : ContinuousOn G (Set.Icc a b)) :
    ContinuousOn (fun x => χ x • G x) (Set.Icc a b) :=
  hχ.smul hG

/-- Pointwise Frechet derivative for a scalar cutoff times a Pi-space vector
field.

The derivative is exactly the Mathlib product-rule derivative
`χ x • G' + χ'.smulRight (G x)`.  This is only a pointwise derivative leaf; it
does not prove continuity, trace integrability, boundary cancellation, or
weighted integration by parts. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Continuity is on the closed box only; no smoothness or support premise.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ContinuousOn.smul

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.
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.