ASTIS mathematical exposition

Transfer trace integrability to coordinate divergence

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

Statement

Assume F has supplied derivative field A on O outside a countable s and τ_A is integrable on K. Then the wrapped coordinate-divergence function δF is integrable on K.

\[\tau_A\in L^1(K,dx),\quad DF=A\text{ on }O\setminus s,\quad s\text{ countable}\quad\Longrightarrow\quad\delta F\in L^1(K,dx).\]

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.
s⊆P is countable; derivative A(x) exists at every x∈O∖s.
τ_A is integrable on K. Neither a≤b nor continuity of F on K is assumed.

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. Obtain the a.e. representation equality

The off-countable trace bridge gives δF=τ_A a.e. for volume restricted to K.

\[\delta F=\tau_A\quad\text{a.e. on }K.\]

Corresponding Lean step

coordinateDivergence_wrapped_toPi_trace_ae_of_hasFDerivAt_off_countable a b F F' s hs Hd.

2. Transfer both measurability and finite integral through a.e. equality

Integrability is unchanged by replacing a function by an almost-everywhere equal one; apply this to the supplied integrable trace.

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

Corresponding Lean step

Hi_trace.congr_fun_ae hdiv_ae.symm.

Lean statement · integrableOn_coordinateDivergence_wrapped_of_integrableOn_trace_of_hasFDerivAt_off_countable

`IntegrableOn` means integrable with respect to the restricted measure. The theorem solves only the representation mismatch; trace integrability is still a premise.

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 integrableOn_coordinateDivergence_wrapped_of_integrableOn_trace_of_hasFDerivAt_off_countable
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (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)
    (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt F (F' x) x)
    (Hi_trace : IntegrableOn (fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i)
      (Set.Icc a b) volume) :
    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

Exact module and namespace context

Lean proof · integrableOn_coordinateDivergence_wrapped_of_integrableOn_trace_of_hasFDerivAt_off_countable

The source first the off-countable trace bridge gives δF=τ_A a.e. for volume restricted to K. It finishes as follows: Integrability is unchanged by replacing a function by an almost-everywhere equal one; apply this to the supplied integrable trace. Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem integrableOn_coordinateDivergence_wrapped_of_integrableOn_trace_of_hasFDerivAt_off_countable
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (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)
    (Hd : ∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s,
      HasFDerivAt F (F' x) x)
    (Hi_trace : IntegrableOn (fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i)
      (Set.Icc a b) volume) :
    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 := by
  have hdiv_ae := coordinateDivergence_wrapped_toPi_trace_ae_of_hasFDerivAt_off_countable
    a b F F' s hs Hd
  exact Hi_trace.congr_fun_ae hdiv_ae.symm

/-- Box-level signed-face divergence theorem wrapper for ASTIS coordinate
divergence.

Mathlib's Bochner divergence theorem is stated on `Fin (n + 1) → ℝ`; ASTIS
finite Euclidean pointwise calculations use `EuclideanSpace ℝ (Fin (n + 1))`.
This theorem only bridges those interfaces under an explicit a.e. equality
`hdiv_ae` between the ASTIS coordinate-divergence integrand and Mathlib's trace
summand.  The conclusion is exactly Mathlib's signed face-term formula.

It does not derive `hdiv_ae`, prove box integrability, take a whole-space
limit, prove boundary cancellation, perform weighted integration by parts,
establish generator domains, or prove invariant/reversible Gibbs laws. -/

Exact module and namespace context

Scope and omitted-condition boundaries

No concrete source-field integrability is established.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.coordinateDivergence_wrapped_toPi_trace_ae_of_hasFDerivAt_off_countable

Mathlib API called (external library)

MeasureTheory.IntegrableOn.congr_fun_ae

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