Continuity of the product-rule trace from exactly its scalar components
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.continuousOn_smul_vectorField_trace_of_component_continuousOn · theorem · Teaching coverage
Statement
For endpoints a,b and fields χ,G,ℓ,B, assume χ is continuous on K and, for every i, the scalar functions G_i, x↦ℓ(x)[e_i], and x↦(B(x)e_i)_i are continuous on K. Then σ(x)=Σ_i(M(x)e_i)_i is continuous on 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→ℝ, 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.
- χ is continuous on K; for every i, G_i, ℓ(·)[e_i], and (B(·)e_i)_i are continuous on K.
- No derivative-existence claim about ℓ or B; no a≤b premise; full operator-valued continuity is not required.
Mathematical proof
1. Expand one trace summand
By the definitions of scalar multiplication and smulRight, the i-th summand is χ(x)(B(x)e_i)_i+ℓ(x)[e_i]G_i(x).
Corresponding Lean step
add_apply; ContinuousLinearMap.smulRight_apply; Pi.smul_apply; smul_eq_mul.
2. Use continuity of products and the finite sum
Both products are continuous by precisely the component hypotheses. Their sum is continuous, and summing over finitely many i preserves continuity on K.
Corresponding Lean step
(hχ.mul (hG' i)).add ((hχ' i).mul (hG i)); continuousOn_finsetSum Finset.univ.
Lean statement · continuousOn_smul_vectorField_trace_of_component_continuousOn
The primes in χ′ and G′ name supplied linear-map fields. This theorem does not certify that they are derivatives; it only proves continuity of their algebraic 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.
theorem continuousOn_smul_vectorField_trace_of_component_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) → ℝ))
(hχ : ContinuousOn χ (Set.Icc a b))
(hG : ∀ i, ContinuousOn (fun x => G x i) (Set.Icc a b))
(hχ' : ∀ i, ContinuousOn
(fun x => χ' x (Pi.single i (1 : ℝ))) (Set.Icc a b))
(hG' : ∀ i, ContinuousOn
(fun x => (G' x (Pi.single i (1 : ℝ))) i) (Set.Icc a b)) :
ContinuousOn
(fun x => ∑ i, ((χ x • G' x + (χ' x).smulRight (G x))
(Pi.single i (1 : ℝ))) i)
(Set.Icc a b)Lean proof · continuousOn_smul_vectorField_trace_of_component_continuousOn
The source first by the definitions of scalar multiplication and smulRight, the i-th summand is χ(x)(B(x)e_i)_i+ℓ(x)[e_i]G_i(x). It finishes as follows: Both products are continuous by precisely the component hypotheses. Their sum is continuous, and summing over finitely many i preserves continuity on K. Intermediate steps below identify the actual helper calls and the conditions each one needs.
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_trace_of_component_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) → ℝ))
(hχ : ContinuousOn χ (Set.Icc a b))
(hG : ∀ i, ContinuousOn (fun x => G x i) (Set.Icc a b))
(hχ' : ∀ i, ContinuousOn
(fun x => χ' x (Pi.single i (1 : ℝ))) (Set.Icc a b))
(hG' : ∀ i, ContinuousOn
(fun x => (G' x (Pi.single i (1 : ℝ))) i) (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
refine continuousOn_finsetSum Finset.univ ?_
intro i _hi
have hscalar : ContinuousOn
(fun x => χ x * ((G' x (Pi.single i (1 : ℝ))) i) +
(χ' x (Pi.single i (1 : ℝ))) * G x i)
(Set.Icc a b) :=
(hχ.mul (hG' i)).add ((hχ' i).mul (hG i))
simpa [add_apply, ContinuousLinearMap.smulRight_apply, Pi.smul_apply,
smul_eq_mul] using hscalar
/-- Closed-box continuity of the cutoff-smul product-rule trace from component
continuity of the cutoff, cutoff derivative field, vector field, and vector
field derivative.
This only assembles continuity of the trace expression
`∑ i, ((χ x • G' x + (χ' x).smulRight (G x)) eᵢ)ᵢ`. It does not prove that
`χ'` or `G'` are actual derivatives, does not identify the product-rule
operator with a canonical `fderiv`, and does not prove cutoff construction,
tail decay, weighted IBP, or invariant laws. -/Scope and omitted-condition boundaries
- No differentiability, integrability or boundary cancellation is concluded.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- ContinuousOn.mul
- ContinuousOn.add
- continuousOn_finsetSum
- 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.
- 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.