Zero normal components make the signed face sum zero
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.signedFaceTermSum_eq_zero_of_boundary_component_eq_zero · theorem · Teaching coverage
Statement
For arbitrary endpoints a,b and field F:P→P, suppose F_i(I_i^{b_i}z)=0 and F_i(I_i^{a_i}z)=0 for every coordinate i and every z∈ℝ^n, not merely z in its face box. Then the signed face sum Φ_a,b(F) is zero.
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.
- Both upper and lower normal-component values vanish on their entire coordinate hyperplanes: ∀i, ∀z∈Fin n→ℝ.
Mathematical proof
1. Integrate zero on each face and sum
The two assumed zero functions have zero integrals over their corresponding face boxes. Every upper-minus-lower difference is 0−0, and the finite sum is zero.
Corresponding Lean step
simp [hupper, hlower] rewrites the actual integrands to zero.
Lean statement · signedFaceTermSum_eq_zero_of_boundary_component_eq_zero
The quantified boundary assumptions are stronger than a.e. or face-box-only vanishing. The theorem only computes the face sum.
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_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 → ℝ),
F (i.insertNth (b i) x) i = 0)
(hlower : ∀ (i : Fin (n + 1)) (x : Fin n → ℝ),
F (i.insertNth (a i) x) 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) = 0Lean proof · signedFaceTermSum_eq_zero_of_boundary_component_eq_zero
The two assumed zero functions have zero integrals over their corresponding face boxes. Every upper-minus-lower difference is 0−0, and the finite sum is zero. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.
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_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 → ℝ),
F (i.insertNth (b i) x) i = 0)
(hlower : ∀ (i : Fin (n + 1)) (x : Fin n → ℝ),
F (i.insertNth (a i) x) 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 := by
simp [hupper, hlower]
/-- Version of `signedFaceTermSum_eq_zero_of_boundary_component_eq_zero`
with boundary values expressed by `Function.update`.
This is often the more convenient shape for later support or cutoff lemmas:
if replacing coordinate `i` by either endpoint forces the `i`-th component of
`F` to vanish, then the signed face-term sum vanishes. This still assumes the
boundary values directly; compact-support and tail-decay proofs remain
separate obligations. -/Scope and omitted-condition boundaries
- No volume-integral identity is concluded.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- MeasureTheory.integral_zero
- Finset.sum_const_zero
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.