ASTIS mathematical exposition

The radial cutoff at a real scale

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff · def · Teaching coverage

Statement

For a normed additive commutative group E, a real scale R, and a point x∈E, define χ_R(x) by applying the fixed scalar cutoff q to the quotient ‖x‖/R. This definition is meaningful for every R; positivity is imposed only in later theorems.

\[\chi_R:E\to\mathbb R,\qquad \chi_R(x):=q\!\left(\frac{\|x\|}{R}\right).\]

All objects and hypotheses

E is a normed additive commutative group; no real scalar multiplication is required.
R is any real number and x∈E; there is no hypothesis R>0.

Construction and meaning

1. Form the radial argument and apply the scalar cutoff

The norm produces a nonnegative real number. Divide this real number by R using Lean's total real division, then evaluate q. In particular, division by zero is defined to be zero, so the construction at R=0 is the constant-one function.

\[\chi_R=q\circ(x\mapsto\|x\|/R),\qquad \chi_0(x)=q(0)=1.\]

Corresponding Lean step

smoothUnitCutoff (‖x‖ / R)

Lean statement · radialSmoothCutoff

`(R : ℝ) (x : E) : ℝ` states that the construction accepts a real scale and an E-valued point and returns a real value. Calling it smooth does not itself prove smoothness; the separate smoothness theorem has stronger ambient assumptions and requires a positive radius. 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.

noncomputable def radialSmoothCutoff (R : ℝ) (x : E) : ℝ

Exact module and namespace context

Lean construction · radialSmoothCutoff

Construction, not a theorem proof. Form the radial argument and apply the scalar cutoff: This is the defining expression, not a proof. `noncomputable` allows use of the library's noncomputable smooth bump; `E` is inferred from the argument x.

noncomputable def radialSmoothCutoff (R : ℝ) (x : E) : ℝ :=
  smoothUnitCutoff (‖x‖ / R)

/-- The radial cutoff is one on the closed ball of radius `R`. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The displayed R=0 observation explains totalization and is not a separately exported declaration.
Negative scales are allowed by the definition, but this module exports no negative-radius ball or derivative-bound theorem.

Source and reuse

ASTIS parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff

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 module overview only; no exact per-declaration curated source-memory entry was found in this card.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff — Exact earlier ASTIS definition or theorem used in this declaration; not an independent external-source claim.
Existing test source — Definition occurs in a checked test statement; 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.