ASTIS mathematical exposition

Pass from closed support to ordinary support

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

Statement

For endpoints a,b and χ:P→ℝ, if tsupp χ⊆O then supp χ⊆O.

\[\operatorname{tsupp}\chi\subseteq O\quad\Longrightarrow\quad\operatorname{supp}\chi\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→ℝ; tsupp χ⊆O. No continuity, compactness, or endpoint-order assumption.

Mathematical proof

1. Use containment in the closure

Every set lies in its closure. Therefore ordinary support lies in topological support, and the given inclusion finishes the result.

\[\operatorname{supp}\chi\subseteq\operatorname{tsupp}\chi\subseteq O.\]

Corresponding Lean step

(subset_tsupport χ).trans hχ.

Lean statement · support_subset_univ_pi_Ioo_of_tsupport_subset_univ_pi_Ioo

This converts the support representation only; it does not construct χ.

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_subset_univ_pi_Ioo_of_tsupport_subset_univ_pi_Ioo
    {n : ℕ} {a b : Fin (n + 1) → ℝ}
    {χ : (Fin (n + 1) → ℝ) → ℝ}
    (hχ : tsupport χ ⊆ Set.univ.pi (fun i => Set.Ioo (a i) (b i))) :
    Function.support χ ⊆ Set.univ.pi (fun i => Set.Ioo (a i) (b i))

Exact module and namespace context

Lean proof · support_subset_univ_pi_Ioo_of_tsupport_subset_univ_pi_Ioo

Every set lies in its closure. Therefore ordinary support lies in topological support, and the given inclusion finishes the result. The Lean correspondence in that step identifies the exact existing rule or definitional reduction used.

theorem support_subset_univ_pi_Ioo_of_tsupport_subset_univ_pi_Ioo
    {n : ℕ} {a b : Fin (n + 1) → ℝ}
    {χ : (Fin (n + 1) → ℝ) → ℝ}
    (hχ : tsupport χ ⊆ Set.univ.pi (fun i => Set.Ioo (a i) (b i))) :
    Function.support χ ⊆ Set.univ.pi (fun i => Set.Ioo (a i) (b i)) := by
  exact (subset_tsupport χ).trans hχ

/-- Smooth finite-dimensional cutoff localized inside a Pi-open box, with both
topological-support and plain function-support conclusions.

This packages `exists_contDiff_cutoff_tsupport_subset_univ_pi_Ioo` with
`support_subset_univ_pi_Ioo_of_tsupport_subset_univ_pi_Ioo`, so downstream
finite-box support lemmas can consume the cutoff directly.  It remains local:
no exhausting cutoff family, derivative bookkeeping, tail limit, weighted IBP,
generator-domain theorem, invariant law, or reversibility is asserted. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Do not reverse this implication without an additional closure argument.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

subset_tsupport

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: subset_tsupport — Generated additive theorem from subset_mulTSupport at this source anchor.
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.