Samplinglib mathematical lesson

Scalar support with continuous trace components gives zero box integral

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

Read this first

Mathematical statement

Let a≤b, χ:P→ℝ, G:P→P, and a countable s⊆P. χ and G are continuous on K. At every x∈O∖s, HasFDerivAt χ (ℓ x) x and HasFDerivAt G (B x) x. For every i, x↦ℓ(x)[e_i] and x↦(B(x)e_i)_i are continuous on K. Full operator-valued continuity of ℓ or B is not assumed. Function.support χ⊆O. Then the wrapped coordinate divergence of H=χG integrates to zero over 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\int_K\delta(\chi G)\,dx=0.\]

Lean statement · integral_coordinateDivergence_toPi_box_eq_zero_of_scalar_support_subset_univ_pi_Ioo_of_component_continuous

The component assumptions on χ′ and G′ are only directional/diagonal scalar continuities, not full continuity of those operator fields. Product differentiation is justified separately by hχd and hGd.

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 integral_coordinateDivergence_toPi_box_eq_zero_of_scalar_support_subset_univ_pi_Ioo_of_component_continuous
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ) (hle : a ≤ b)
    (χ : (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) → ℝ))
    (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable)
    (hχc : ContinuousOn χ (Set.Icc a b))
    (hGc : ContinuousOn G (Set.Icc a b))
    (hχ'c : ∀ i, ContinuousOn
      (fun x => χ' x (Pi.single i (1 : ℝ))) (Set.Icc a b))
    (hG'c : ∀ i, ContinuousOn
      (fun x => (G' x (Pi.single i (1 : ℝ))) i) (Set.Icc a b))
    (hχd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt χ (χ' x) x)
    (hGd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt G (G' x) x)
    (hχsupp : Function.support χ ⊆
      (Set.univ.pi fun i => Set.Ioo (a i) (b i))) :
    ∫ x in Set.Icc a b, coordinateDivergence
        (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
          (WithLp.toLp 2 ((χ (WithLp.ofLp y)) • G (WithLp.ofLp y)) :
            EuclideanSpace ℝ (Fin (n + 1))))
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) = 0

Exact module and namespace context

Proof roadmap

1Extract scalar component continuity of G
Full continuity of G on K gives continuity of each scalar coordinate G_i. Combine this with the given χ, ℓ[e_i], and (B e_i)_i continuities.
2Assemble continuity of the trace expression
Each summand χ(B e_i)_i+ℓ[e_i]G_i is a sum of products of continuous scalar functions. The finite sum σ is therefore continuous on K.
3Use the trace-continuous zero integral theorem
This continuity yields compact-box trace integrability in the preceding theorem; with the unchanged derivative and scalar support assumptions it concludes the zero integral.

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.
a≤b coordinatewise; s⊆P is countable.
χ: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. Let H=χG.
χ and G are continuous on K. At every x∈O∖s, HasFDerivAt χ (ℓ x) x and HasFDerivAt G (B x) x.
For every i, x↦ℓ(x)[e_i] and x↦(B(x)e_i)_i are continuous on K. Full operator-valued continuity of ℓ or B is not assumed.
Function.support χ⊆O.

Notation and interpretation

Notation used below: For a raw field F:P→P, W_F=T∘F∘T⁻¹ and δF(x) is coordinateDivergence W_F at Tx. For a supplied linear-map field A, τ_A is its coordinate trace.
\[W_F:=T\circ F\circ T^{-1},\qquad\delta F(x):=\operatorname{Div}W_F(Tx),\qquad\tau_A(x):=\sum_i(A(x)e_i)_i.\]

Mathematical proof

1. Extract scalar component continuity of G

Full continuity of G on K gives continuity of each scalar coordinate G_i. Combine this with the given χ, ℓ[e_i], and (B e_i)_i continuities.

\[G\in C^0(K)\Longrightarrow G_i\in C^0(K).\]

Corresponding Lean step

(continuous_apply i).comp_continuousOn hGc.

2. Assemble continuity of the trace expression

Each summand χ(B e_i)_i+ℓ[e_i]G_i is a sum of products of continuous scalar functions. The finite sum σ is therefore continuous on K.

\[\sigma(x)=\sum_i[\chi(x)(B(x)e_i)_i+\ell(x)[e_i]G_i(x)]\in C^0(K).\]

Corresponding Lean step

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

3. Use the trace-continuous zero integral theorem

This continuity yields compact-box trace integrability in the preceding theorem; with the unchanged derivative and scalar support assumptions it concludes the zero integral.

\[\int_K\delta(\chi G)\,dx=0.\]

Corresponding Lean step

integral_coordinateDivergence_toPi_box_eq_zero_of_scalar_support_subset_univ_pi_Ioo_of_trace_continuous ...

Lean verification

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

Lean proof · integral_coordinateDivergence_toPi_box_eq_zero_of_scalar_support_subset_univ_pi_Ioo_of_component_continuous

The source first full continuity of G on K gives continuity of each scalar coordinate G_i. Combine this with the given χ, ℓ[e_i], and (B e_i)_i continuities. It finishes as follows: This continuity yields compact-box trace integrability in the preceding theorem; with the unchanged derivative and scalar support assumptions it concludes the zero integral. Intermediate steps below identify the actual helper calls and the conditions each one needs.

Download module (.lean)

theorem integral_coordinateDivergence_toPi_box_eq_zero_of_scalar_support_subset_univ_pi_Ioo_of_component_continuous
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ) (hle : a ≤ b)
    (χ : (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) → ℝ))
    (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable)
    (hχc : ContinuousOn χ (Set.Icc a b))
    (hGc : ContinuousOn G (Set.Icc a b))
    (hχ'c : ∀ i, ContinuousOn
      (fun x => χ' x (Pi.single i (1 : ℝ))) (Set.Icc a b))
    (hG'c : ∀ i, ContinuousOn
      (fun x => (G' x (Pi.single i (1 : ℝ))) i) (Set.Icc a b))
    (hχd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt χ (χ' x) x)
    (hGd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt G (G' x) x)
    (hχsupp : Function.support χ ⊆
      (Set.univ.pi fun i => Set.Ioo (a i) (b i))) :
    ∫ x in Set.Icc a b, coordinateDivergence
        (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
          (WithLp.toLp 2 ((χ (WithLp.ofLp y)) • G (WithLp.ofLp y)) :
            EuclideanSpace ℝ (Fin (n + 1))))
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) = 0 := by
  exact integral_coordinateDivergence_toPi_box_eq_zero_of_scalar_support_subset_univ_pi_Ioo_of_trace_continuous
    a b hle χ χ' G G' s hs hχc hGc hχd hGd
    (continuousOn_smul_vectorField_trace_of_component_continuousOn a b χ χ' G G' hχc
      (fun i => (continuous_apply i).comp_continuousOn hGc) hχ'c hG'c)
    hχsupp

Exact module and namespace context

Scope and omitted-condition boundaries

Finite-box zero integral only; no whole-space passage or invariant-law conclusion.
The support/vanishing assumption is imposed on χ; no value-one plateau or range [0,1] assumption is needed in this theorem.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

continuous_apply
Continuous.comp_continuousOn

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: AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.integral_coordinateDivergence_toPi_box_eq_zero_of_scalar_support_subset_univ_pi_Ioo_of_trace_continuous — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
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.