ASTIS mathematical exposition

Construct the fixed smooth unit cutoff

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

Statement

Define q:ℝ→ℝ to be Mathlib's inner-product bump base on the real line with outer-radius parameter 2. This is a fixed function, before any radial scale is chosen; its pointwise description is q(t)=S(2−|t|), where S is the smooth transition from 0 to 1.

\[q(t):=B_{\mathbb R}(2,t),\qquad B_E(\rho,x)=S\!\left(\frac{\rho-\|x\|}{\rho-1}\right),\qquad q(t)=S(2-|t|).\]

All objects and hypotheses

There are no explicit parameters: q is a fixed real-to-real function.

Construction and meaning

1. Use the existing smooth bump family

Mathlib's inner-product-space bump base supplies a family B_E(ρ,x), built from the smooth transition S and the norm. Select E=ℝ.

\[B_{\mathbb R}(\rho,t)=S\!\left(\frac{\rho-|t|}{\rho-1}\right).\]

Corresponding Lean step

ContDiffBumpBase.ofInnerProductSpace ℝ

2. Fix its scale parameter at two

Evaluate the family at ρ=2. The denominator becomes 1, which yields the transition expression proved formally in the next declaration.

\[q(t)=B_{\mathbb R}(2,t)=S(2-|t|).\]

Corresponding Lean step

(ContDiffBumpBase.ofInnerProductSpace ℝ).toFun 2

Lean statement · smoothUnitCutoff

noncomputable marks an abstract real function construction. The one-dimensional q is distinct from the later family χ_R on an arbitrary normed space.

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 smoothUnitCutoff : ℝ → ℝ

Exact module and namespace context

Lean construction · smoothUnitCutoff

Construction, not a theorem proof. Use the existing smooth bump family: This is an imported structure containing the family and its properties; no smooth-bump existence theorem is reproved. Fix its scale parameter at two: toFun extracts the function from the bump structure. This body constructs q; it is not a theorem proof.

noncomputable def smoothUnitCutoff : ℝ → ℝ :=
  (ContDiffBumpBase.ofInnerProductSpace ℝ).toFun 2

/-- The unit cutoff written using Mathlib's smooth transition function. -/

Exact module and namespace context

Scope and omitted-condition boundaries

Construction only; later declarations expose smoothness, values, support and derivative bounds.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

ContDiffBumpBase.ofInnerProductSpace

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.
ContDiffBumpBase.ofInnerProductSpace — Exact checked local Mathlib dependency definition or theorem.
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.