ASTIS mathematical exposition

Finite dimension makes the radial cutoff compactly supported

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_hasCompactSupport · theorem · Teaching coverage

Statement

Let E be a finite-dimensional real normed vector space and R>0. Then χ_R has compact support: the closure of its nonzero set is compact.

\[\dim_{\mathbb R}E<\infty,\ R>0\quad\Longrightarrow\quad\operatorname{tsupp}\chi_R\text{ is compact}.\]

All objects and hypotheses

E is a normed additive commutative group with a real normed-vector-space structure and `FiniteDimensional ℝ E`.
R∈ℝ with R>0; no inner-product-space or nontriviality assumption is present.

Mathematical proof

1. Place the closed support inside a compact ball

The closed support is closed by its definition as a closure and lies in the closed ball of radius 2R. In a finite-dimensional real normed vector space, this ball is compact.

\[\operatorname{tsupp}\chi_R\subseteq\overline B(0,2R),\qquad\overline B(0,2R)\text{ compact}.\]

Corresponding Lean step

isCompact_closedBall (0 : E) (2 * R); isClosed_closure; radialSmoothCutoff_tsupport_subset_closedBall hR

2. Use compactness of a closed subset

A closed subset of a compact set is compact. This is precisely the definition of compact support for χ_R.

\[\operatorname{tsupp}\chi_R\text{ closed in a compact containing ball}\quad\Longrightarrow\quad\operatorname{HasCompactSupport}(\chi_R).\]

Corresponding Lean step

rw [hasCompactSupport_def]; exact IsCompact.of_isClosed_subset ...

Lean statement · radialSmoothCutoff_hasCompactSupport

The finite-dimensional assumption enters the compactness argument rather than the value or support-inclusion lemmas. This theorem applies to arbitrary real norms, not just inner-product norms. The source's surrounding Radial section contributes the implicit type E and its NormedAddCommGroup instance; further structures appear explicitly in the declaration.

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 radialSmoothCutoff_hasCompactSupport [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {R : ℝ} (hR : 0 < R) :
    HasCompactSupport (radialSmoothCutoff R : E → ℝ)

Exact module and namespace context

Lean proof · radialSmoothCutoff_hasCompactSupport

Actual proof outline: Place the closed support inside a compact ball: Finite-dimensionality supplies the proper-space instance needed for the compact closed-ball fact; smoothness of χ_R is not used. Use compactness of a closed subset: `hasCompactSupport_def` unfolds the predicate into compactness of tsupport; `IsCompact.of_isClosed_subset` finishes that exact goal.

theorem radialSmoothCutoff_hasCompactSupport [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    {R : ℝ} (hR : 0 < R) :
    HasCompactSupport (radialSmoothCutoff R : E → ℝ) := by
  rw [hasCompactSupport_def]
  exact IsCompact.of_isClosed_subset
    (isCompact_closedBall (0 : E) (2 * R)) isClosed_closure
    (radialSmoothCutoff_tsupport_subset_closedBall hR)

/-- A single positive constant controls the second iterated Fréchet
derivative of every positive-scale radial cutoff by `C / R^2`.

The proof first bounds the second derivative of the unit-scale radial cutoff
using continuity and compact support.  It then writes the radius-`R` cutoff as
the unit cutoff composed with scalar dilation and applies Mathlib's exact
iterated-derivative composition rule for continuous linear maps. -/

Exact module and namespace context

Scope and omitted-condition boundaries

No compact-support theorem for an arbitrary infinite-dimensional space is asserted.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_tsupport_subset_closedBall

Mathlib API called (external library)

hasCompactSupport_def
isCompact_closedBall
isClosed_closure
IsCompact.of_isClosed_subset

Mathematical sources

Current ASTIS declaration and complete body — Authority for the statement, local assumptions, and actual proof/construction documented here.
Existing module card — Existing curated entry for this declaration. Attribution is preserved as local card evidence only, without a new external-source audit or source-equivalence verdict.
hasCompactSupport_def — Additive declaration generated by to_additive; compactness of the closure of ordinary support.
isCompact_closedBall — ProperSpace field exported at line 42; finite-dimensional normed-space instances supply properness.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_tsupport_subset_closedBall — Exact earlier ASTIS definition or theorem used in this declaration; not an independent external-source claim.
Existing test source — Existing direct example invocation inspected; no build or test run was performed.

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