At each fixed point the cutoffs are eventually equal to one
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_tendsto_one · theorem · Teaching coverage
Statement
For any normed additive commutative group E and any fixed x∈E, χ_R(x) tends to one as the real scale R tends to positive infinity. Indeed it equals one for every R≥‖x‖+1.
All objects and hypotheses
- E is a normed additive commutative group and x∈E is fixed.
- The limit is over all real R along `atTop`; sufficiently large R are automatically positive.
Mathematical proof
1. Choose a threshold depending on the fixed point
Take R₀=‖x‖+1. If R≥R₀, then R>0 and ‖x‖≤R, so the point lies on the inner plateau of χ_R.
Corresponding Lean step
apply tendsto_atTop_of_eventually_const (i₀ := ‖x‖ + 1); intro R hR; have hR_pos : 0 < R := by ...
2. Use eventual equality to obtain the limit
The inner-ball value theorem gives χ_R(x)=1 beyond this threshold. An eventually constant function converges to that constant.
Corresponding Lean step
apply radialSmoothCutoff_eq_one_of_norm_le hR_pos; linarith
Lean statement · radialSmoothCutoff_tendsto_one
`Tendsto ... atTop (𝓝 1)` expresses convergence to the neighborhood filter at one as R grows without bound. It is a pointwise result, and actually follows from exact eventual equality. The source's surrounding Radial section contributes the implicit type E and its NormedAddCommGroup instance; further structures appear explicitly in the declaration.
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 radialSmoothCutoff_tendsto_one (x : E) :
Tendsto (fun R : ℝ => radialSmoothCutoff R x) atTop (𝓝 1)Lean proof · radialSmoothCutoff_tendsto_one
Actual proof outline: Choose a threshold depending on the fixed point: The threshold is allowed to depend on x because x is fixed before the limit is stated. Use eventual equality to obtain the limit: `tendsto_atTop_of_eventually_const` supplies the limit once the remaining equality goal has been proved.
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 radialSmoothCutoff_tendsto_one (x : E) :
Tendsto (fun R : ℝ => radialSmoothCutoff R x) atTop (𝓝 1) := by
apply tendsto_atTop_of_eventually_const (i₀ := ‖x‖ + 1)
intro R hR
have hR_pos : 0 < R := by
calc
0 < ‖x‖ + 1 := by positivity
_ ≤ R := hR
apply radialSmoothCutoff_eq_one_of_norm_le hR_pos
linarith
end Radial
section Plateau
/-- A compact subset of an open set admits a smooth compactly supported plateau in that set.
The function takes values in `[0, 1]` and is identically one on the compact set. -/Scope and omitted-condition boundaries
- No measure, integrability hypothesis, dominated-convergence argument, or limit of integrals appears.
- No uniform convergence on all of E is asserted.
Source and reuse
ASTIS parents called
Mathlib API called (external library)
- tendsto_atTop_of_eventually_const
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.
- tendsto_atTop_of_eventually_const — Exact checked local Mathlib dependency definition or theorem.
- AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_eq_one_of_norm_le — 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.