ASTIS mathematical exposition

Vanishing outside the open box forces both boundary component zeros

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

Statement

For arbitrary endpoints a,b and F:P→P, assume F(x)=0 at every x∉O. Then for every i and every x∈P, replacing x_i by either b_i or a_i makes the i-th component of F vanish.

\[F|_{P\setminus O}=0\Longrightarrow\bigl[\forall i,x,\ F_i(x[i\leftarrow b_i])=0\ \land\ F_i(x[i\leftarrow a_i])=0\bigr].\]

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; ∀x∉O, F(x)=0. No endpoint-order or regularity hypothesis.

Mathematical proof

1. An endpoint update cannot lie in the open box

Membership in O after an upper update would require b_i<b_i; after a lower update it would require a_i<a_i. Both are impossible, independently of the other coordinates.

\[x[i\leftarrow b_i]\notin O,\qquad x[i\leftarrow a_i]\notin O.\]

Corresponding Lean step

Apply Pi-box membership at coordinate i; lt_irrefl contradicts the resulting strict self-inequality.

2. Apply whole-vector vanishing and project

The off-box assumption gives F equal to the zero vector at each update. Projecting to coordinate i gives both claimed scalar zeros.

\[F(x[i\leftarrow c])=0\Longrightarrow F_i(x[i\leftarrow c])=0,\quad c=a_i,b_i.\]

Corresponding Lean step

congrArg (fun y => y i) (hoff ... hxnot) in both branches.

Lean statement · update_boundary_component_eq_zero_of_eq_zero_off_univ_pi_Ioo

The output is a conjunction of two universally quantified statements, upper and lower. It does not require differentiability on the boundary.

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 update_boundary_component_eq_zero_of_eq_zero_off_univ_pi_Ioo
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hoff : ∀ x ∉ (Set.univ.pi fun i => Set.Ioo (a i) (b i)), F x = 0) :
    (∀ (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ),
        F (Function.update x i (b i)) i = 0) ∧
      (∀ (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ),
        F (Function.update x i (a i)) i = 0)

Exact module and namespace context

Lean proof · update_boundary_component_eq_zero_of_eq_zero_off_univ_pi_Ioo

The source first membership in O after an upper update would require b_i<b_i; after a lower update it would require a_i<a_i. Both are impossible, independently of the other coordinates. It finishes as follows: The off-box assumption gives F equal to the zero vector at each update. Projecting to coordinate i gives both claimed scalar zeros. Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem update_boundary_component_eq_zero_of_eq_zero_off_univ_pi_Ioo
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hoff : ∀ x ∉ (Set.univ.pi fun i => Set.Ioo (a i) (b i)), F x = 0) :
    (∀ (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ),
        F (Function.update x i (b i)) i = 0) ∧
      (∀ (i : Fin (n + 1)) (x : Fin (n + 1) → ℝ),
        F (Function.update x i (a i)) i = 0) := by
  constructor
  · intro i x
    have hxnot : Function.update x i (b i) ∉
        (Set.univ.pi fun j => Set.Ioo (a j) (b j)) := by
      intro hx
      have hlt : b i < b i := by
        simpa using (hx i (Set.mem_univ _)).2
      exact (lt_irrefl (b i)) hlt
    exact congrArg (fun y => y i) (hoff (Function.update x i (b i)) hxnot)
  · intro i x
    have hxnot : Function.update x i (a i) ∉
        (Set.univ.pi fun j => Set.Ioo (a j) (b j)) := by
      intro hx
      have hlt : a i < a i := by
        simpa using (hx i (Set.mem_univ _)).1
      exact (lt_irrefl (a i)) hlt
    exact congrArg (fun y => y i) (hoff (Function.update x i (a i)) hxnot)

/-- Off-open-box vanishing implies Mathlib's finite-box signed face-term sum
is zero.

This composes `update_boundary_component_eq_zero_of_eq_zero_off_univ_pi_Ioo`
with the update-shaped face-term producer.  It still does not prove how the
off-open-box vanishing hypothesis arises; compact support and tail decay remain
separate leaves. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Off-open-box vanishing is assumed, not derived from decay.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

Function.update

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