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

Scalar ordinary support cancels product-field faces

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

Read this first

Mathematical statement

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

\[\operatorname{supp}\chi\subseteq O\Longrightarrow\Phi_{a,b}(\chi G)=0.\]
Lean statement · signedFaceTermSum_smul_eq_zero_of_scalar_support_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.

Download module (.lean)
theorem signedFaceTermSum_smul_eq_zero_of_scalar_support_subset_univ_pi_Ioo
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hχsupp : Function.support χ ⊆
      (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

Proof roadmap

  1. 1Localize the product's nonzero set

    The scalar condition makes χG zero outside O, so its ordinary support lies in O.

  2. 2Cancel the supported product's faces

    Apply the vector-support-to-face theorem to H=χG. It makes each normal component zero on the endpoint hyperplanes and gives the zero signed sum.

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.
  • χ: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.
  • supp χ⊆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. Localize the product's nonzero set

The scalar condition makes χG zero outside O, so its ordinary support lies in O.

\[\operatorname{supp}(\chi G)\subseteq O.\]
Corresponding Lean step

support_smul_subset_univ_pi_Ioo_of_scalar_support_subset_univ_pi_Ioo a b χ G.

2. Cancel the supported product's faces

Apply the vector-support-to-face theorem to H=χG. It makes each normal component zero on the endpoint hyperplanes and gives the zero signed sum.

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

signedFaceTermSum_eq_zero_of_support_subset_univ_pi_Ioo a b (fun x => χ x • G x).

Lean verification

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

Lean proof · signedFaceTermSum_smul_eq_zero_of_scalar_support_subset_univ_pi_Ioo

The source first the scalar condition makes χG zero outside O, so its ordinary support lies in O. It finishes as follows: Apply the vector-support-to-face theorem to H=χG. It makes each normal component zero on the endpoint hyperplanes and gives the zero signed sum. 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_smul_eq_zero_of_scalar_support_subset_univ_pi_Ioo
    {n : ℕ}
    (a b : Fin (n + 1) → ℝ)
    (χ : (Fin (n + 1) → ℝ) → ℝ)
    (G : (Fin (n + 1) → ℝ) → Fin (n + 1) → ℝ)
    (hχsupp : Function.support χ ⊆
      (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_eq_zero_of_support_subset_univ_pi_Ioo a b (fun x => χ x • G x)
    (support_smul_subset_univ_pi_Ioo_of_scalar_support_subset_univ_pi_Ioo a b χ G hχsupp)

Exact module and namespace context

Scope and omitted-condition boundaries
  • No integral of divergence is claimed by this boundary-only lemma.
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.