ASTIS mathematical exposition

Every radial cutoff value lies between zero and one

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

Statement

For every normed additive commutative group E, every real scale R, and every x∈E, the cutoff value χ_R(x) belongs to [0,1].

\[\forall R\in\mathbb R\ \forall x\in E,\qquad0\le\chi_R(x)\le1.\]

All objects and hypotheses

E is a normed additive commutative group.
R is arbitrary, including zero or negative values; x is any point of E.

Mathematical proof

1. Reuse the scalar range theorem at the radial argument

The scalar bound holds at every real input, so it applies directly to ‖x‖/R without a positivity condition on R.

\[q(t)\in[0,1]\ \text{for all }t\in\mathbb R\quad\Longrightarrow\quad q(\|x\|/R)\in[0,1].\]

Corresponding Lean step

smoothUnitCutoff_mem_Icc _

Lean statement · radialSmoothCutoff_mem_Icc

`Set.Icc (0 : ℝ) 1` is the closed real interval; membership is a pair of inequalities. This is one of the statements intentionally valid at all totalized scales. 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_mem_Icc (R : ℝ) (x : E) :
    radialSmoothCutoff R x ∈ Set.Icc (0 : ℝ) 1

Exact module and namespace context

Lean proof · radialSmoothCutoff_mem_Icc

Actual proof outline: Reuse the scalar range theorem at the radial argument: The underscore asks Lean to infer the particular input ‖x‖/R. This one-line wrapper does not supply new range analysis.

theorem radialSmoothCutoff_mem_Icc (R : ℝ) (x : E) :
    radialSmoothCutoff R x ∈ Set.Icc (0 : ℝ) 1 :=
  smoothUnitCutoff_mem_Icc _

/-- Scaling the norm by a positive radius gives an operator-norm derivative
bound of `1 / R`.  Mathlib's totalized `fderiv` makes the statement valid at
the origin as well. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The all-scale range bound does not extend positive-radius support or scale-decay theorems to nonpositive R.
No direct named invocation was found in the inspected cutoff example block Tests/Basic.lean:49–169; this is not a statement about all possible project consumers.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

No direct Mathlib call recorded; see the ASTIS parents.

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.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff — Exact earlier ASTIS definition or theorem used in this declaration; not an independent external-source claim.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_mem_Icc — Exact earlier ASTIS definition or theorem used in this declaration; not an independent external-source claim.

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