The unit cutoff equals one on the closed unit interval
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_eq_one_of_abs_le_one · theorem · Teaching coverage
Statement
For any real t satisfying |t|≤1, q(t)=1, including both endpoints t=−1 and t=1.
All objects and hypotheses
- x : ℝ with hx : |x|≤1.
Mathematical proof
1. Put the transition input in its upper plateau
The hypothesis gives 2−|t|≥1.
Corresponding Lean step
have h : (1 : ℝ) ≤ 2 - |x| := by linarith
2. Use the transition's value-one theorem
S(u)=1 whenever u≥1. Apply this at u=2−|t| and rewrite q using its evaluation formula.
Corresponding Lean step
simpa [smoothUnitCutoff_eq_smoothTransition] using (Real.smoothTransition.one_of_one_le (x := 2 - |x|) h)
Lean statement · smoothUnitCutoff_eq_one_of_abs_le_one
The implicit x is a real input and hx is the exact closed-interval premise.
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_one_of_abs_le_one {x : ℝ} (hx : |x| ≤ 1) :
smoothUnitCutoff x = 1Lean proof · smoothUnitCutoff_eq_one_of_abs_le_one
Actual proof outline: Put the transition input in its upper plateau: The linear arithmetic step is exactly the rearrangement of hx. Use the transition's value-one theorem: one_of_one_le includes equality at the endpoint, so this is a closed-interval assertion.
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_one_of_abs_le_one {x : ℝ} (hx : |x| ≤ 1) :
smoothUnitCutoff x = 1 := by
have h : (1 : ℝ) ≤ 2 - |x| := by linarith
simpa [smoothUnitCutoff_eq_smoothTransition] using
(Real.smoothTransition.one_of_one_le (x := 2 - |x|) h)
/-- The unit cutoff vanishes when `2 <= |x|`. -/Scope and omitted-condition boundaries
- Only a value identity is asserted; no derivative formula is added here.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- Real.smoothTransition.one_of_one_le
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.one_of_one_le — 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.