ASTIS mathematical exposition

Scalar ordinary support localizes the product field

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

Statement

For endpoints a,b and arbitrary χ:P→ℝ and G:P→P, assume Function.support χ⊆O. Then the ordinary support of the product H(x)=χ(x)G(x) lies in O.

\[\operatorname{supp}\chi\subseteq O\quad\Longrightarrow\quad\operatorname{supp}(\chi G)\subseteq O.\]

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 are arbitrary; H(x)=χ(x)G(x). No continuity, differentiability, or endpoint-order hypothesis.
Function.support χ⊆O.

Mathematical proof

1. Derive scalar zero values outside O

If χ(x)≠0 then support containment puts x in O. Thus χ(x)=0 for x∉O.

\[\operatorname{supp}\chi\subseteq O\Longrightarrow\chi|_{P\setminus O}=0.\]

Corresponding Lean step

The local contradiction proof uses hχsupp hχne.

2. Apply the off-box scalar localization lemma

Using these scalar zero values, the previously proved support theorem places supp H in O.

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

Corresponding Lean step

support_smul_subset_univ_pi_Ioo_of_eq_zero_off_univ_pi_Ioo a b χ G.

Lean statement · support_smul_subset_univ_pi_Ioo_of_scalar_support_subset_univ_pi_Ioo

The conclusion is `Function.support (fun x => χ x • G x) ⊆ O`. No derivative or compactness property of the product is implicit.

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 support_smul_subset_univ_pi_Ioo_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))) :
    Function.support (fun x => χ x • G x) ⊆
      (Set.univ.pi fun i => Set.Ioo (a i) (b i))

Exact module and namespace context

Lean proof · support_smul_subset_univ_pi_Ioo_of_scalar_support_subset_univ_pi_Ioo

The source first if χ(x)≠0 then support containment puts x in O. Thus χ(x)=0 for x∉O. It finishes as follows: Using these scalar zero values, the previously proved support theorem places supp H in O. Intermediate steps below identify the actual helper calls and the conditions each one needs.

theorem support_smul_subset_univ_pi_Ioo_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))) :
    Function.support (fun x => χ x • G x) ⊆
      (Set.univ.pi fun i => Set.Ioo (a i) (b i)) := by
  exact support_smul_subset_univ_pi_Ioo_of_eq_zero_off_univ_pi_Ioo a b χ G
    (by
      intro x hxbox
      by_contra hχne
      exact hxbox (hχsupp hχne))

/-- If the topological support of a scalar cutoff is contained in the open
Pi-box, then multiplying any vector field by that cutoff is plain-supported in
the same open box.

This is the direct consumer-facing bridge from Mathlib's `tsupport` cutoff
output to the cutoff-smul support hypothesis used by the finite-box zero-face
route.  It does not prove cutoff construction, regularity of the smul field,
tail decay, or whole-space integration by parts. -/

Exact module and namespace context

Scope and omitted-condition boundaries

This produces ordinary support containment, not a compact-support or regularity theorem.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.support_smul_subset_univ_pi_Ioo_of_eq_zero_off_univ_pi_Ioo

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

Mathematical sources

Current ASTIS source — Exact statement and actual proof/construction authority; raw code intentionally omitted from this packet.
Existing curated module card — Existing declaration-specific attribution entry, read as documentation without a new source-equivalence verdict.
Called library/source declaration: AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.support_smul_subset_univ_pi_Ioo_of_eq_zero_off_univ_pi_Ioo — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
Existing focused test — Exact named declaration invocation located in an existing example; no test was run.

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