Samplinglib
Lean gate not recorded for this source state main · 0e31a3cda412
ASTIS mathematical exposition

Full field continuity implies continuity of the product-rule trace

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

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).\]

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

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

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.

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_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))

/-- Closed-box integrability for the trace of the cutoff-smul product-rule
derivative, assuming that trace expression is continuous on the closed box.

This is a compact-box integrability handoff only.  It does not prove continuity
of the trace from component assumptions, construct a smooth cutoff, prove tail
decay, or pass from finite boxes to whole-space weighted integration by parts. -/

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.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

  • continuous_apply
  • Continuous.comp_continuousOn
  • ContinuousOn.clm_apply

Mathematical sources

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.