Samplinglib mathematical lesson

Evaluate the unit cutoff through the smooth transition

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

Read this first

Mathematical statement

For every real t, the fixed unit cutoff is q(t)=S(2−|t|), where S=Real.smoothTransition.

\[\forall t\in\mathbb R,\quad q(t)=S(2-|t|).\]

Lean statement · smoothUnitCutoff_eq_smoothTransition

This is an equality of functions evaluated at an arbitrary input. It adds an accessible formula for the existing definition, not a second cutoff.

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 smoothUnitCutoff_eq_smoothTransition (x : ℝ) :
    smoothUnitCutoff x = Real.smoothTransition (2 - |x|)

Exact module and namespace context

Proof roadmap

1Unfold the bump-base formula
The selected bump base evaluates S at (2−‖t‖)/(2−1).
2Simplify the real norm and denominator
On ℝ, ‖t‖=|t| and 2−1=1. Substitution leaves exactly S(2−|t|).

Full assumptions and notation

All objects and hypotheses

x : ℝ is arbitrary (called t in the display).

Mathematical proof

1. Unfold the bump-base formula

The selected bump base evaluates S at (2−‖t‖)/(2−1).

\[q(t)=S\!\left(\frac{2-\|t\|}{2-1}\right).\]

Corresponding Lean step

simp [smoothUnitCutoff, ContDiffBumpBase.ofInnerProductSpace, Real.norm_eq_abs, hden]

2. Simplify the real norm and denominator

On ℝ, ‖t‖=|t| and 2−1=1. Substitution leaves exactly S(2−|t|).

\[\|t\|=|t|,\quad 2-1=1,\quad (2-|t|)/1=2-|t|.\]

Corresponding Lean step

have hden : (2 : ℝ) - 1 = 1 := by norm_num

Lean verification

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

Lean proof · smoothUnitCutoff_eq_smoothTransition

Actual proof outline: Unfold the bump-base formula: The rewrite list uses the two actual definitions and the identity of the real norm with absolute value. Simplify the real norm and denominator: hden is a proved arithmetic equality, not an extra hypothesis; the final simp applies it.

Download module (.lean)

theorem smoothUnitCutoff_eq_smoothTransition (x : ℝ) :
    smoothUnitCutoff x = Real.smoothTransition (2 - |x|) := by
  have hden : (2 : ℝ) - 1 = 1 := by norm_num
  simp [smoothUnitCutoff, ContDiffBumpBase.ofInnerProductSpace, Real.norm_eq_abs, hden]

Exact module and namespace context

Scope and omitted-condition boundaries

Do not infer smoothness merely by treating |t| as differentiable at zero; smoothness is established separately.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff

Mathlib API called (external library)

ContDiffBumpBase.ofInnerProductSpace
Real.norm_eq_abs

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