ASTIS mathematical exposition

Update-form boundary zeros cancel the face sum

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

Statement

For endpoints a,b and arbitrary F:P→P, assume the i-th component of F becomes zero whenever coordinate i of any x∈P is replaced by b_i, and likewise by a_i. Then Φ_a,b(F)=0.

\[\forall i,x,\ F_i(x[i\leftarrow b_i])=F_i(x[i\leftarrow a_i])=0\quad\Longrightarrow\quad\Phi_{a,b}(F)=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 is arbitrary.
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.
No a≤b, continuity, differentiability or integrability assumption.
The update zero assumptions hold for every i and every full vector x∈P.

Notation and interpretation

Notation used below: 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.
\[\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]\]

Mathematical proof

1. Convert updates to the inserted-face representation

An inserted face point already has coordinate b_i or a_i, so updating that coordinate to the same value changes nothing. The hypotheses therefore imply the inserted-face zero assumptions.

\[I_i^{c}z[i\leftarrow c]=I_i^{c}z,\qquad c\in\{a_i,b_i\}.\]

Corresponding Lean step

Function.update_eq_self; apply hupper and hlower to the corresponding i.insertNth vectors.

2. Reuse the zero-face evaluation

The converted upper and lower component identities are exactly the inputs of the preceding face-sum theorem.

\[\Phi_{a,b}(F)=0.\]

Corresponding Lean step

signedFaceTermSum_eq_zero_of_boundary_component_eq_zero a b F.

Lean statement · signedFaceTermSum_eq_zero_of_update_boundary_component_eq_zero

`Function.update` replaces one entry of a full vector; `Fin.insertNth` inserts one entry into an (n)-coordinate vector. The proof relates these representations.

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 signedFaceTermSum_eq_zero_of_update_boundary_component_eq_zero
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hupper : ∀ (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ),
      F (Function.update x i (b i)) i = 0)
    (hlower : ∀ (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ),
      F (Function.update x i (a i)) i = 0) :
    ∑ 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) = 0

Exact module and namespace context

Lean proof · signedFaceTermSum_eq_zero_of_update_boundary_component_eq_zero

The source first an inserted face point already has coordinate b_i or a_i, so updating that coordinate to the same value changes nothing. The hypotheses therefore imply the inserted-face zero assumptions. It finishes as follows: The converted upper and lower component identities are exactly the inputs of the preceding face-sum theorem. Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem signedFaceTermSum_eq_zero_of_update_boundary_component_eq_zero
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hupper : ∀ (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ),
      F (Function.update x i (b i)) i = 0)
    (hlower : ∀ (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ),
      F (Function.update x i (a i)) i = 0) :
    ∑ 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) = 0 :=
  signedFaceTermSum_eq_zero_of_boundary_component_eq_zero a b F
    (fun i x => by
      simpa [Function.update_eq_self] using hupper i (i.insertNth (b i) x))
    (fun i x => by
      simpa [Function.update_eq_self] using hlower i (i.insertNth (a i) x))

/-- If a Pi-space vector field vanishes outside the open box
`Set.univ.pi (fun i => Set.Ioo (a i) (b i))`, then its normal components
vanish after updating any coordinate to either endpoint.

This is a direct boundary producer for later compact-support or cutoff
arguments: those arguments can prove the off-open-box vanishing hypothesis,
and this leaf converts it into the update-boundary hypotheses used by the
finite-box face-term lemmas.  It does not prove compact support, tail decay,
whole-space limits, weighted integration by parts, generator domains, invariant
laws, or reversibility. -/

Exact module and namespace context

Scope and omitted-condition boundaries

No regularity result is supplied.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.signedFaceTermSum_eq_zero_of_boundary_component_eq_zero

Mathlib API called (external library)

Function.update_eq_self

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

ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.