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

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

Read this first

Mathematical 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.\]
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.

Download module (.lean)
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

Proof roadmap

  1. 1Produce both update-boundary zero statements

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

  2. 2Cancel the faces

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

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

Download module (.lean)
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

Exact module and namespace context

Scope and omitted-condition boundaries
  • No whole-space statement.
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.