ASTIS mathematical exposition

The radial cutoff equals one on the inner closed ball

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

Statement

Let E be a normed additive commutative group, let R>0, and let x∈E satisfy ‖x‖≤R. Then the radius-R cutoff has value one at x.

\[R>0,\ \|x\|\le R\quad\Longrightarrow\quad\chi_R(x)=1.\]

All objects and hypotheses

E is a normed additive commutative group.
R∈ℝ, R>0, x∈E, and ‖x‖≤R.

Mathematical proof

1. Put the radial argument in the scalar plateau

Because R is positive and norms are nonnegative, the quotient is nonnegative. The assumed norm bound gives a quotient at most one, hence absolute value at most one.

\[0\le\frac{\|x\|}{R}\le1,\qquad \left|\frac{\|x\|}{R}\right|\le1.\]

Corresponding Lean step

rw [abs_of_nonneg (div_nonneg (norm_nonneg x) hR.le)]; exact div_le_one_of_le₀ hx hR.le

2. Use the scalar plateau value

The already-proved scalar cutoff equals one whenever its argument has absolute value at most one. Substitute the quotient.

\[\chi_R(x)=q(\|x\|/R)=1.\]

Corresponding Lean step

apply smoothUnitCutoff_eq_one_of_abs_le_one

Lean statement · radialSmoothCutoff_eq_one_of_norm_le

Curly braces mark inferred R and x; explicit arguments `hR` and `hx` are proofs of positivity and membership in the inner closed ball. The conclusion is equality of real values, not yet a smoothness statement. 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_eq_one_of_norm_le {R : ℝ} (hR : 0 < R) {x : E}
    (hx : ‖x‖ ≤ R) : radialSmoothCutoff R x = 1

Exact module and namespace context

Lean proof · radialSmoothCutoff_eq_one_of_norm_le

Actual proof outline: Put the radial argument in the scalar plateau: `hR` is the proof that R is positive, and `hx` is the norm bound. These lines discharge the absolute-value premise of the scalar plateau theorem. Use the scalar plateau value: `apply` reduces this radial value statement to the precise scalar condition verified in the preceding mathematical step.

theorem radialSmoothCutoff_eq_one_of_norm_le {R : ℝ} (hR : 0 < R) {x : E}
    (hx : ‖x‖ ≤ R) : radialSmoothCutoff R x = 1 := by
  apply smoothUnitCutoff_eq_one_of_abs_le_one
  rw [abs_of_nonneg (div_nonneg (norm_nonneg x) hR.le)]
  exact div_le_one_of_le₀ hx hR.le

/-- The radial cutoff vanishes when `2 * R <= ||x||`. -/

Exact module and namespace context

Scope and omitted-condition boundaries

The sphere ‖x‖=R is included; this theorem alone does not say the function is locally constant at that sphere.

Source and reuse

ASTIS parents called

Mathlib API called (external library)

div_le_one_of_le₀
abs_of_nonneg

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.
div_le_one_of_le₀ — Exact checked local Mathlib lemma used in this proof.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff — Exact earlier ASTIS definition or theorem used in this declaration; not an independent external-source claim.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.smoothUnitCutoff_eq_one_of_abs_le_one — 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.