Samplinglib mathematical lesson

Construct the fixed smooth unit cutoff

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

Read this first

Mathematical 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|).\]

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.

Download module (.lean)

noncomputable def smoothUnitCutoff : ℝ → ℝ

Exact module and namespace context

Proof roadmap

1Use 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=ℝ.
2Fix 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.

Full assumptions and notation

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 verification

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

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.

Download module (.lean)

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

Exact module and namespace context

Scope and omitted-condition boundaries

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

Sources, dependencies, and reuse

Source and reuse

Samplinglib 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.

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