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

Zero inserted-face components give zero box divergence integral

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

Statement

Let a≤b and let F:P→P be continuous on K, have derivative A(x) at each x∈O∖s for a countable s, and have integrable trace τ_A on K. Assume additionally: For every coordinate i and every z∈Fin n→ℝ, F_i(I_i^{b_i}z)=0 and F_i(I_i^{a_i}z)=0. These quantify over whole hyperplanes, not only the face boxes. Then the integral of δF over K is zero.

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

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.
  • For every coordinate i and every z∈Fin n→ℝ, F_i(I_i^{b_i}z)=0 and F_i(I_i^{a_i}z)=0. These quantify over whole hyperplanes, not only the face boxes.

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. Produce the zero signed face sum

Each boundary component function is zero everywhere on its parametrizing hyperplane, so its integral over the corresponding face box is zero. Summing upper-minus-lower zeros gives Φ=0.

\[\forall i,z,\ F_i(I_i^{b_i}z)=F_i(I_i^{a_i}z)=0\Longrightarrow\Phi_{a,b}(F)=0.\]
Corresponding Lean step

signedFaceTermSum_eq_zero_of_boundary_component_eq_zero a b F with the stated boundary/support premises.

2. Combine with the conditional zero-face theorem

The original regularity and trace-integrability data satisfy the finite-box divergence theorem. Its zero-face corollary uses the just-proved Φ=0 to give the zero box integral.

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

integral_coordinateDivergence_toPi_box_eq_zero_of_integrableOn_trace_of_hasFDerivAt_off_countable a b hle F F' s hs Hc Hd Hi_trace (...).

Lean statement · integral_coordinateDivergence_toPi_box_eq_zero_of_boundary_component_eq_zero

The derivative field F′ is supplied and is required to be correct only on O∖s. The chosen boundary/support premise replaces hfaces, but does not replace any regularity or 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_eq_zero_of_boundary_component_eq_zero
    {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)
    (hupper : ∀ (i : Fin (n + 1)) (x : Fin n → ℝ),
      F (i.insertNth (b i) x) i = 0)
    (hlower : ∀ (i : Fin (n + 1)) (x : Fin n → ℝ),
      F (i.insertNth (a i) x) i = 0) :
    ∫ 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))) = 0

Exact module and namespace context

Lean proof · integral_coordinateDivergence_toPi_box_eq_zero_of_boundary_component_eq_zero

The source first each boundary component function is zero everywhere on its parametrizing hyperplane, so its integral over the corresponding face box is zero. Summing upper-minus-lower zeros gives Φ=0. It finishes as follows: The original regularity and trace-integrability data satisfy the finite-box divergence theorem. Its zero-face corollary uses the just-proved Φ=0 to give the zero box integral. 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_eq_zero_of_boundary_component_eq_zero
    {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)
    (hupper : ∀ (i : Fin (n + 1)) (x : Fin n → ℝ),
      F (i.insertNth (b i) x) i = 0)
    (hlower : ∀ (i : Fin (n + 1)) (x : Fin n → ℝ),
      F (i.insertNth (a i) x) i = 0) :
    ∫ 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))) = 0 := by
  exact integral_coordinateDivergence_toPi_box_eq_zero_of_integrableOn_trace_of_hasFDerivAt_off_countable
    a b hle F F' s hs Hc Hd Hi_trace
    (signedFaceTermSum_eq_zero_of_boundary_component_eq_zero a b F hupper hlower)

/-- Finite-box coordinate-divergence integral vanishes from `Function.update`
boundary-value hypotheses.

This is the `Function.update`-shaped companion to
`integral_coordinateDivergence_toPi_box_eq_zero_of_boundary_component_eq_zero`.
It is intended as a staging point for later compact-support or cutoff leaves.
It still does not prove compact support, tail decay, whole-space weighted IBP,
generator domains, invariant laws, or reversibility. -/

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.

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.