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

The box divergence formula from trace integrability

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

Statement

Let a≤b. If F is continuous on K, has derivative field A on O outside a countable s, and τ_A is integrable on K, then the box integral of δF equals Φ_a,b(F), the upper-minus-lower signed face sum.

\[\int_K\delta F\,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.
  • a≤b coordinatewise (zero-width coordinates are allowed).
  • s⊆P is countable; F is continuous on K; for every x∈O∖s, HasFDerivAt F (A x) x.
  • τ_A is integrable on K with respect to volume.
  • 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.

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

The off-countable derivative hypothesis produces δF=τ_A a.e. on K.

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

coordinateDivergence_wrapped_toPi_trace_ae_of_hasFDerivAt_off_countable.

2. Derive coordinate-divergence integrability

Transfer the assumed trace integrability to δF through that equality.

\[\tau_A\in L^1(K)\Longrightarrow\delta F\in L^1(K).\]
Corresponding Lean step

integrableOn_coordinateDivergence_wrapped_of_integrableOn_trace_of_hasFDerivAt_off_countable.

3. Supply the two derived inputs to the box formula

The earlier wrapper now applies with the original endpoint, continuity, derivative and countability data plus the derived equality and integrability.

\[\int_K\delta F\,dx=\Phi_{a,b}(F).\]
Corresponding Lean step

integral_coordinateDivergence_toPi_box_of_hasFDerivAt_off_countable ... hdiv_ae Hi_coord.

Lean statement · integral_coordinateDivergence_toPi_box_of_integrableOn_trace_of_hasFDerivAt_off_countable

This version removes two caller obligations by proving them locally, but does not remove the explicit trace-integrability 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 integral_coordinateDivergence_toPi_box_of_integrableOn_trace_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)
    (Hi_trace : IntegrableOn (fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i)
      (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_integrableOn_trace_of_hasFDerivAt_off_countable

The source first the off-countable derivative hypothesis produces δF=τ_A a.e. on K. It finishes as follows: The earlier wrapper now applies with the original endpoint, continuity, derivative and countability data plus the derived equality and integrability. 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 integral_coordinateDivergence_toPi_box_of_integrableOn_trace_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)
    (Hi_trace : IntegrableOn (fun x => ∑ i, F' x (Pi.single i (1 : ℝ)) i)
      (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 hdiv_ae := coordinateDivergence_wrapped_toPi_trace_ae_of_hasFDerivAt_off_countable
    a b F F' s hs Hd
  have Hi_coord :=
    integrableOn_coordinateDivergence_wrapped_of_integrableOn_trace_of_hasFDerivAt_off_countable
    a b F F' s hs Hd Hi_trace
  exact integral_coordinateDivergence_toPi_box_of_hasFDerivAt_off_countable
    a b hle F F' s hs Hc Hd hdiv_ae Hi_coord

/-- If the normal component of a Pi-space vector field vanishes on every
lower and upper face of a finite box, then Mathlib's signed face-term sum is
zero.

This is a boundary-value producer for the finite-box divergence route.  It only
turns explicit componentwise zero boundary values into a zero signed face term;
it does not prove compact support, tail decay, weighted integration by parts,
whole-space limits, generator domains, invariant laws, or reversibility. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • No boundary cancellation is asserted.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

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.