Samplinglib mathematical lesson

The radial cutoff vanishes on and beyond the outer sphere

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

Read this first

Mathematical statement

Let E be a normed additive commutative group and let R>0. For every x∈E with 2R≤‖x‖, the radius-R cutoff vanishes.

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

Lean statement · radialSmoothCutoff_eq_zero_of_two_mul_le_norm

The inequality is non-strict, so the exported zero region includes the boundary sphere of radius 2R. No differentiable structure on E is needed for this value assertion. 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_eq_zero_of_two_mul_le_norm {R : ℝ} (hR : 0 < R) {x : E}
    (hx : 2 * R ≤ ‖x‖) : radialSmoothCutoff R x = 0

Exact module and namespace context

Proof roadmap

1Put the radial argument outside the scalar support region
The radial argument is nonnegative. Dividing the assumed inequality by the positive radius shows it is at least two.
2Apply scalar vanishing
The scalar cutoff vanishes whenever the argument has absolute value at least two. Applying that fact gives the desired zero value.

Full assumptions and notation

All objects and hypotheses

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

Mathematical proof

1. Put the radial argument outside the scalar support region

The radial argument is nonnegative. Dividing the assumed inequality by the positive radius shows it is at least two.

\[\left|\frac{\|x\|}{R}\right|=\frac{\|x\|}{R}\ge\frac{2R}{R}=2.\]

Corresponding Lean step

rw [abs_of_nonneg (div_nonneg (norm_nonneg x) hR.le)]; calc (2 : ℝ) = 2 * R / R := by field_simp; _ ≤ ‖x‖ / R := div_le_div_of_nonneg_right hx hR.le

2. Apply scalar vanishing

The scalar cutoff vanishes whenever the argument has absolute value at least two. Applying that fact gives the desired zero value.

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

Corresponding Lean step

apply smoothUnitCutoff_eq_zero_of_two_le_abs

Lean verification

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

Lean proof · radialSmoothCutoff_eq_zero_of_two_mul_le_norm

Actual proof outline: Put the radial argument outside the scalar support region: The proof uses positivity both to remove absolute values and to preserve the inequality on division. `field_simp` verifies cancellation of the nonzero radius. Apply scalar vanishing: This is a radial substitution into the scalar zero-value theorem.

Download module (.lean)

theorem radialSmoothCutoff_eq_zero_of_two_mul_le_norm {R : ℝ} (hR : 0 < R) {x : E}
    (hx : 2 * R ≤ ‖x‖) : radialSmoothCutoff R x = 0 := by
  apply smoothUnitCutoff_eq_zero_of_two_le_abs
  rw [abs_of_nonneg (div_nonneg (norm_nonneg x) hR.le)]
  calc
    (2 : ℝ) = 2 * R / R := by field_simp
    _ ≤ ‖x‖ / R := div_le_div_of_nonneg_right hx hR.le

Exact module and namespace context

Scope and omitted-condition boundaries

Zero at a boundary point is not a claim of local constancy there.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

div_le_div_of_nonneg_right
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_div_of_nonneg_right — 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_zero_of_two_le_abs — 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.