ASTIS mathematical exposition

The box divergence formula with an explicit a.e. representation bridge

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

Statement

Let a≤b, let F be continuous on K and have derivative field A on O outside a countable s. Assume explicitly both δF=τ_A a.e. on K and integrability of δF on K. Then its box integral equals the signed sum Φ_a,b(F) of upper minus lower face integrals.

\[\int_K\delta F(x)\,dx=\Phi_{a,b}(F),\qquad \Phi_{a,b}(F):=\sum_{i=0}^{d-1}\left[\int_{K_{\widehat i}}F_i(I_i^{b_i}z)\,dz-\int_{K_{\widehat i}}F_i(I_i^{a_i}z)\,dz\right]\]

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.
F:P→P and A:P→(P→L[ℝ]P) is a supplied linear-map field. Write δF(x)=Div(T∘F∘T⁻¹)(Tx) and τ_A(x)=Σ_i(A(x)e_i)_i.
For each i, K_hat_i=∏_{j≠i}[a_j,b_j] is parametrized by Fin n→ℝ; I_i^c inserts c in coordinate i, retaining the other coordinates in their original order. Φ_a,b(F) is the sum of upper-face integrals of F_i minus lower-face integrals of F_i.
a≤b coordinatewise; s⊆P countable; F continuous on K and HasFDerivAt F (A x) x on O∖s.
δF=τ_A a.e. on K is an explicit premise (`hdiv_ae`). δF is integrable on K (`Hi`).

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. Transfer the given integrability to the trace

The supplied a.e. equality carries integrability of δF to τ_A.

\[\delta F\in L^1(K),\quad\delta F=\tau_A\text{ a.e.}\Longrightarrow\tau_A\in L^1(K).\]

Corresponding Lean step

Hi.congr_fun_ae hdiv_ae.

2. Replace the integrand by its trace representative

A.e. equal functions have equal Bochner integrals for the restricted measure.

\[\int_K\delta F\,dx=\int_K\tau_A\,dx.\]

Corresponding Lean step

MeasureTheory.integral_congr_ae hdiv_ae.

3. Invoke the exact existing finite-box divergence theorem

Mathlib's theorem uses continuity on K, derivatives on O∖s, countability, endpoint order, and integrability of the trace. It returns exactly the upper-minus-lower face formula, including degenerate boxes.

\[\int_K\tau_A\,dx=\sum_i\left(\int_{K_{\widehat i}}F_i(I_i^{b_i}z)\,dz-\int_{K_{\widehat i}}F_i(I_i^{a_i}z)\,dz\right).\]

Corresponding Lean step

MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable hle F F' s hs Hc Hd Hi_trace.

Lean statement · integral_coordinateDivergence_toPi_box_of_hasFDerivAt_off_countable

This ASTIS theorem is an interface wrapper around Mathlib's integration theorem, not a fresh proof of the divergence theorem. It deliberately still takes `hdiv_ae` and `Hi` as assumptions.

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 integral_coordinateDivergence_toPi_box_of_hasFDerivAt_off_countable
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ) (hle : a ≤ b)
    (F : (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 F (Set.Icc a b))
    (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt F (F' x) x)
    (hdiv_ae :
      (fun x => coordinateDivergence
        (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
          (WithLp.toLp 2 (F (WithLp.ofLp y)) :
            EuclideanSpace ℝ (Fin (n + 1))))
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))))
      =ᵐ[volume.restrict (Set.Icc a b)]
      fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i)
    (Hi : IntegrableOn
      (fun x => coordinateDivergence
        (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
          (WithLp.toLp 2 (F (WithLp.ofLp y)) :
            EuclideanSpace ℝ (Fin (n + 1))))
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))))
      (Set.Icc a b) volume) :
    ∫ x in Set.Icc a b, coordinateDivergence
        (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
          (WithLp.toLp 2 (F (WithLp.ofLp y)) :
            EuclideanSpace ℝ (Fin (n + 1))))
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) =
      ∑ i : Fin (n + 1),
        ((∫ x in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
            F (i.insertNth (b i) x) i) -
          ∫ x in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
            F (i.insertNth (a i) x) i)

Exact module and namespace context

Lean proof · integral_coordinateDivergence_toPi_box_of_hasFDerivAt_off_countable

The source first the supplied a.e. equality carries integrability of δF to τ_A. It finishes as follows: Mathlib's theorem uses continuity on K, derivatives on O∖s, countability, endpoint order, and integrability of the trace. It returns exactly the upper-minus-lower face formula, including degenerate boxes. Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem integral_coordinateDivergence_toPi_box_of_hasFDerivAt_off_countable
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ) (hle : a ≤ b)
    (F : (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 F (Set.Icc a b))
    (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt F (F' x) x)
    (hdiv_ae :
      (fun x => coordinateDivergence
        (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
          (WithLp.toLp 2 (F (WithLp.ofLp y)) :
            EuclideanSpace ℝ (Fin (n + 1))))
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))))
      =ᵐ[volume.restrict (Set.Icc a b)]
      fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i)
    (Hi : IntegrableOn
      (fun x => coordinateDivergence
        (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
          (WithLp.toLp 2 (F (WithLp.ofLp y)) :
            EuclideanSpace ℝ (Fin (n + 1))))
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))))
      (Set.Icc a b) volume) :
    ∫ x in Set.Icc a b, coordinateDivergence
        (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
          (WithLp.toLp 2 (F (WithLp.ofLp y)) :
            EuclideanSpace ℝ (Fin (n + 1))))
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1))) =
      ∑ i : Fin (n + 1),
        ((∫ x in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
            F (i.insertNth (b i) x) i) -
          ∫ x in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
            F (i.insertNth (a i) x) i) := by
  have Hi_trace : IntegrableOn (fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i)
      (Set.Icc a b) volume :=
    Hi.congr_fun_ae hdiv_ae
  calc
    (∫ x in Set.Icc a b, coordinateDivergence
        (fun y : EuclideanSpace ℝ (Fin (n + 1)) =>
          (WithLp.toLp 2 (F (WithLp.ofLp y)) :
            EuclideanSpace ℝ (Fin (n + 1))))
        (WithLp.toLp 2 x : EuclideanSpace ℝ (Fin (n + 1)))) =
        ∫ x in Set.Icc a b, ∑ i, F' x (Pi.single i (1 : ℝ)) i := by
          exact MeasureTheory.integral_congr_ae hdiv_ae
    _ = ∑ i : Fin (n + 1),
        ((∫ x in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
            F (i.insertNth (b i) x) i) -
          ∫ x in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
            F (i.insertNth (a i) x) i) := by
          exact MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable
            (a := a) (b := b) hle F F' s hs Hc Hd Hi_trace

/-- Box-level signed-face divergence theorem wrapper for ASTIS coordinate
divergence, using Mathlib's trace-integrability hypothesis directly.

Compared with `integral_coordinateDivergence_toPi_box_of_hasFDerivAt_off_countable`,
this version no longer asks callers to provide the `hdiv_ae` representation
bridge or coordinate-divergence integrability.  Both are derived from the
open-box/off-countable derivative hypothesis and the explicit trace-integrability
assumption.

It still proves only the finite-box signed face-term formula.  It does not
prove trace integrability for a concrete vector field, whole-space/no-boundary
limits, weighted IBP, generator domains, invariant Gibbs law, reversibility,
stationarity, or KL/FI dissipation. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The signed face sum is not assumed zero. This is a finite-box formula, not a whole-space or weighted integration-by-parts theorem.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence

Mathlib API called (external library)

MeasureTheory.IntegrableOn.congr_fun_ae
MeasureTheory.integral_congr_ae
MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable

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.coordinateDivergence — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
Called library/source declaration: MeasureTheory.IntegrableOn.congr_fun_ae — Exact existing Mathlib theorem used by the documented argument.
Called library/source declaration: MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable — 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.