Samplinglib mathematical lesson

The totalized derivative vanishes throughout the outer zero region

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

Read this first

Mathematical statement

Let E be a real normed vector space, let R>0, and let x∈E satisfy 2R≤‖x‖. Then Mathlib's totalized Fréchet derivative of χ_R at x is the zero continuous linear map. This includes the outer boundary sphere and does not assume an inner-product norm or differentiability of χ_R.

\[R>0,\ 2R\le\|x\|\quad\Longrightarrow\quad D_{\mathrm{tot}}\chi_R(x)=0.\]

Lean statement · radialSmoothCutoff_fderiv_eq_zero_of_two_mul_le_norm

The right-hand zero is the zero continuous linear map, not just a zero real value. At ‖x‖=2R the proof uses a minimum, not an unjustified locally-constant neighborhood. 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_fderiv_eq_zero_of_two_mul_le_norm [NormedSpace ℝ E]
    {R : ℝ} (hR : 0 < R) {x : E} (hx : 2 * R ≤ ‖x‖) :
    fderiv ℝ (radialSmoothCutoff R : E → ℝ) x = 0

Exact module and namespace context

Proof roadmap

1Recognize a global, hence local, minimum
The outer value theorem gives χ_R(x)=0. The range theorem gives χ_R(y)≥0 for every y∈E. Thus x is a global minimum, and in particular a local minimum.
2Apply the totalized form of Fermat's rule
At a differentiable local minimum the derivative is zero. Mathlib's theorem states this for totalized fderiv: if differentiability fails, fderiv is zero by definition instead. Consequently the same conclusion holds without an explicit differentiability assumption.

Full assumptions and notation

All objects and hypotheses

E is a normed additive commutative group equipped with a real normed-vector-space structure.
R>0, x∈E, and 2R≤‖x‖.
No differentiability or inner-product-space hypothesis is assumed; fderiv is totalized.

Mathematical proof

1. Recognize a global, hence local, minimum

The outer value theorem gives χ_R(x)=0. The range theorem gives χ_R(y)≥0 for every y∈E. Thus x is a global minimum, and in particular a local minimum.

\[\chi_R(x)=0\le\chi_R(y)\quad(\forall y\in E).\]

Corresponding Lean step

rw [radialSmoothCutoff_eq_zero_of_two_mul_le_norm hR hx]; exact Filter.Eventually.of_forall fun y => (radialSmoothCutoff_mem_Icc R y).1

2. Apply the totalized form of Fermat's rule

At a differentiable local minimum the derivative is zero. Mathlib's theorem states this for totalized fderiv: if differentiability fails, fderiv is zero by definition instead. Consequently the same conclusion holds without an explicit differentiability assumption.

\[x\text{ a local minimum of }\chi_R\quad\Longrightarrow\quad D_{\mathrm{tot}}\chi_R(x)=0.\]

Corresponding Lean step

apply IsLocalMin.fderiv_eq_zero

Lean verification

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

Lean proof · radialSmoothCutoff_fderiv_eq_zero_of_two_mul_le_norm

Actual proof outline: Recognize a global, hence local, minimum: `Filter.Eventually.of_forall` turns the inequality at all points into the neighborhood inequality defining a local minimum. Apply the totalized form of Fermat's rule: This exact library theorem handles both differentiability cases. The ASTIS proof supplies the local-minimum premise.

Download module (.lean)

theorem radialSmoothCutoff_fderiv_eq_zero_of_two_mul_le_norm [NormedSpace ℝ E]
    {R : ℝ} (hR : 0 < R) {x : E} (hx : 2 * R ≤ ‖x‖) :
    fderiv ℝ (radialSmoothCutoff R : E → ℝ) x = 0 := by
  apply IsLocalMin.fderiv_eq_zero
  change ∀ᶠ y in 𝓝 x, radialSmoothCutoff R x ≤ radialSmoothCutoff R y
  rw [radialSmoothCutoff_eq_zero_of_two_mul_le_norm hR hx]
  exact Filter.Eventually.of_forall fun y => (radialSmoothCutoff_mem_Icc R y).1

Exact module and namespace context

Scope and omitted-condition boundaries

On a general normed space this statement does not itself establish differentiability.
No strict inequality or omission of the boundary sphere should be substituted for the existing statement.

Sources, dependencies, and reuse

Source and reuse

Samplinglib parents called

Mathlib API called (external library)

IsLocalMin.fderiv_eq_zero
Filter.Eventually.of_forall
fderiv_zero_of_not_differentiableAt

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.
IsLocalMin.fderiv_eq_zero — Exact checked local Mathlib dependency definition or theorem.
fderiv_zero_of_not_differentiableAt — Explanatory library dependency behind totalization, not necessarily a direct call in this ASTIS body.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_eq_zero_of_two_mul_le_norm — Exact earlier ASTIS definition or theorem used in this declaration; not an independent external-source claim.
AutoSamplingTheory.TechnicalLemmas.Analysis.Calculus.Cutoff.radialSmoothCutoff_mem_Icc — 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.