ASTIS mathematical exposition

Scalar closed support localizes the product's ordinary support

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

Statement

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

\[\operatorname{tsupp}\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.
tsupport χ⊆O.

Mathematical proof

1. Forget the closure and apply scalar support localization

Ordinary support lies in topological support, so supp χ⊆O. Apply the scalar ordinary-support product lemma to get supp H⊆O.

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

Corresponding Lean step

support_subset_univ_pi_Ioo_of_tsupport_subset_univ_pi_Ioo hχtsupp; support_smul_subset_univ_pi_Ioo_of_scalar_support_subset_univ_pi_Ioo.

Lean statement · support_smul_subset_univ_pi_Ioo_of_scalar_tsupport_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_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))) :
    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_tsupport_subset_univ_pi_Ioo

Ordinary support lies in topological support, so supp χ⊆O. Apply the scalar ordinary-support product lemma to get supp H⊆O. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.

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

/-- Closed-box continuity for a scalar cutoff times a Pi-space vector field.

This packages Mathlib's `ContinuousOn.smul` in the exact finite-box shape used
by the cutoff-smul divergence-theorem route.  It does not prove smooth cutoff
construction, differentiability, trace integrability, or any boundary result. -/

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

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_subset_univ_pi_Ioo_of_tsupport_subset_univ_pi_Ioo — Exact ASTIS parent called in the proof steps above; this anchor adds no source-equivalence verdict.
Called library/source declaration: AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Divergence.support_smul_subset_univ_pi_Ioo_of_scalar_support_subset_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.