Samplinglib
Lean gate not recorded for this source state main · 9bb7a7394ab0
Samplinglib mathematical lesson

Ordinary support inside the open box cancels all face terms

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

Read this first

Mathematical statement

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

\[\operatorname{supp}F\subseteq O\Longrightarrow\Phi_{a,b}(F)=0.\]
Lean statement · signedFaceTermSum_eq_zero_of_support_subset_univ_pi_Ioo

Only the finite-box boundary quantity is concluded. The assumption does not itself identify F as a smooth field.

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.

Download module (.lean)
theorem signedFaceTermSum_eq_zero_of_support_subset_univ_pi_Ioo
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hsupp : Function.support F ⊆ (Set.univ.pi fun i => Set.Ioo (a i) (b i))) :
    ∑ 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

Proof roadmap

  1. 1Turn support containment into off-box vanishing

    A nonzero value outside O would violate the support inclusion, so F=0 on P∖O.

  2. 2Invoke the off-box face cancellation theorem

    The established zero values imply all endpoint normal components vanish and therefore the signed face sum is zero.

Full assumptions and notation

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.
  • Function.support F⊆O; the hypothesis concerns the nonzero set.

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. Turn support containment into off-box vanishing

A nonzero value outside O would violate the support inclusion, so F=0 on P∖O.

\[F|_{P\setminus O}=0.\]
Corresponding Lean step

eq_zero_off_univ_pi_Ioo_of_support_subset_univ_pi_Ioo a b F hsupp.

2. Invoke the off-box face cancellation theorem

The established zero values imply all endpoint normal components vanish and therefore the signed face sum is zero.

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

signedFaceTermSum_eq_zero_of_eq_zero_off_univ_pi_Ioo a b F (...).

Lean verification

The exact proof begins folded immediately after the mathematical argument; the statement is folded beside the claim above.

Lean proof · signedFaceTermSum_eq_zero_of_support_subset_univ_pi_Ioo

The source first a nonzero value outside O would violate the support inclusion, so F=0 on P∖O. It finishes as follows: The established zero values imply all endpoint normal components vanish and therefore the signed face sum is zero. 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.

Download module (.lean)
theorem signedFaceTermSum_eq_zero_of_support_subset_univ_pi_Ioo
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (F : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hsupp : Function.support F ⊆ (Set.univ.pi fun i => Set.Ioo (a i) (b i))) :
    ∑ 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_eq_zero_off_univ_pi_Ioo a b F
    (eq_zero_off_univ_pi_Ioo_of_support_subset_univ_pi_Ioo a b F hsupp)

Exact module and namespace context

Scope and omitted-condition boundaries
  • No volume-integral or whole-space theorem.
Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the Samplinglib parents.

Mathematical sources

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