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

Off-open-box vanishing cancels the signed face sum

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

Statement

For arbitrary endpoints a,b and F:P→P with F=0 outside O, the signed face sum Φ_a,b(F) is zero.

\[F|_{P\setminus O}=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.
  • F(x)=0 for every x∉O.

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. Produce both update-boundary zero statements

An endpoint update lies outside O, so the preceding theorem gives its upper and lower component zeros.

\[F|_{P\setminus O}=0\Longrightarrow F_i(x[i\leftarrow a_i])=F_i(x[i\leftarrow b_i])=0.\]
Corresponding Lean step

update_boundary_component_eq_zero_of_eq_zero_off_univ_pi_Ioo a b F hoff.

2. Cancel the faces

Feed those two boundary statements into the update-shaped face-sum theorem.

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

signedFaceTermSum_eq_zero_of_update_boundary_component_eq_zero ... hbdry.1 hbdry.2.

Lean statement · signedFaceTermSum_eq_zero_of_eq_zero_off_univ_pi_Ioo

This assembles two boundary lemmas. It contains no divergence-integrability assumption because it concludes only a face-sum equality.

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_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 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_eq_zero_off_univ_pi_Ioo

The source first an endpoint update lies outside O, so the preceding theorem gives its upper and lower component zeros. It finishes as follows: Feed those two boundary statements into the update-shaped face-sum theorem. 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 signedFaceTermSum_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 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
  have hbdry := update_boundary_component_eq_zero_of_eq_zero_off_univ_pi_Ioo a b F hoff
  exact signedFaceTermSum_eq_zero_of_update_boundary_component_eq_zero a b F hbdry.1 hbdry.2

/-- If the support of a Pi-space vector field is contained in the open box,
then the field vanishes outside that open box.

This is a support-to-boundary staging leaf.  It uses plain
`Function.support`; it does not assert compactness of the support and does not
construct a cutoff. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • No whole-space statement.

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.