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

Scalar topological support cancels product-field faces

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

Statement

For arbitrary endpoints a,b and functions χ:P→ℝ and G:P→P, assume tsupp χ⊆O. Then the signed face sum of H(x)=χ(x)G(x) is zero.

\[\operatorname{tsupp}\chi\subseteq O\Longrightarrow\Phi_{a,b}(\chi G)=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.
  • χ:P→ℝ and G:P→P; H=χG.
  • 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.
  • tsupp χ⊆O.
  • No a≤b, regularity, or integrability assumption.

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. Pass from closed support to ordinary support

Ordinary support lies in tsupport, giving supp χ⊆O. The already-proved scalar-support face theorem applies to the same product.

\[\operatorname{supp}\chi\subseteq\operatorname{tsupp}\chi\subseteq O\Longrightarrow\Phi_{a,b}(\chi G)=0.\]
Corresponding Lean step

support_subset_univ_pi_Ioo_of_tsupport_subset_univ_pi_Ioo; signedFaceTermSum_smul_eq_zero_of_scalar_support_subset_univ_pi_Ioo.

Lean statement · signedFaceTermSum_smul_eq_zero_of_scalar_tsupport_subset_univ_pi_Ioo

The conclusion concerns only the face-integral expression for the product. Scalar support does not automatically supply the product's continuity or derivative trace integrability.

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_smul_eq_zero_of_scalar_tsupport_subset_univ_pi_Ioo
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hχtsupp : tsupport χ ⊆
      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),
            (χ (i.insertNth (b i) x) • G (i.insertNth (b i) x)) i) -
          ∫ x in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
            (χ (i.insertNth (a i) x) • G (i.insertNth (a i) x)) i) = 0

Exact module and namespace context

Lean proof · signedFaceTermSum_smul_eq_zero_of_scalar_tsupport_subset_univ_pi_Ioo

Ordinary support lies in tsupport, giving supp χ⊆O. The already-proved scalar-support face theorem applies to the same product. 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_smul_eq_zero_of_scalar_tsupport_subset_univ_pi_Ioo
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hχtsupp : tsupport χ ⊆
      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),
            (χ (i.insertNth (b i) x) • G (i.insertNth (b i) x)) i) -
          ∫ x in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove),
            (χ (i.insertNth (a i) x) • G (i.insertNth (a i) x)) i) = 0 :=
  signedFaceTermSum_smul_eq_zero_of_scalar_support_subset_univ_pi_Ioo a b χ G
    (support_subset_univ_pi_Ioo_of_tsupport_subset_univ_pi_Ioo hχtsupp)

/-- Finite-box zero-face corollary for ASTIS coordinate divergence.

This is the smallest finite-box integration-by-parts handoff: once the signed
face term from Mathlib's divergence theorem is explicitly known to vanish, the
box integral of the coordinate divergence is zero.

It does not prove that the face term vanishes, does not pass to whole space,
and does not state a Langevin invariant law. -/

Exact module and namespace context

Scope and omitted-condition boundaries

  • No integral of divergence is claimed by this boundary-only lemma.

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.