Samplinglib mathematical lesson

The closed support lies in the same outer closed ball

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

Read this first

Mathematical statement

Let E be a normed additive commutative group and R>0. The topological support of χ_R, defined as the closure of its nonzero set, is contained in the closed ball about zero of radius 2R.

\[\operatorname{tsupp}\chi_R:=\overline{\{x:\chi_R(x)\ne0\}}\subseteq\overline B(0,2R).\]

Lean statement · radialSmoothCutoff_tsupport_subset_closedBall

This is a short topological wrapper around the ordinary-support inclusion. It is useful for compact-support arguments, which concern the closed support. 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.

Download module (.lean)

theorem radialSmoothCutoff_tsupport_subset_closedBall {R : ℝ} (hR : 0 < R) :
    tsupport (radialSmoothCutoff R : E → ℝ) ⊆
      Metric.closedBall 0 (2 * R)

Exact module and namespace context

Proof roadmap

1Take closure inside the closed containing ball
The preceding theorem places the ordinary support inside the outer closed ball. Because that ball is closed, it also contains the closure of the support.

Full assumptions and notation

All objects and hypotheses

E is a normed additive commutative group.
R∈ℝ with R>0.
Topological support is the closure of ordinary support.

Mathematical proof

1. Take closure inside the closed containing ball

The preceding theorem places the ordinary support inside the outer closed ball. Because that ball is closed, it also contains the closure of the support.

\[\operatorname{supp}\chi_R\subseteq\overline B(0,2R),\quad\overline B(0,2R)\text{ closed}\quad\Longrightarrow\quad\overline{\operatorname{supp}\chi_R}\subseteq\overline B(0,2R).\]

Corresponding Lean step

closure_minimal (radialSmoothCutoff_support_subset_closedBall hR) Metric.isClosed_closedBall

Lean verification

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

Lean proof · radialSmoothCutoff_tsupport_subset_closedBall

Actual proof outline: Take closure inside the closed containing ball: `closure_minimal` is the topological fact that the closure is contained in every closed superset. The apparent change from support to tsupport is exactly this closure operation.

Download module (.lean)

theorem radialSmoothCutoff_tsupport_subset_closedBall {R : ℝ} (hR : 0 < R) :
    tsupport (radialSmoothCutoff R : E → ℝ) ⊆
      Metric.closedBall 0 (2 * R) := by
  exact closure_minimal
    (radialSmoothCutoff_support_subset_closedBall hR) Metric.isClosed_closedBall

Exact module and namespace context

Scope and omitted-condition boundaries

Containment in a bounded closed ball is not yet compactness in infinite dimension.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_support_subset_closedBall

Mathlib API called (external library)

closure_minimal
Metric.isClosed_closedBall

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.
closure_minimal — Exact checked local Mathlib lemma used in this proof.
Metric.isClosed_closedBall — Exact checked local Mathlib lemma used in this proof.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_support_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.

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