Samplinglib mathematical lesson

Every unit-cutoff value lies between zero and one

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

Read this first

Mathematical statement

For every real t, 0≤q(t)≤1.

\[\forall t\in\mathbb R,\qquad q(t)\in[0,1].\]

Lean statement · smoothUnitCutoff_mem_Icc

Icc 0 1 is the closed interval, so both endpoints are allowed.

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_mem_Icc (x : ℝ) : smoothUnitCutoff x ∈ Set.Icc (0 : ℝ) 1

Exact module and namespace context

Proof roadmap

1Evaluate the bump family's range guarantee
The bump base already includes the [0,1] range property at every parameter and input. Apply it to parameter 2 and t.

Full assumptions and notation

All objects and hypotheses

x : ℝ arbitrary.

Mathematical proof

1. Evaluate the bump family's range guarantee

The bump base already includes the [0,1] range property at every parameter and input. Apply it to parameter 2 and t.

\[B_{\mathbb R}(2,t)\in[0,1].\]

Corresponding Lean step

exact (ContDiffBumpBase.ofInnerProductSpace ℝ).mem_Icc 2 x

Lean verification

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

Lean proof · smoothUnitCutoff_mem_Icc

Actual proof outline: Evaluate the bump family's range guarantee: mem_Icc is the range field of the imported bump structure. Its two components are the lower and upper inequalities.

Download module (.lean)

theorem smoothUnitCutoff_mem_Icc (x : ℝ) : smoothUnitCutoff x ∈ Set.Icc (0 : ℝ) 1 := by
  exact (ContDiffBumpBase.ofInnerProductSpace ℝ).mem_Icc 2 x

Exact module and namespace context

Scope and omitted-condition boundaries

The theorem supplies bounds, not strict positivity throughout the transition region.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff

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