Samplinglib mathematical lesson

Scalar off-box vanishing gives zero product divergence integral

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

Read this first

Mathematical statement

Let a≤b, χ:P→ℝ, G:P→P and H=χG. Suppose H is continuous on K, has supplied derivative A(x) at each x∈O∖s for a countable s, and τ_A is integrable on K. Assume additionally χ(x)=0 for every x∉O. Then ∫_K δH dx=0.

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

Lean statement · integral_coordinateDivergence_toPi_box_eq_zero_of_cutoff_eq_zero_off_univ_pi_Ioo

The hypotheses are imposed on the product χG directly. No separate continuity or differentiability of χ and G is assumed or derived; A need not be presented in product-rule form.

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_cutoff_eq_zero_off_univ_pi_Ioo
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ) (hle : a ≤ b)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (F' : (Fin (n + 1) → ℝ) →
      (Fin (n + 1) → ℝ) →L[ℝ] (Fin (n + 1) → ℝ))
    (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable)
    (Hc : ContinuousOn (fun x => χ x • G x) (Set.Icc a b))
    (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt (fun x => χ x • G x) (F' x) x)
    (Hi_trace : IntegrableOn (fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i)
      (Set.Icc a b) volume)
    (hχ : ∀ x ∉ (Set.univ.pi fun i => Set.Ioo (a i) (b i)), χ x = 0) :
    ∫ 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

1Localize the product field
The scalar premise ensures χ=0 outside O, hence H=χG is zero there. The corresponding support lemma gives supp H⊆O.
2Apply the supported-field zero integral theorem
The already-assumed continuity, supplied derivative, countability and trace integrability for H combine with this support inclusion to give the zero box 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. χ:P→ℝ and G:P→P are arbitrary factors; H(x)=χ(x)G(x). A:P→(P→L[ℝ]P) is a supplied derivative field for H.
s⊆P is countable; H is continuous on K, and HasFDerivAt H (A x) x for every x∈O∖s.
τ_A(x)=Σ_i(A(x)e_i)_i is integrable on K with respect to volume.
χ(x)=0 for every x∉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. Localize the product field

The scalar premise ensures χ=0 outside O, hence H=χG is zero there. The corresponding support lemma gives supp H⊆O.

\[\operatorname{supp}H=\operatorname{supp}(\chi G)\subseteq O.\]

Corresponding Lean step

support_smul_subset_univ_pi_Ioo_of_eq_zero_off_univ_pi_Ioo a b χ G.

2. Apply the supported-field zero integral theorem

The already-assumed continuity, supplied derivative, countability and trace integrability for H combine with this support inclusion to give the zero box integral.

\[\int_K\delta H\,dx=0.\]

Corresponding Lean step

integral_coordinateDivergence_toPi_box_eq_zero_of_support_subset_univ_pi_Ioo a b hle (fun x => χ x • G x) F' s hs Hc Hd Hi_trace.

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_cutoff_eq_zero_off_univ_pi_Ioo

The source first the scalar premise ensures χ=0 outside O, hence H=χG is zero there. The corresponding support lemma gives supp H⊆O. It finishes as follows: The already-assumed continuity, supplied derivative, countability and trace integrability for H combine with this support inclusion to give the zero box 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_cutoff_eq_zero_off_univ_pi_Ioo
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ) (hle : a ≤ b)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (F' : (Fin (n + 1) → ℝ) →
      (Fin (n + 1) → ℝ) →L[ℝ] (Fin (n + 1) → ℝ))
    (s : Set (Fin (n + 1) → ℝ)) (hs : s.Countable)
    (Hc : ContinuousOn (fun x => χ x • G x) (Set.Icc a b))
    (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt (fun x => χ x • G x) (F' x) x)
    (Hi_trace : IntegrableOn (fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i)
      (Set.Icc a b) volume)
    (hχ : ∀ x ∉ (Set.univ.pi fun i => Set.Ioo (a i) (b i)), χ x = 0) :
    ∫ 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_support_subset_univ_pi_Ioo
    a b hle (fun x => χ x • G x) F' s hs Hc Hd Hi_trace
    (support_smul_subset_univ_pi_Ioo_of_eq_zero_off_univ_pi_Ioo a b χ G hχ)

Exact module and namespace context

Scope and omitted-condition boundaries

Only the finite box K is integrated. No passage to whole space, weighted integration by parts, generator domain, stationary law, or invariance follows from this wrapper alone.
Derivative values at the boundary and on the countable exceptional set are not prescribed; equality of integrands is used a.e.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

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.support_smul_subset_univ_pi_Ioo_of_eq_zero_off_univ_pi_Ioo — 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_support_subset_univ_pi_Ioo — 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.