The unit cutoff vanishes at and beyond radius two
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_eq_zero_of_two_le_abs · theorem · Teaching coverage
Statement
For any real t with 2≤|t|, q(t)=0. The boundary points ±2 are included.
All objects and hypotheses
- x : ℝ with hx : 2≤|x|.
Mathematical proof
1. Put the transition input in its zero region
The hypothesis gives 2−|t|≤0.
Corresponding Lean step
have h : 2 - |x| ≤ 0 := by linarith
2. Apply the zero-value rule
S(u)=0 for u≤0. The unit-cutoff evaluation formula therefore gives q(t)=0.
Corresponding Lean step
simpa [smoothUnitCutoff_eq_smoothTransition] using (Real.smoothTransition.zero_of_nonpos (x := 2 - |x|) h)
Lean statement · smoothUnitCutoff_eq_zero_of_two_le_abs
The non-strict inequality is important: the function vanishes on the boundary itself.
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.
theorem smoothUnitCutoff_eq_zero_of_two_le_abs {x : ℝ} (hx : 2 ≤ |x|) :
smoothUnitCutoff x = 0Lean proof · smoothUnitCutoff_eq_zero_of_two_le_abs
Actual proof outline: Put the transition input in its zero region: h is the elementary consequence of hx needed by the transition API. Apply the zero-value rule: zero_of_nonpos is an imported value theorem, not a support or differentiability assumption.
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.
theorem smoothUnitCutoff_eq_zero_of_two_le_abs {x : ℝ} (hx : 2 ≤ |x|) :
smoothUnitCutoff x = 0 := by
have h : 2 - |x| ≤ 0 := by linarith
simpa [smoothUnitCutoff_eq_smoothTransition] using
(Real.smoothTransition.zero_of_nonpos (x := 2 - |x|) h)
/-- The unit cutoff takes values in `[0, 1]`. -/Scope and omitted-condition boundaries
- Vanishing at a boundary point must not be confused with being locally constant there.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- Real.smoothTransition.zero_of_nonpos
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.
- Real.smoothTransition.zero_of_nonpos — Exact checked local Mathlib dependency definition or theorem.
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_eq_smoothTransition — 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.
ASTIS prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.