ASTIS mathematical exposition

A continuous product-rule trace is integrable on a closed box

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

Statement

For endpoints a,b and fields χ,G,ℓ,B, if σ(x)=Σ_i(M(x)e_i)_i is continuous on K, then σ is Lebesgue-integrable 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\sigma\in C^0(K)\Longrightarrow\sigma\in L^1(K,dx).\]

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.
Only σ is assumed continuous on K. No separate continuity of χ,ℓ,G,B, no derivative correctness, and no endpoint-order premise.

Mathematical proof

1. Integrate a continuous function over a compact box

K is a compact finite-dimensional closed box. A continuous real function on such a set is integrable for restricted Lebesgue measure.

\[K\text{ compact},\quad \sigma\in C^0(K)\Longrightarrow \sigma\in L^1(K,dx).\]

Corresponding Lean step

htrace.integrableOn_compact isCompact_Icc.

Lean statement · integrableOn_smul_vectorField_trace_of_continuousOn

This solves the trace-integrability obligation only after trace continuity has been supplied. The supplied fields are not asserted to be derivatives.

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 integrableOn_smul_vectorField_trace_of_continuousOn
    {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) → ℝ))
    (htrace : ContinuousOn
      (fun x => ∑ i, ((χ x • G' x + (χ' x).smulRight (G x))
        (Pi.single i (1 : ℝ))) i)
      (Set.Icc a b)) :
    IntegrableOn
      (fun x => ∑ i, ((χ x • G' x + (χ' x).smulRight (G x))
        (Pi.single i (1 : ℝ))) i)
      (Set.Icc a b) volume

Exact module and namespace context

Lean proof · integrableOn_smul_vectorField_trace_of_continuousOn

K is a compact finite-dimensional closed box. A continuous real function on such a set is integrable for restricted Lebesgue measure. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.

theorem integrableOn_smul_vectorField_trace_of_continuousOn
    {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) → ℝ))
    (htrace : ContinuousOn
      (fun x => ∑ i, ((χ x • G' x + (χ' x).smulRight (G x))
        (Pi.single i (1 : ℝ))) i)
      (Set.Icc a b)) :
    IntegrableOn
      (fun x => ∑ i, ((χ x • G' x + (χ' x).smulRight (G x))
        (Pi.single i (1 : ℝ))) i)
      (Set.Icc a b) volume :=
  htrace.integrableOn_compact isCompact_Icc

/-- Scalar cutoff vanishing outside the open Pi-box implies Mathlib's finite-box
signed face-term sum is zero for the cutoff-smul vector field.

Regularity of the cutoff-smul field is not addressed here; this is only the
finite-box support-to-face producer. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Compact-box integrability does not imply whole-space integrability.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ContinuousOn.integrableOn_compact
isCompact_Icc

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: ContinuousOn.integrableOn_compact — 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.