Samplinglib mathematical lesson

At each fixed point the cutoffs are eventually equal to one

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

Read this first

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

\[\forall x\in E,\qquad \lim_{R\to+\infty}\chi_R(x)=1,\qquad R\ge\|x\|+1\Longrightarrow\chi_R(x)=1.\]

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.

Download module (.lean)

theorem radialSmoothCutoff_tendsto_one (x : E) :
    Tendsto (fun R : ℝ => radialSmoothCutoff R x) atTop (𝓝 1)

Exact module and namespace context

Proof roadmap

1Choose 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.
2Use 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.

Full assumptions and notation

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.

\[R\ge R_0:=\|x\|+1\quad\Longrightarrow\quad R>0,\quad\|x\|\le 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.

\[\forall R\ge R_0,\ \chi_R(x)=1\quad\Longrightarrow\quad\chi_R(x)\longrightarrow1.\]

Corresponding Lean step

apply radialSmoothCutoff_eq_one_of_norm_le hR_pos; linarith

Lean verification

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

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.

Download module (.lean)

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

Exact module and namespace context

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.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_eq_one_of_norm_le

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.

Samplinglib prose is not a quotation or a source-equivalence certificate. Definitions and aliases are explained as constructions, not counted as new mathematical proofs.